Switch to Bool b; prepare CardinalityetaExpandCorrect with the new cases
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 16 Jan 2015 11:59:08 +0000 (11:59 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 16 Jan 2015 11:59:08 +0000 (11:59 +0000)
13 files changed:
Launchbury/AbstractDenotational.thy
Launchbury/AbstractTransform.thy
Launchbury/ArityAnalysisPreImpl.thy
Launchbury/ArityAnalysisSpec.thy
Launchbury/CardinalityAnalysisSpec.thy
Launchbury/CardinalityEtaExpandCorrect.thy
Launchbury/CoCallAnalysisImpl.thy
Launchbury/DeadCodeRemoval.thy
Launchbury/DeadCodeRemoval2.thy
Launchbury/Sestoft.thy
Launchbury/SestoftConf.thy
Launchbury/Substitution.thy
Launchbury/Terms.thy

index f4fc96f..afac097 100644 (file)
@@ -24,7 +24,7 @@ where
 | "ESem (App e x) = (\<Lambda> \<rho>. tick \<cdot> (Fn_project \<cdot> (ESem e \<cdot> \<rho>) \<cdot> (\<rho> x)))"
 | "ESem (Var x) = (\<Lambda> \<rho>. tick \<cdot> (\<rho> x))"
 | "ESem (Let as body) = (\<Lambda> \<rho>. tick \<cdot> (ESem body \<cdot> (has_ESem.HSem ESem as \<cdot>  (\<rho> f|` fv (Let as body)))))"
-| "ESem Null = \<bottom>"
+| "ESem (Bool b) = \<bottom>"
 | "ESem (scrut ? e1 : e2) = \<bottom>"
 proof-
 txt {* The following proofs discharge technical obligations generated by the Nominal package. *}
index c5d9621..a2f8518 100644 (file)
@@ -37,7 +37,7 @@ begin
   | "transform a (Let \<Gamma> e) = TransLet (AnalLet \<Gamma> e a)
         (map_transform transform (PropLetHeap (AnalLet \<Gamma> e a)) \<Gamma>)
         (transform (PropLetBody (AnalLet \<Gamma> e a)) e)"
-  | "transform a Null = Null"
+  | "transform a (Bool b) = (Bool b)"
   | "transform a (scrut ? e1 : e2)  = (transform a scrut ? transform a e1 : transform a e2)"
 proof-
 case goal1
index ba7a2c7..92c6f5f 100644 (file)
@@ -36,7 +36,7 @@ where
 | "Aexp (Lam [x]. e) = (\<Lambda> n . (Aexp e \<cdot> (pred \<cdot> n)  f|` (fv (Lam [x]. e))))"
 | "Aexp (App e x) = (\<Lambda> n . Aexp e  \<cdot> (inc \<cdot> n) \<squnion> (esing x \<cdot> (up \<cdot> 0)))"
 | "Aexp (Terms.Let as e) = (\<Lambda> n . (Afix Aexp as \<cdot> (Aexp e \<cdot> n \<squnion> thunks_AE as)) f|` (fv (Terms.Let as e)))"
-| "Aexp Null = \<bottom>"
+| "Aexp (Bool b) = \<bottom>"
 | "Aexp (scrut ? e1 : e2) = \<bottom>"
 proof-
 case goal1
index d89de6c..9cc3f33 100644 (file)
@@ -9,6 +9,7 @@ locale CorrectArityAnalysis = SubstArityAnalysis +
   assumes Aexp_Var: "up \<cdot> n \<sqsubseteq> (Aexp (Var x)\<cdot>n) x"
   assumes Aexp_App: "Aexp e \<cdot>(inc\<cdot>n) \<squnion> esing x \<cdot> (up\<cdot>0) \<sqsubseteq>  Aexp (App e x) \<cdot> n"
   assumes Aexp_Lam: "env_delete y (Aexp e \<cdot>(pred\<cdot>n)) \<sqsubseteq> Aexp (Lam [y]. e) \<cdot> n"
+  assumes Aexp_IfThenElse: "Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a \<sqsubseteq> Aexp (scrut ? e1 : e2)\<cdot>a"
 
 locale CorrectArityAnalysisHeap = CorrectArityAnalysis + ArityAnalysisHeapEqvt +
   assumes edom_Aheap: "edom (Aheap \<Gamma> e\<cdot> a) \<subseteq> domA \<Gamma>"
index 2cfe496..943ade7 100644 (file)
@@ -26,6 +26,10 @@ locale CardinalityPrognosisVar = CardinalityPrognosis +
   assumes prognosis_Var_thunk: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> \<not> isVal e \<Longrightarrow> prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
   assumes prognosis_Var2: "isVal e \<Longrightarrow> x \<notin> domA \<Gamma> \<Longrightarrow> prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)"
 
+locale CardinalityPrognosisIfThenElse = CardinalityPrognosis +
+  assumes prognosis_IfThenElse: "prognosis ae 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> prognosis ae a (\<Gamma>, scrut ? e1 : e2, S)"
+  assumes prognosis_Alts: "prognosis ae a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, Bool b, Alts e1 e2 # S)"
+
 locale CardinalityPrognosisLet = CardinalityPrognosis + CardinalityHeap + ArityAnalysisHeap +
   assumes prognosis_Let:
   "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> edom ae \<subseteq> domA \<Gamma> \<union> upds S \<Longrightarrow> prognosis (Aheap \<Delta> e\<cdot>a \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae a (\<Gamma>, Terms.Let \<Delta> e, S)"
@@ -41,6 +45,7 @@ locale CardinalityPrognosisCorrect =
   CardinalityPrognosisLam + 
   CardinalityPrognosisVar +
   CardinalityPrognosisLet +
+  CardinalityPrognosisIfThenElse +
   CardinalityHeapCorrect +
   CorrectArityAnalysisLet
 
index ad18a29..fc5d51d 100644 (file)
@@ -41,6 +41,7 @@ begin
     | "stack_consistent as S \<Longrightarrow> stack_consistent as (Arg x # S)"
   inductive_simps stack_consistent_foo[simp]:
     "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)"
+  inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"
 
   fun AEstack :: "Arity list \<Rightarrow> stack \<Rightarrow> AEnv"
     where 
@@ -502,16 +503,39 @@ begin
     show ?case by (blast del: consistentI consistentE)
   next
     case (if\<^sub>1 \<Gamma> scrut e1 e2 S)
-    show ?case
-    sorry
-  next
-    case (if\<^sub>t \<Gamma> x e e1 e2 S)
-    show ?case
-    sorry
+    {
+    have "Aexp (scrut ? e1 : e2)\<cdot>a f|` edom ce \<sqsubseteq> ae" using if\<^sub>1 by (auto simp add: env_restr_join join_below_iff)
+    hence "(Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a) f|` edom ce \<sqsubseteq> ae"
+      by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]])
+    moreover
+    have "prognosis ae a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
+    hence "prognosis ae 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
+      by (rule below_trans[OF prognosis_IfThenElse])
+    ultimately
+    have "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+      using if\<^sub>1  by (auto simp add: env_restr_join join_below_iff)
+    }
+    moreover
+    have "conf_transform (ae, ce, a, as) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+      sorry
+    ultimately
+    show ?case by (blast del: consistentI consistentE)
   next
-    case (if\<^sub>f \<Gamma> e1 e2 S)
-    show ?case
-    sorry
+    case (if\<^sub>2 \<Gamma> b e1 e2 S)
+    from if\<^sub>2 obtain a' as' where [simp]: "as = a' # as'" by auto
+    from if\<^sub>2 have [simp]: "a = 0" by auto
+
+    {
+    have "prognosis ae 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
+    hence "prognosis ae a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
+    then
+    have "consistent (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" 
+      using if\<^sub>2 by (auto simp add: env_restr_join join_below_iff)
+    }
+    moreover
+    have "conf_transform (ae, ce, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" sorry
+    ultimately
+    show ?case by (blast del: consistentI consistentE)
   next
     case refl thus ?case by auto
   next
index 77c9881..8811138 100644 (file)
@@ -74,7 +74,7 @@ where
 | "cCCexp (Lam [x]. e) = (\<Lambda> n . combined_restrict (fv (Lam [x]. e)) (fst (cCCexp e\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp e\<cdot>a))\<cdot>n))"
 | "cCCexp (App e x) =    (\<Lambda> n . (fst (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> (esing x \<cdot> (up\<cdot>0)),          snd (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> ccProd {x} (insert x (fv e))))"
 | "cCCexp (Let \<Gamma> e) =    (\<Lambda> n . combined_restrict (fv (Let \<Gamma> e)) (CoCallArityAnalysis.cccFix_choose cCCexp \<Gamma> \<cdot> (cCCexp e\<cdot>n)))"
-| "cCCexp Null =         \<bottom>"
+| "cCCexp (Bool b) =     \<bottom>"
 | "cCCexp (scrut ? e1 : e2) = \<bottom>"
 proof-
 case goal1
@@ -145,7 +145,7 @@ lemma cCCexp_eq[simp]:
   "cCCexp (Lam [x]. e)\<cdot>n = combined_restrict (fv (Lam [x]. e)) (fst (cCCexp e\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp e\<cdot>a))\<cdot>n)"
   "cCCexp (App e x)\<cdot>n =    (fst (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> (esing x \<cdot> (up\<cdot>0)),          snd (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> ccProd {x} (insert x (fv e)))"
   "cCCexp (Let \<Gamma> e)\<cdot>n =    combined_restrict (fv (Let \<Gamma> e)) (CoCallArityAnalysis.cccFix_choose cCCexp \<Gamma> \<cdot> (cCCexp e\<cdot>n))"
-  "cCCexp Null\<cdot>n = \<bottom>"
+  "cCCexp (Bool b)\<cdot>n = \<bottom>"
   "cCCexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
 by (simp_all)
 declare cCCexp.simps[simp del]
@@ -157,7 +157,7 @@ lemma Aexp_simps[simp]:
   "Aexp (App e x)\<cdot>n = Aexp e\<cdot>(inc\<cdot>n) \<squnion> esing x\<cdot>(up\<cdot>0)"
   "\<not> nonrec \<Gamma> \<Longrightarrow> Aexp (Let \<Gamma> e)\<cdot>n = (Afix \<Gamma>\<cdot>(Aexp e\<cdot>n \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` (fv (Let \<Gamma> e))"
   "atom x \<sharp> e \<Longrightarrow> Aexp (let x be e in exp)\<cdot>n = (fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> (Aexp exp\<cdot>n, CCexp exp\<cdot>n)) \<squnion> Aexp exp\<cdot>n) f|` (fv (let x be e in exp))"
-  "Aexp Null\<cdot>n = \<bottom>"
+  "Aexp (Bool b)\<cdot>n = \<bottom>"
   "Aexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq)+
 
@@ -169,7 +169,7 @@ lemma CCexp_simps[simp]:
   "\<not> nonrec \<Gamma> \<Longrightarrow> CCexp (Let \<Gamma> e)\<cdot>n = cc_restr (fv (Let \<Gamma> e)) (CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>n  \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>n))"
   "atom x \<sharp> e \<Longrightarrow> CCexp (let x be e in exp)\<cdot>n =
     cc_restr (fv (let x be e in exp)) (ccBind x e \<cdot>(Aheap_nonrec x e\<cdot>(Aexp exp\<cdot>n, CCexp exp\<cdot>n), CCexp exp\<cdot>n) \<squnion> ccProd (fv e) (ccNeighbors x (CCexp exp\<cdot>n) - (if isVal e then {} else {x})) \<squnion> CCexp exp\<cdot>n)"
-  "CCexp Null\<cdot>n = \<bottom>"
+  "CCexp (Bool b)\<cdot>n = \<bottom>"
   "CCexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq predCC_eq)+
 
index 46b07ec..a2867fa 100644 (file)
@@ -11,7 +11,7 @@ where
 | "remove_dead_code (Let as e) =
     (if domA as \<inter> fv e = {} then remove_dead_code e
                            else Let (map_ran (\<lambda> _ e. remove_dead_code e) as) (remove_dead_code e))"
-| "remove_dead_code Null = Null"
+| "remove_dead_code (Bool b) = Bool b"
 | "remove_dead_code (scrut ? e1 : e2) = (remove_dead_code scrut ? remove_dead_code e1 : remove_dead_code e2)"
 proof-
 case goal1 thus ?case
index 87042b6..30f56e0 100644 (file)
@@ -92,7 +92,7 @@ where
 | "remove_dead_code (App e x) = App (remove_dead_code e) x"
 | "remove_dead_code (Var x) = Var x"
 | "remove_dead_code (Terms.Let as e) = SmartLet (restrict_reachable (map_ran (\<lambda> _ e. remove_dead_code e) as) (remove_dead_code e)) (remove_dead_code e)"
-| "remove_dead_code Null = Null"
+| "remove_dead_code (Bool b) = Bool b"
 | "remove_dead_code (scrut ? e1 : e2) = (remove_dead_code scrut ? remove_dead_code e1 : remove_dead_code e2)"
 proof-
 case goal1 thus ?case
index b6c30f3..ab3c640 100644 (file)
@@ -9,8 +9,7 @@ inductive step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightar
 | var\<^sub>2:  "x \<notin> domA \<Gamma> \<Longrightarrow> isVal e \<Longrightarrow> (\<Gamma>, e, Upd x # S) \<Rightarrow> ((x,e)# \<Gamma>, e , S)"
 | let\<^sub>1:  "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> (\<Gamma>, Let \<Delta> e, S) \<Rightarrow> (\<Delta>@\<Gamma>, e , S)"
 | if\<^sub>1:  "(\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow> (\<Gamma>, scrut, Alts e1 e2 # S)"
-| if\<^sub>t:  "(\<Gamma>, (Lam [x].e), Alts e1 e2 # S) \<Rightarrow> (\<Gamma>, e1, S)"
-| if\<^sub>f:  "(\<Gamma>, Null, Alts e1 e2 # S) \<Rightarrow> (\<Gamma>, e2, S)"
+| if\<^sub>2:  "(\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow> (\<Gamma>, if b then e1 else e2, S)"
 
 abbreviation steps (infix "\<Rightarrow>\<^sup>*" 50) where "steps \<equiv> step\<^sup>*\<^sup>*"
 
@@ -26,7 +25,7 @@ text {* An induction rule that skips the annoying case of a lambda taken off the
 
 thm step.induct[no_vars]
 
-lemma step_induction[consumes 2, case_names app\<^sub>1 app\<^sub>2 thunk lamvar var\<^sub>2 let\<^sub>1 if\<^sub>1 if\<^sub>t if\<^sub>f refl trans]:
+lemma step_induction[consumes 2, case_names app\<^sub>1 app\<^sub>2 thunk lamvar var\<^sub>2 let\<^sub>1 if\<^sub>1 if\<^sub>2 refl trans]:
   assumes "c \<Rightarrow>\<^sup>* c'"
   assumes "\<not> boring_step c'"
   assumes app\<^sub>1:  "\<And> \<Gamma> e x S . P (\<Gamma>, App e x, S)  (\<Gamma>, e , Arg x # S)"
@@ -36,8 +35,7 @@ lemma step_induction[consumes 2, case_names app\<^sub>1 app\<^sub>2 thunk lamvar
   assumes var\<^sub>2:  "\<And> \<Gamma> x e S . x \<notin> domA \<Gamma> \<Longrightarrow> isVal e \<Longrightarrow> P (\<Gamma>, e, Upd x # S) ((x,e)# \<Gamma>, e , S)"
   assumes let\<^sub>1:  "\<And> \<Delta> \<Gamma> e S . atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> P (\<Gamma>, Let \<Delta> e, S) (\<Delta>@\<Gamma>, e, S)"
   assumes if\<^sub>1:   "\<And>\<Gamma> scrut e1 e2 S. P (\<Gamma>, scrut ? e1 : e2, S) (\<Gamma>, scrut, Alts e1 e2 # S)"
-  assumes if\<^sub>t:   "\<And>\<Gamma> x e e1 e2 S. P (\<Gamma>, Lam [x]. e, Alts e1 e2 # S) (\<Gamma>, e1, S)"
-  assumes if\<^sub>f:   "\<And>\<Gamma> e1 e2 S. P (\<Gamma>, Null, Alts e1 e2 # S) (\<Gamma>, e2, S)"
+  assumes if\<^sub>2:   "\<And>\<Gamma> b e1 e2 S. P (\<Gamma>, Bool b, Alts e1 e2 # S) (\<Gamma>, if b then e1 else e2, S)"
   assumes refl: "\<And> c. P c c"
   assumes trans[trans]: "\<And> c c' c''. c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c' \<Rightarrow>\<^sup>* c'' \<Longrightarrow> P c c' \<Longrightarrow> P c' c'' \<Longrightarrow> P c c''"
   shows "P c c'"
@@ -92,10 +90,7 @@ proof-
         case if\<^sub>1 hence "P y z" using assms(9) by metis
         with `P c y` show ?thesis by (metis t)
       next
-        case if\<^sub>t hence "P y z" using assms(10) by metis
-        with `P c y` show ?thesis by (metis t)
-      next
-        case if\<^sub>f hence "P y z" using assms(11) by metis
+        case if\<^sub>2 hence "P y z" using assms(10) by metis
         with `P c y` show ?thesis by (metis t)
       qed
     next
index 4952f25..f17b50d 100644 (file)
@@ -87,6 +87,8 @@ lemma heap_upds_okE: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> x \<in> domA
 lemma heap_upds_ok_Nil[simp]: "heap_upds_ok (\<Gamma>, [])" by auto
 lemma heap_upds_ok_app1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Arg x # S)" by auto
 lemma heap_upds_ok_app2: "heap_upds_ok (\<Gamma>, Arg x # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
+lemma heap_upds_ok_alts1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Alts e1 e2 # S)" by auto
+lemma heap_upds_ok_alts2: "heap_upds_ok (\<Gamma>, Alts e1 e2 # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
 
 lemma heap_upds_ok_append:
   assumes "domA \<Delta> \<inter> domA \<Gamma> = {}"
@@ -109,7 +111,7 @@ lemma heap_upds_ok_reorder:
   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok ((x,e) # delete x \<Gamma>, S)"
   by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)
 
-lemmas heap_upds_ok_intros[intro] = heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_reorder heap_upds_ok_app1 heap_upds_ok_app2
+lemmas heap_upds_ok_intros[intro] = heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_reorder heap_upds_ok_app1 heap_upds_ok_app2 heap_upds_ok_alts1 heap_upds_ok_alts2
 lemmas heap_upds_ok.simps[simp del]
 
 fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
index ce4d11a..9ab0ab4 100644 (file)
@@ -17,7 +17,7 @@ where
  |"(App e v)[y ::= z] = App (e[y ::= z]) (v[y ::v= z])"
  |"atom ` domA as \<sharp>* (y,z) \<Longrightarrow> (Let as body)[y ::= z] = Let (as[y ::h= z]) (body[y ::= z])" 
  |"atom x \<sharp> (y,z) \<Longrightarrow> (Lam [x].e)[y ::= z] = Lam [x].(e[y::=z])"
- |"Null[y ::= z] = Null"
+ |"(Bool b)[y ::= z] = Bool b"
  |"(scrut ? e1 : e2)[y ::= z] = (scrut[y ::= z] ? e1[y ::= z] : e2[y ::= z])"
  |"[][y ::h= z] = []"
  |"((v,e)# as)[y ::h= z] = (v, e[y ::= z])# (as[y ::h= z])"
index 192fdf4..802e8da 100644 (file)
@@ -22,7 +22,7 @@ nominal_datatype exp =
 | App exp var
 | LetA as::assn body::exp binds "bn as" in body as
 | Lam x::var body::exp binds x in body  ("Lam [_]. _" [100, 100] 100)
-| Null
+| Bool bool
 | IfThenElse exp exp exp  ("((_)/ ? (_)/ : (_))" [0, 0, 10] 10)
 and assn =
   ANil | ACons var exp assn
@@ -156,8 +156,8 @@ lemma Let_distinct[simp]:
   "Lam [v]. e' \<noteq> Let \<Gamma> e"
   "Let \<Gamma> e \<noteq> Lam [v]. e'"
   "Let \<Gamma> e' \<noteq> App e v"
-  "Null \<noteq> Let \<Gamma> e"
-  "Let \<Gamma> e \<noteq> Null"
+  "Bool b \<noteq> Let \<Gamma> e"
+  "Let \<Gamma> e \<noteq> Bool b"
   "(scrut ? e1 : e2) \<noteq> Let \<Gamma> e"
   "Let \<Gamma> e \<noteq> (scrut ? e1 : e2)"
   unfolding Let_def by simp_all
@@ -195,7 +195,7 @@ lemma exp_strong_exhaust:
   assumes "\<And>exp var. y = App exp var \<Longrightarrow> P"
   assumes "\<And>\<Gamma> exp. atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> y = Let \<Gamma> exp \<Longrightarrow> P"
   assumes "\<And>var exp. {atom var} \<sharp>* c \<Longrightarrow> y = Lam [var]. exp \<Longrightarrow> P"
-  assumes "(y = Null) \<Longrightarrow> P"
+  assumes "\<And> b. (y = Bool b) \<Longrightarrow> P"
   assumes "\<And> scrut e1 e2. y = (scrut ? e1 : e2) \<Longrightarrow> P"
   shows P
   apply (rule  exp_assn.strong_exhaust(1)[where y = y and c = c])
@@ -211,12 +211,12 @@ text {*
 And finally the induction rules with @{term Let}.
 *}
 
-lemma exp_heap_induct[case_names Var App Let Lam Null IfThenElse Nil Cons]:
+lemma exp_heap_induct[case_names Var App Let Lam Bool IfThenElse Nil Cons]:
   assumes "\<And>b var. P1 (Var var)"
   assumes "\<And>exp var. P1 exp \<Longrightarrow> P1 (App exp var)"
   assumes "\<And>\<Gamma> exp. P2 \<Gamma> \<Longrightarrow> P1 exp \<Longrightarrow> P1 (Let \<Gamma> exp)"
   assumes "\<And>var exp. P1 exp \<Longrightarrow> P1 (Lam [var]. exp)"
-  assumes "P1 Null"
+  assumes "\<And> b. P1 (Bool b)"
   assumes "\<And> scrut e1 e2. P1 scrut \<Longrightarrow> P1 e1 \<Longrightarrow> P1 e2 \<Longrightarrow> P1 (scrut ? e1 : e2)"
   assumes "P2 []"
   assumes "\<And>var exp \<Gamma>. P1 exp \<Longrightarrow> P2 \<Gamma> \<Longrightarrow> P2 ((var, exp)#\<Gamma>)"
@@ -236,12 +236,12 @@ proof-
   thus "P1 e" and "P2 \<Gamma>" unfolding asToHeap_heapToAssn.
 qed
 
-lemma exp_heap_strong_induct[case_names Var App Let Lam Null IfThenElse Nil Cons]:
+lemma exp_heap_strong_induct[case_names Var App Let Lam Bool IfThenElse Nil Cons]:
   assumes "\<And>var c. P1 c (Var var)"
   assumes "\<And>exp var c. (\<And>c. P1 c exp) \<Longrightarrow> P1 c (App exp var)"
   assumes "\<And>\<Gamma> exp c. atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> (\<And>c. P2 c \<Gamma>) \<Longrightarrow> (\<And>c. P1 c exp) \<Longrightarrow> P1 c (Let \<Gamma> exp)"
   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P1 c exp) \<Longrightarrow> P1 c (Lam [var]. exp)"
-  assumes "\<And> c. P1 c Null"
+  assumes "\<And> b c. P1 c (Bool b)"
   assumes "\<And> scrut e1 e2 c. (\<And> c. P1 c scrut) \<Longrightarrow> (\<And> c. P1 c e1) \<Longrightarrow> (\<And> c. P1 c e2) \<Longrightarrow> P1 c (scrut ? e1 : e2)"
   assumes "\<And>c. P2 c []"
   assumes "\<And>var exp \<Gamma> c. (\<And>c. P1 c exp) \<Longrightarrow> (\<And>c. P2 c \<Gamma>) \<Longrightarrow> P2 c ((var,exp)#\<Gamma>)"
@@ -269,14 +269,14 @@ These rules can be used instead of the original induction rules, which require a
 goal for @{typ assn}.
 *}
 
-lemma exp_induct[case_names Var App Let Lam  Null IfThenElse]:
+lemma exp_induct[case_names Var App Let Lam Bool IfThenElse]:
   assumes "\<And>var. P (Var var)"
   assumes "\<And>exp var. P exp \<Longrightarrow> P (App exp var)"
   assumes "\<And>\<Gamma> exp. (\<And> x. x \<in> domA \<Gamma> \<Longrightarrow>  P (the (map_of \<Gamma> x))) \<Longrightarrow> P exp \<Longrightarrow> P (Let \<Gamma> exp)"
   assumes "\<And>var exp.  P exp \<Longrightarrow> P (Lam [var]. exp)"
-  assumes "P Null"
+  assumes "\<And> b. P (Bool b)"
   assumes "\<And> scrut e1 e2. P scrut \<Longrightarrow> P e1 \<Longrightarrow> P e2 \<Longrightarrow> P (scrut ? e1 : e2)"
-  shows "P  exp"
+  shows "P exp"
   apply (rule exp_heap_induct[of P "\<lambda> \<Gamma>. (\<forall>x \<in> domA \<Gamma>. P (the (map_of \<Gamma> x)))"])
   apply (metis assms(1))
   apply (metis assms(2))
@@ -287,14 +287,14 @@ lemma exp_induct[case_names Var App Let Lam  Null IfThenElse]:
   apply auto
   done
 
-lemma  exp_strong_induct_set[case_names Var App Let Lam Null IfThenElse]:
+lemma  exp_strong_induct_set[case_names Var App Let Lam Bool IfThenElse]:
   assumes "\<And>var c. P c (Var var)"
   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
   assumes "\<And>\<Gamma> exp c.
     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> (\<And>c x e. (x,e) \<in> set \<Gamma> \<Longrightarrow>  P c e) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
-  assumes "\<And> c. P c Null"
-  assumes "\<And> scrut e1 e2 c. (\<And> c. P c scrut) \<Longrightarrow> (\<And> c. P c e1) \<Longrightarrow> (\<And> c. P c e2) \<Longrightarrow> P c (scrut ? e1 : e2)"
+  assumes "\<And>b c. P c (Bool b)"
+  assumes "\<And>scrut e1 e2 c. (\<And> c. P c scrut) \<Longrightarrow> (\<And> c. P c e1) \<Longrightarrow> (\<And> c. P c e2) \<Longrightarrow> P c (scrut ? e1 : e2)"
   shows "P (c::'a::fs) exp"
   apply (rule exp_heap_strong_induct(1)[of P "\<lambda> c \<Gamma>. (\<forall>(x,e) \<in> set \<Gamma>. P c e)"])
   apply (metis assms(1))
@@ -307,13 +307,13 @@ lemma  exp_strong_induct_set[case_names Var App Let Lam Null IfThenElse]:
   done
 
 
-lemma  exp_strong_induct[case_names Var App Let Lam Null IfThenElse]:
+lemma  exp_strong_induct[case_names Var App Let Lam Bool IfThenElse]:
   assumes "\<And>var c. P c (Var var)"
   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
   assumes "\<And>\<Gamma> exp c.
     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> (\<And>c x. x \<in> domA \<Gamma> \<Longrightarrow>  P c (the (map_of \<Gamma> x))) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
-  assumes "\<And> c. P c Null"
+  assumes "\<And>b c. P c (Bool b)"
   assumes "\<And> scrut e1 e2 c. (\<And> c. P c scrut) \<Longrightarrow> (\<And> c. P c e1) \<Longrightarrow> (\<And> c. P c e2) \<Longrightarrow> P c (scrut ? e1 : e2)"
   shows "P (c::'a::fs) exp"
   apply (rule exp_heap_strong_induct(1)[of P "\<lambda> c \<Gamma>. (\<forall>x \<in> domA \<Gamma>. P c (the (map_of \<Gamma> x)))"])
@@ -361,8 +361,8 @@ lemma fv_App[simp]: "fv (App e x) = insert x (fv e)"
   unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base)
 lemma fv_Let[simp]: "fv (Let \<Gamma> e) = (fv \<Gamma> \<union> fv e) - domA \<Gamma>"
   unfolding fv_def by (auto simp add: Let_supp exp_assn.supp supp_at_base set_bn_to_atom_domA)
-lemma fv_Null[simp]: "fv Null = {}"
-  unfolding fv_def by (auto simp add: exp_assn.supp)
+lemma fv_Bool[simp]: "fv (Bool b) = {}"
+  unfolding fv_def by (auto simp add: exp_assn.supp pure_supp)
 lemma fv_IfThenElse[simp]: "fv (scrut ? e1 : e2)  = fv scrut \<union> fv e1 \<union> fv e2"
   unfolding fv_def by (auto simp add: exp_assn.supp)
 
@@ -492,7 +492,7 @@ nominal_function isLam :: "exp \<Rightarrow> bool" where
   "isLam (Lam [x]. e) = True" |
   "isLam (App e x) = False" |
   "isLam (Let as e) = False" |
-  "isLam Null = False" |
+  "isLam (Bool b) = False" |
   "isLam (scrut ? e1 : e2) = False"
   unfolding isLam_graph_aux_def eqvt_def
   apply simp
@@ -509,7 +509,7 @@ nominal_function isVal :: "exp \<Rightarrow> bool" where
   "isVal (Lam [x]. e) = True" |
   "isVal (App e x) = False" |
   "isVal (Let as e) = False" |
-  "isVal Null = True" |
+  "isVal (Bool b) = True" |
   "isVal (scrut ? e1 : e2) = False"
   unfolding isVal_graph_aux_def eqvt_def
   apply simp
@@ -520,7 +520,7 @@ nominal_function isVal :: "exp \<Rightarrow> bool" where
 nominal_termination (eqvt) by lexicographic_order
 
 lemma isVal_Lam: "isVal (Lam [x]. e)" by simp
-lemma isVal_Null: "isVal Null" by simp
+lemma isVal_Bool: "isVal (Bool b)" by simp
 
 
 subsubsection {* The notion of thunks *}
@@ -578,13 +578,13 @@ lemma nonrec_eqvt[eqvt]:
   "nonrec \<Gamma> \<Longrightarrow> nonrec (\<pi> \<bullet> \<Gamma>)"
   by (erule nonrecE) (auto simp add: nonrec_def)
 
-lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam Null IfThenElse]:
+lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
   assumes "\<And>var. P (Var var)"
   assumes "\<And>exp var. P exp \<Longrightarrow> P (App exp var)"
   assumes "\<And>\<Gamma> exp. \<not> nonrec \<Gamma> \<Longrightarrow> (\<And> x. x \<in> domA \<Gamma> \<Longrightarrow>  P (the (map_of \<Gamma> x))) \<Longrightarrow> P exp \<Longrightarrow> P (Let \<Gamma> exp)"
   assumes "\<And>x e exp. atom x \<sharp> e \<Longrightarrow> P e \<Longrightarrow> P exp \<Longrightarrow> P (let x be e in exp)"
   assumes "\<And>var exp.  P exp \<Longrightarrow> P (Lam [var]. exp)"
-  assumes "P Null"
+  assumes "\<And>b. P (Bool b)"
   assumes "\<And> scrut e1 e2. P scrut \<Longrightarrow> P e1 \<Longrightarrow> P e2 \<Longrightarrow> P (scrut ? e1 : e2)"
   shows "P exp"
   apply (rule exp_induct[of P])
@@ -600,14 +600,14 @@ lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam Null IfThenElse]:
   apply (metis assms(7))
   done
 
-lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam Null IfThenElse]:
+lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
   assumes "\<And>var c. P c (Var var)"
   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
   assumes "\<And>\<Gamma> exp c.
     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> \<not> nonrec \<Gamma> \<Longrightarrow> (\<And>c x. x \<in> domA \<Gamma> \<Longrightarrow>  P c (the (map_of \<Gamma> x))) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
   assumes "\<And>x e exp c. {atom x} \<sharp>* c \<Longrightarrow> atom x \<sharp> e \<Longrightarrow> (\<And> c. P c e) \<Longrightarrow> (\<And> c. P c exp) \<Longrightarrow> P c (let x be e in exp)"
   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
-  assumes "\<And> c. P c Null"
+  assumes "\<And>b c. P c (Bool b)"
   assumes "\<And> scrut e1 e2 c. (\<And> c. P c scrut) \<Longrightarrow> (\<And> c. P c e1) \<Longrightarrow> (\<And> c. P c e2) \<Longrightarrow> P c (scrut ? e1 : e2)"
   shows "P (c::'a::fs) exp"
   apply (rule exp_strong_induct[of P])
@@ -623,14 +623,14 @@ lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam Null IfThenEl
   apply (metis assms(7))
   done
 
-lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam Null IfThenElse]:
+lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam Bool IfThenElse]:
   assumes "\<And>var c. P c (Var var)"
   assumes "\<And>exp var c. (\<And>c. P c exp) \<Longrightarrow> P c (App exp var)"
   assumes "\<And>\<Gamma> exp c.
     atom ` domA \<Gamma> \<sharp>* c \<Longrightarrow> \<not> nonrec \<Gamma> \<Longrightarrow> (\<And>c x e. (x,e) \<in> set \<Gamma> \<Longrightarrow>  P c e) \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Let \<Gamma> exp)"
   assumes "\<And>x e exp c. {atom x} \<sharp>* c \<Longrightarrow> atom x \<sharp> e \<Longrightarrow> (\<And> c. P c e) \<Longrightarrow> (\<And> c. P c exp) \<Longrightarrow> P c (let x be e in exp)"
   assumes "\<And>var exp c. {atom var} \<sharp>* c \<Longrightarrow> (\<And>c. P c exp) \<Longrightarrow> P c (Lam [var]. exp)"
-  assumes "\<And> c. P c Null"
+  assumes "\<And>b c. P c (Bool b)"
   assumes "\<And> scrut e1 e2 c. (\<And> c. P c scrut) \<Longrightarrow> (\<And> c. P c e1) \<Longrightarrow> (\<And> c. P c e2) \<Longrightarrow> P c (scrut ? e1 : e2)"
   shows "P (c::'a::fs) exp"
   apply (rule exp_strong_induct_set(1)[of P])