Add Null and (e ? e : e)
authorJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 13:25:49 +0000 (13:25 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 13:25:49 +0000 (13:25 +0000)
14 files changed:
Launchbury/Abstract-Denotational-Props.thy
Launchbury/AbstractDenotational.thy
Launchbury/AbstractTransform.thy
Launchbury/ArityAnalysisImplCorrect.thy
Launchbury/ArityAnalysisPreImpl.thy
Launchbury/CoCallAnalysisImpl.thy
Launchbury/CoCallImplCorrect.thy
Launchbury/DeadCodeRemoval.thy
Launchbury/DeadCodeRemoval2.thy
Launchbury/Denotational-Related.thy
Launchbury/ResourcedAdequacy.thy
Launchbury/SestoftNU.thy [deleted file]
Launchbury/Substitution.thy
Launchbury/Terms.thy

index 4540aaf..65c7c3c 100644 (file)
@@ -36,7 +36,7 @@ next
     by (rule HSem_restr_cong) (auto simp add: lookup_env_restr_eq)
   finally
   show ?case by simp
-qed
+qed auto
 
 sublocale has_ignore_fresh_ESem ESem
   by default (rule fv_supp_exp, rule ESem_considers_fv')
@@ -131,7 +131,7 @@ next
 case Cons
   from Cons(1,2)[OF Cons(3)] Cons(3)
   show ?case by auto
-qed
+qed auto
 
 lemma ESem_subst:
   assumes "x \<noteq> y"
index cfcc068..f4fc96f 100644 (file)
@@ -24,6 +24,8 @@ 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 (scrut ? e1 : e2) = \<bottom>"
 proof-
 txt {* The following proofs discharge technical obligations generated by the Nominal package. *}
 
@@ -55,8 +57,8 @@ case (goal4 x e x' e')
   qed
 next
 
-case (goal13 as body as' body')
-  from goal13(9)
+case (goal19 as body as' body')
+  from goal19(9)
   show ?case
   proof (rule eqvt_let_case)
     fix \<pi> :: perm
@@ -71,7 +73,7 @@ case (goal13 as body as' body')
       also have "(- \<pi> \<bullet> ESem_sumC) body = ESem_sumC body"
         by (rule eqvt_at_apply[OF `eqvt_at ESem_sumC body`])
       also have "has_ESem.HSem (- \<pi> \<bullet> ESem_sumC) as = has_ESem.HSem  ESem_sumC as"
-        by (rule HSem_cong[OF eqvt_at_apply[OF goal13(2)] refl])
+        by (rule HSem_cong[OF eqvt_at_apply[OF goal19(2)] refl])
       also have "- \<pi> \<bullet> \<rho> f|` fv (Let as body) = \<rho> f|` fv (Let as body)"
         by (rule env_restr_perm'[OF *], simp)
       finally have "ESem_sumC (\<pi> \<bullet> body)\<cdot>(has_ESem.HSem ESem_sumC (\<pi> \<bullet> as)\<cdot>(\<rho> f|` fv (Let as body))) = ESem_sumC body\<cdot>(has_ESem.HSem ESem_sumC as\<cdot>(\<rho> f|` fv (Let as body)))".
index 0aeb1e6..7391d5b 100644 (file)
@@ -37,6 +37,8 @@ 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 (scrut ? e1 : e2)  = (transform a scrut ? transform a e1 : transform a e2)"
 proof-
 case goal1
   note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] TransVar_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
@@ -58,8 +60,8 @@ case goal1
       done
     qed
   next
-case (goal8 a x e a' x' e')
-  from goal8(5)
+case (goal10 a x e a' x' e')
+  from goal10(5)
   have "a' = a" and  "Lam [x]. e = Lam [x']. e'" by simp_all
   from this(2)
   show ?case
@@ -69,7 +71,7 @@ case (goal8 a x e a' x' e')
 
     have "supp (TransLam a x (transform_sumC (PropLam a, e))) \<subseteq> supp (Lam [x]. e)"
       apply (rule subset_trans[OF SuppTransLam])
-      apply (auto simp add:  exp_assn.supp supp_Pair supp_at_base pure_supp exp_assn.fsupp dest!: set_mp[OF supp_eqvt_at[OF goal8(1)], rotated])
+      apply (auto simp add:  exp_assn.supp supp_Pair supp_at_base pure_supp exp_assn.fsupp dest!: set_mp[OF supp_eqvt_at[OF goal10(1)], rotated])
       done
     moreover
     assume "supp \<pi> \<sharp>* (Lam [x]. e)" 
@@ -82,7 +84,7 @@ case (goal8 a x e a' x' e')
         = TransLam a (\<pi> \<bullet> x) (transform_sumC (\<pi> \<bullet>  (PropLam a, e)))"
       by perm_simp rule
     also have "\<dots> = TransLam a (\<pi> \<bullet> x) (\<pi> \<bullet> transform_sumC (PropLam a, e))"
-      unfolding eqvt_at_apply'[OF goal8(1)]..
+      unfolding eqvt_at_apply'[OF goal10(1)]..
     also have "\<dots> = \<pi> \<bullet> (TransLam a x (transform_sumC (PropLam a, e)))"
       by simp
     also have "\<dots> = TransLam a x (transform_sumC (PropLam a, e))"
@@ -90,16 +92,16 @@ case (goal8 a x e a' x' e')
     finally show "TransLam a (\<pi> \<bullet> x) (transform_sumC (PropLam a, \<pi> \<bullet> e)) = TransLam a x (transform_sumC (PropLam a, e))" by simp
   qed
 next
-case (goal13 a as body a' as' body')
+case (goal19 a as body a' as' body')
   note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw]  AnalLet_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
 
-  from supp_eqvt_at[OF goal13(1)]
+  from supp_eqvt_at[OF goal19(1)]
   have "\<And> x e a. (x, e) \<in> set as \<Longrightarrow> supp (transform_sumC (a, e)) \<subseteq> supp e"
     by (auto simp add: exp_assn.fsupp supp_Pair pure_supp)
   hence supp_map: "\<And>ae. supp (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) ae as) \<subseteq> supp as"
     by (rule supp_map_transform_step)
 
-  from goal13(9)
+  from goal19(9)
   have "a' = a" and  "Terms.Let as body = Terms.Let as' body'" by simp_all
   from this(2)
   show ?case
@@ -107,7 +109,7 @@ case (goal13 a as body a' as' body')
   proof (rule eqvt_let_case)
     have "supp (TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))) \<subseteq> supp (Let as body)"
       by (auto simp add: Let_supp supp_Pair pure_supp exp_assn.fsupp
-               dest!: set_mp[OF supp_eqvt_at[OF goal13(2)], rotated] set_mp[OF SuppTransLet] set_mp[OF supp_map])
+               dest!: set_mp[OF supp_eqvt_at[OF goal19(2)], rotated] set_mp[OF SuppTransLet] set_mp[OF supp_map])
     moreover
     fix \<pi> :: perm
     assume "supp \<pi> \<sharp>* Terms.Let as body"
@@ -117,7 +119,7 @@ case (goal13 a as body a' as' body')
 
     have "TransLet (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a) (map_transform (\<lambda>x0 x1. (\<pi> \<bullet> transform_sumC) (x0, x1)) (PropLetHeap (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a)) (\<pi> \<bullet> as)) ((\<pi> \<bullet> transform_sumC) (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body)) = 
         \<pi> \<bullet> TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))"
-       by (simp del: Let_eq_iff Pair_eqvt add:  eqvt_at_apply[OF goal13(2)])
+       by (simp del: Let_eq_iff Pair_eqvt add:  eqvt_at_apply[OF goal19(2)])
     also have "\<dots> = TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))"
       by (rule perm_supp_eq[OF *])
     also
@@ -126,11 +128,11 @@ case (goal13 a as body a' as' body')
         apply (rule map_transform_fundef_cong[OF _ refl refl])
         apply (subst (asm) set_eqvt[symmetric])
         apply (subst (asm) mem_permute_set)
-        apply (auto simp add: permute_self  dest: eqvt_at_apply''[OF goal13(1)[where aa = "(- \<pi> \<bullet> a)" for a], where p = \<pi>, symmetric])
+        apply (auto simp add: permute_self  dest: eqvt_at_apply''[OF goal19(1)[where aa = "(- \<pi> \<bullet> a)" for a], where p = \<pi>, symmetric])
         done
     moreover
     have "(\<pi> \<bullet> transform_sumC) (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body) = transform_sumC (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body)"
-      using eqvt_at_apply''[OF goal13(2), where p = \<pi>] by perm_simp
+      using eqvt_at_apply''[OF goal19(2), where p = \<pi>] by perm_simp
     ultimately
     show "TransLet (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a)) (\<pi> \<bullet> as)) (transform_sumC (PropLetBody (AnalLet (\<pi> \<bullet> as) (\<pi> \<bullet> body) a), \<pi> \<bullet> body)) =
           TransLet (AnalLet as body a) (map_transform (\<lambda>x0 x1. transform_sumC (x0, x1)) (PropLetHeap (AnalLet as body a)) as) (transform_sumC (PropLetBody (AnalLet as body a), body))" by metis
index de47b6f..0efcc2f 100644 (file)
@@ -58,7 +58,7 @@ next
     apply (simp add: env_restr_join)
     done
   thus ?case using Let(1,2) by (auto simp add: fresh_star_Pair elim:env_restr_eq_subset[rotated])
-qed
+qed auto
 
 interpretation CorrectArityAnalysis Aexp
   by default (simp_all add:Aexp_restr_subst)
index eb790b1..ba7a2c7 100644 (file)
@@ -36,6 +36,8 @@ 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 (scrut ? e1 : e2) = \<bottom>"
 proof-
 case goal1
     note Afix_eqvt[eqvt]
@@ -48,8 +50,8 @@ case goal1
 next
 case goal3 thus ?case by (metis Terms.exp_strong_exhaust)
 next
-case (goal8 x e x' e')
-  from goal8(5)
+case (goal10 x e x' e')
+  from goal10(5)
   show ?case
   proof(rule eqvt_lam_case)
     fix \<pi> :: perm
@@ -59,16 +61,16 @@ case (goal8 x e x' e')
     have "Aexp_sumC (\<pi> \<bullet> e)\<cdot>(pred\<cdot>n)  f|` fv  (Lam [x]. e) = (-\<pi> \<bullet> Aexp_sumC (\<pi> \<bullet> e)\<cdot>(pred\<cdot>n)) f|` fv  (Lam [x]. e)"
       by (rule env_restr_perm[symmetric, OF *]) simp
     also have "\<dots> = ((Aexp_sumC e)\<cdot>(pred\<cdot>n)) f|` fv  (Lam [x]. e)"
-      by (simp add: eqvt_at_apply[OF goal8(1)] pemute_minus_self)
+      by (simp add: eqvt_at_apply[OF goal10(1)] pemute_minus_self)
     also note calculation
     }
     thus "(\<Lambda> n. Aexp_sumC (\<pi> \<bullet> e)\<cdot>(pred\<cdot>n) f|` fv (Lam [x]. e)) = (\<Lambda> n. Aexp_sumC e\<cdot>(pred\<cdot>n) f|` fv (Lam [x]. e))" by simp
   qed
 next
-case (goal13 as body as' body')
+case (goal19 as body as' body')
   note Afix_eqvt[eqvt]
 
-  from goal13(9)
+  from goal19(9)
   show ?case
   proof (rule eqvt_let_case)
     fix \<pi> :: perm
@@ -82,9 +84,9 @@ case (goal13 as body as' body')
                        Afix (- \<pi> \<bullet> Aexp_sumC) as\<cdot>((- \<pi> \<bullet> Aexp_sumC) body\<cdot>n \<squnion> thunks_AE as)"
         by (simp add: pemute_minus_self)
       also have "Afix (- \<pi> \<bullet> Aexp_sumC) as = Afix Aexp_sumC as"
-        by (rule Afix_cong[OF eqvt_at_apply[OF goal13(1)] refl])
+        by (rule Afix_cong[OF eqvt_at_apply[OF goal19(1)] refl])
       also have "(- \<pi> \<bullet> Aexp_sumC) body = Aexp_sumC body"
-        by (rule eqvt_at_apply[OF goal13(2)])
+        by (rule eqvt_at_apply[OF goal19(2)])
       also note calculation
     }
     thus "(\<Lambda> n. Afix Aexp_sumC (\<pi> \<bullet> as)\<cdot>(Aexp_sumC (\<pi> \<bullet> body)\<cdot>n \<squnion> thunks_AE (\<pi> \<bullet> as)) f|` fv (Terms.Let as body)) =
index 8990025..35760a8 100644 (file)
@@ -74,6 +74,8 @@ 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 (scrut ? e1 : e2) = \<bottom>"
 proof-
 case goal1
     show ?case
@@ -85,8 +87,8 @@ case goal1
 next
 case goal3 thus ?case by (metis Terms.exp_strong_exhaust)
 next
-case (goal8 x e x' e')
-  from goal8(9)
+case (goal10 x e x' e')
+  from goal10(9)
   show ?case
   proof(rule eqvt_lam_case)
     fix \<pi> :: perm
@@ -97,7 +99,7 @@ case (goal8 x e x' e')
        = combined_restrict (fv (Lam [x]. e)) (- \<pi> \<bullet> (fst (cCCexp_sumC (\<pi> \<bullet> e)\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC (\<pi> \<bullet> e)\<cdot>a))\<cdot>n))"
       by (rule combined_restrict_perm[symmetric, OF *]) simp
     also have "\<dots> = combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC e\<cdot>(pred\<cdot>n)), predCC (- \<pi> \<bullet> fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC e\<cdot>a))\<cdot>n)"
-      by (perm_simp, simp add: eqvt_at_apply[OF goal8(1)] pemute_minus_self Abs_cfun_eqvt)
+      by (perm_simp, simp add: eqvt_at_apply[OF goal10(1)] pemute_minus_self Abs_cfun_eqvt)
     also have "- \<pi> \<bullet> fv (Lam [x]. e) = (fv (Lam [x]. e) :: var set)" by (rule perm_supp_eq[OF *])
     also note calculation
     }
@@ -105,8 +107,8 @@ case (goal8 x e x' e')
         = (\<Lambda> n. combined_restrict (fv (Lam [x]. e)) (fst (cCCexp_sumC e\<cdot>(pred\<cdot>n)), predCC (fv (Lam [x]. e)) (\<Lambda> a. snd(cCCexp_sumC e\<cdot>a))\<cdot>n))" by simp
   qed
 next
-case (goal13 \<Gamma> body \<Gamma>' body')
-  from goal13(9)
+case (goal19 \<Gamma> body \<Gamma>' body')
+  from goal19(9)
   show ?case
   proof (rule eqvt_let_case)
     fix \<pi> :: perm
@@ -121,9 +123,9 @@ case (goal13 \<Gamma> body \<Gamma>' body')
         by (simp add: pemute_minus_self)
       also have "CoCallArityAnalysis.cccFix_choose (- \<pi> \<bullet> cCCexp_sumC) \<Gamma> = CoCallArityAnalysis.cccFix_choose cCCexp_sumC \<Gamma>"
         thm cccFix_cong
-        by (rule cccFix_choose_cong[OF eqvt_at_apply[OF goal13(1)] refl])
+        by (rule cccFix_choose_cong[OF eqvt_at_apply[OF goal19(1)] refl])
       also have "(- \<pi> \<bullet> cCCexp_sumC) body = cCCexp_sumC body"
-        by (rule eqvt_at_apply[OF goal13(2)])
+        by (rule eqvt_at_apply[OF goal19(2)])
       also note calculation
     }
     thus "(\<Lambda> n. combined_restrict (fv (Terms.Let \<Gamma> body)) (CoCallArityAnalysis.cccFix_choose cCCexp_sumC (\<pi> \<bullet> \<Gamma>)\<cdot>(cCCexp_sumC (\<pi> \<bullet> body)\<cdot>n))) =
@@ -143,6 +145,8 @@ 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 (scrut ? e1 : e2)\<cdot>n = \<bottom>"
 by (simp_all)
 declare cCCexp.simps[simp del]
 
@@ -153,6 +157,8 @@ 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 (scrut ? e1 : e2)\<cdot>n = \<bottom>"
  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq)+
 
 
@@ -163,6 +169,8 @@ 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 isLam e then {} else {x})) \<squnion> CCexp exp\<cdot>n)"
+  "CCexp Null\<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)+
 
 lemma ccField_CCexp:
index 9bd8587..98b077d 100644 (file)
@@ -183,7 +183,7 @@ next
 
   show "Aexp (let x' be e in exp )[y::=x]\<cdot>a f|` S = Aexp (let x' be e in exp )\<cdot>a f|` S"
     by (simp add: env_restr_join env_delete_env_restr_swap[symmetric] ABind_nonrec_eq)
-qed
+qed auto
    
 sublocale CorrectArityAnalysis Aexp
   by default (simp_all add:Aexp_restr_subst)
index 731422c..46b07ec 100644 (file)
@@ -11,6 +11,8 @@ 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 (scrut ? e1 : e2) = (remove_dead_code scrut ? remove_dead_code e1 : remove_dead_code e2)"
 proof-
 case goal1 thus ?case
   unfolding remove_dead_code_graph_aux_def eqvt_def 
@@ -37,13 +39,13 @@ case (goal4 x e x' e')
     finally show  "Lam [(\<pi> \<bullet> x)]. remove_dead_code_sumC (\<pi> \<bullet> e) = Lam [x]. remove_dead_code_sumC e".
   qed
 next
-case (goal13 as body as' body')
-  from goal13(13)
+case (goal19 as body as' body')
+  from goal19(13)
   show ?case
   proof (rule eqvt_let_case)
     fix \<pi> :: perm
   
-    from goal13(1,3) have eqvt_at1: "eqvt_at remove_dead_code_sumC body" by auto
+    from goal19(1,3) have eqvt_at1: "eqvt_at remove_dead_code_sumC body" by auto
 
     assume assm: "supp \<pi> \<sharp>* Let as body"
 
@@ -54,7 +56,7 @@ case (goal13 as body as' body')
         by (metis empty_eqvt permute_eq_iff inter_eqvt fv_eqvt domA)
     next
       assume "domA as \<inter> fv body \<noteq> {}"
-      from goal13(2)[OF this]
+      from goal19(2)[OF this]
       have eqvt_at2: "eqvt_at (map_ran (\<lambda>_. remove_dead_code_sumC)) as" by (induction as) (fastforce simp add: eqvt_at_def)+
 
       have *: "supp \<pi> \<sharp>* Let (map_ran (\<lambda>_. remove_dead_code_sumC) as) (remove_dead_code_sumC body)" using assm
index 5aebab1..87042b6 100644 (file)
@@ -92,6 +92,8 @@ 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 (scrut ? e1 : e2) = (remove_dead_code scrut ? remove_dead_code e1 : remove_dead_code e2)"
 proof-
 case goal1 thus ?case
   unfolding remove_dead_code_graph_aux_def eqvt_def 
@@ -118,14 +120,14 @@ case (goal4 x e x' e')
     finally show  "Lam [(\<pi> \<bullet> x)]. remove_dead_code_sumC (\<pi> \<bullet> e) = Lam [x]. remove_dead_code_sumC e".
   qed
 next
-case (goal13 as body as' body')
-  from goal13(13)
+case (goal19 as body as' body')
+  from goal19(13)
   show ?case
   proof (rule eqvt_let_case)
     fix \<pi> :: perm
   
-    from goal13(2) have eqvt_at1: "eqvt_at remove_dead_code_sumC body" by auto
-    from goal13(1)
+    from goal19(2) have eqvt_at1: "eqvt_at remove_dead_code_sumC body" by auto
+    from goal19(1)
     have eqvt_at2: "eqvt_at (map_ran (\<lambda>_. remove_dead_code_sumC)) as" by (induction as) (fastforce simp add: eqvt_at_def)+
 
     assume assm: "supp \<pi> \<sharp>* Terms.Let as body"
index 14e375a..241bf68 100644 (file)
@@ -54,7 +54,7 @@ next
   qed auto
   hence "\<lbrakk>e\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>\<rho>\<^esub> \<triangleleft>\<triangleright> (\<N>\<lbrakk>e\<rbrakk>\<^bsub>\<N>\<lbrace>as\<rbrace>\<sigma>\<^esub>)\<cdot>C\<^sup>\<infinity>" by (rule Let(2))
   thus ?case by simp
-qed
+qed auto
 
 corollary evalHeap_similar:
   "\<And>y z. y \<triangleleft>\<triangleright>\<^sup>* z \<Longrightarrow> \<^bold>\<lbrakk> \<Gamma> \<^bold>\<rbrakk>\<^bsub>y\<^esub> \<triangleleft>\<triangleright>\<^sup>* \<^bold>\<N>\<lbrakk> \<Gamma> \<^bold>\<rbrakk>\<^bsub>z\<^esub>"
index 5f5ea02..c0eeb94 100644 (file)
@@ -135,7 +135,7 @@ next
       unfolding CESem_simps
       by -(rule C_case_cong, simp)
   qed
-qed
+qed auto
 
 lemma can_restrict_env:
   "(\<N>\<lbrakk>e\<rbrakk>\<^bsub>\<rho>\<^esub>)\<cdot>r = (\<N>\<lbrakk> e \<rbrakk>\<^bsub>\<rho>|\<^sup>\<circ>\<^bsub>Cpred\<cdot>r\<^esub>\<^esub>)\<cdot>r"
@@ -252,6 +252,7 @@ proof(induction n arbitrary: \<Gamma> e S)
   thus ?case..
 next
   case (Suc n)
+  from Suc.prems
   show ?case
   proof(cases e rule:exp_strong_exhaust(1)[where c = "(\<Gamma>,S)", case_names Var App Let Lam])
   case (Var x)
@@ -332,7 +333,7 @@ next
     hence "\<Gamma> : Let as e' \<Down>\<^bsub>S\<^esub> \<Delta> : v"
       by (rule reds.Let[OF Let(1)])
     thus ?thesis using Let by auto
-  qed
+  qed auto
 qed
 
 theorem resourced_adequacy:
diff --git a/Launchbury/SestoftNU.thy b/Launchbury/SestoftNU.thy
deleted file mode 100644 (file)
index 21ca777..0000000
+++ /dev/null
@@ -1,101 +0,0 @@
-theory SestoftNU
-imports SestoftConf
-begin
-
-inductive step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightarrow>¹" 50) where
-  app\<^sub>1:  "(\<Gamma>, App e x, S) \<Rightarrow>¹ (\<Gamma>, e , Arg x # S)"
-| app\<^sub>2:  "(\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>¹ (\<Gamma>, e[y ::= x] , S)"
-| var\<^sub>1:  "map_of \<Gamma> x = Some e \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>¹ (delete x \<Gamma>, e , Upd x # S)"
-| var\<^sub>2:  "x \<notin> domA \<Gamma> \<Longrightarrow> isLam e \<Longrightarrow> (\<Gamma>, e, Upd x # S) \<Rightarrow>¹ ((x,e)# \<Gamma>, e , S)"
-| var\<^sub>3:  "map_of \<Gamma> x = Some e \<Longrightarrow> (\<Gamma>, Var1 x, S) \<Rightarrow>¹ (delete x \<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)"
-
-abbreviation steps (infix "\<Rightarrow>¹\<^sup>*" 50) where "steps \<equiv> step\<^sup>*\<^sup>*"
-
-lemma SmartLet_stepI:
-   "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> (\<Gamma>, SmartLet \<Delta> e, S) \<Rightarrow>¹\<^sup>*  (\<Delta>@\<Gamma>, e , S)"
-unfolding SmartLet_def by (auto intro: let\<^sub>1)
-
-lemma lambda_var: "map_of \<Gamma> x = Some e \<Longrightarrow> isLam e  \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>¹\<^sup>* ((x,e) # delete x \<Gamma>, e , S)"
-  by (rule rtranclp_trans[OF r_into_rtranclp r_into_rtranclp])
-     (auto intro: var\<^sub>1 var\<^sub>2)
-
-text {* An induction rule that skips the annoying case of a lambda taken off the heap *}
-
-lemma step_induction[consumes 2, case_names app\<^sub>1 app\<^sub>2 thunk lamvar var\<^sub>2 let\<^sub>1 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)"
-  assumes app\<^sub>2:  "\<And> \<Gamma> y e x S . P (\<Gamma>, Lam [y]. e, Arg x # S) (\<Gamma>, e[y ::= x] , S)"
-  assumes thunk:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e \<Longrightarrow> P (\<Gamma>, Var x, S) (delete x \<Gamma>, e , Upd x # S)"
-  assumes lamvar:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> isLam e \<Longrightarrow> P (\<Gamma>, Var x, S) ((x,e) # delete x \<Gamma>, e , S)"
-  assumes var\<^sub>2:  "\<And> \<Gamma> x e S . x \<notin> domA \<Gamma> \<Longrightarrow> isLam e \<Longrightarrow> P (\<Gamma>, e, Upd x # S) ((x,e)# \<Gamma>, e , S)"
-  assumes var1:  "\<And> \<Gamma> x e S .  map_of \<Gamma> x = Some e  \<Longrightarrow> P (\<Gamma>, Var1 x, S) (delete x \<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 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'"
-proof-
-  from assms(1)
-  have "P c c' \<or> (boring_step c' \<and> (\<forall> c''. c' \<Rightarrow>¹ c'' \<longrightarrow> P c c''))"
-  proof(induction)
-  case base
-    have "P c c" by (rule refl)
-    thus ?case..
-  next
-  case (step y z)
-    from step(3)
-    show ?case
-    proof
-      assume "P c y"
-
-      note t = trans[OF `c \<Rightarrow>¹\<^sup>* y` r_into_rtranclp[where r = step, OF `y \<Rightarrow>¹ z`]]
-      
-      from `y \<Rightarrow>¹ z`
-      show ?thesis
-      proof (cases)
-        case app\<^sub>1 hence "P y z" using assms(3) by metis
-        with `P c y` show ?thesis by (metis t)
-      next
-        case app\<^sub>2 hence "P y z" using assms(4) by metis
-        with `P c y` show ?thesis by (metis t)
-      next
-        case (var\<^sub>1 \<Gamma> x e S)
-        show ?thesis
-        proof (cases "isLam e")
-          case False with var\<^sub>1 have "P y z" using assms(5) by metis
-          with `P c y` show ?thesis by (metis t)
-        next
-          case True
-          have *: "y \<Rightarrow>¹\<^sup>* ((x,e) # delete x \<Gamma>, e , S)" using var\<^sub>1 True lambda_var by metis
-
-          have "boring_step (delete x \<Gamma>, e, Upd x # S)" using True ..
-          moreover
-          have "P y ((x,e) # delete x \<Gamma>, e , S)" using var\<^sub>1 True assms(6) by metis
-          with `P c y` have "P c ((x,e) # delete x \<Gamma>, e , S)" by (rule trans[OF `c \<Rightarrow>¹\<^sup>* y` *])
-          ultimately
-          show ?thesis using var\<^sub>1(2,3) True by (auto elim!: step.cases)
-        qed
-      next
-        case var\<^sub>2 hence "P y z" using assms(7) by metis
-        with `P c y` show ?thesis by (metis t)
-      next
-        case var\<^sub>3 hence "P y z" using assms(8) by metis
-        with `P c y` show ?thesis by (metis t)
-      next
-        case let\<^sub>1 hence "P y z" using assms(9) by metis
-        with `P c y` show ?thesis by (metis t)
-      qed
-    next
-      assume "boring_step y \<and> (\<forall>c''. y \<Rightarrow>¹ c'' \<longrightarrow> P c c'')"
-      with `y \<Rightarrow>¹ z`
-      have "P c z" by blast
-      thus ?thesis..
-    qed
-  qed
-  with assms(2)
-  show ?thesis by auto
-qed
-
-
-end
index 264b69e..3079f47 100644 (file)
@@ -17,6 +17,8 @@ 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"
+ |"(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])"
 proof-
@@ -55,6 +57,16 @@ have eqvt_at_subst: "\<And> e y z . eqvt_at subst_subst_heap_sumC (Inl (e, y, z)
   apply (rule the1_equality)
   apply blast 
   apply(simp (no_asm) only: sum.sel)
+  apply(rule_tac x="Sum_Type.projl x" in exI)
+  apply(clarify)
+  apply (rule the1_equality)
+  apply blast 
+  apply(simp (no_asm) only: sum.sel)
+  apply(rule_tac x="Sum_Type.projl x" in exI)
+  apply(clarify)
+  apply (rule the1_equality)
+  apply blast 
+  apply(simp (no_asm) only: sum.sel)
   apply (metis Inr_not_Inl)
   apply (metis Inr_not_Inl)
   apply(simp)
@@ -125,7 +137,7 @@ next case (goal3 P x) show ?case
   qed
 qed
 
-next case (goal15 e y2 z2 as e2 y z as2) thus ?case
+next case (goal19 e y2 z2 as e2 y z as2) thus ?case
   apply -
   apply (drule eqvt_at_subst)+
   apply (drule eqvt_at_subst_heap)+
@@ -146,7 +158,7 @@ next case (goal15 e y2 z2 as e2 y z as2) thus ?case
   apply (simp add: eqvt_at_def)
   done
 
-next case (goal19 x2 y2 z2 e2 x y z e) thus ?case
+next case (goal25 x2 y2 z2 e2 x y z e) thus ?case
   apply -
   apply (drule eqvt_at_subst)+
   apply (simp only: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
index 58c95aa..411ae3a 100644 (file)
@@ -15,11 +15,15 @@ and redo the various lemmas in terms of that, so that afterwards, the type @{tex
 referenced.
 *}
 
+term If
+
 nominal_datatype exp =
   Var var
 | 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
+| IfThenElse exp exp exp  ("((_)/ ? (_)/ : (_))" [0, 0, 10] 10)
 and assn =
   ANil | ACons var exp assn
 binder
@@ -152,6 +156,10 @@ 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"
+  "(scrut ? e1 : e2) \<noteq> Let \<Gamma> e"
+  "Let \<Gamma> e \<noteq> (scrut ? e1 : e2)"
   unfolding Let_def by simp_all
 
 lemma Let_perm_simps[simp,eqvt]:
@@ -183,27 +191,33 @@ lemma Let_eq_iff[simp]:
 
 lemma exp_strong_exhaust:
   fixes c :: "'a :: fs"
-  assumes "(\<And>var. y = Var var \<Longrightarrow> P)"
+  assumes "\<And>var. y = Var var \<Longrightarrow> P"
   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> scrut e1 e2. y = (scrut ? e1 : e2) \<Longrightarrow> P"
   shows P
   apply (rule  exp_assn.strong_exhaust(1)[where y = y and c = c])
   apply (metis assms(1))
   apply (metis assms(2))
   apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap)
   apply (metis assms(4))
+  apply (metis assms(5))
+  apply (metis assms(6))
   done
 
 text {*
 And finally the induction rules with @{term Let}.
 *}
 
-lemma exp_heap_induct[case_names Var App Let Lam Nil Cons]:
+lemma exp_heap_induct[case_names Var App Let Lam Null 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> 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>)"
   shows "P1 e" and "P2 \<Gamma>"
@@ -214,17 +228,21 @@ proof-
     apply (metis assms(2))
     apply (metis assms(3) Let_def heapToAssn_asToHeap )
     apply (metis assms(4))
-    apply (metis assms(5) asToHeap.simps(1))
-    apply (metis assms(6) asToHeap.simps(2))
+    apply (metis assms(5))
+    apply (metis assms(6))
+    apply (metis assms(7) asToHeap.simps(1))
+    apply (metis assms(8) asToHeap.simps(2))
     done
   thus "P1 e" and "P2 \<Gamma>" unfolding asToHeap_heapToAssn.
 qed
 
-lemma exp_heap_strong_induct[case_names Var App Let Lam Nil Cons]:
+lemma exp_heap_strong_induct[case_names Var App Let Lam Null 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> 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>)"
   fixes c :: "'a :: fs"
@@ -236,8 +254,10 @@ proof-
     apply (metis assms(2))
     apply (metis assms(3) set_bn_to_atom_domA Let_def heapToAssn_asToHeap )
     apply (metis assms(4))
-    apply (metis assms(5) asToHeap.simps(1))
-    apply (metis assms(6) asToHeap.simps(2))
+    apply (metis assms(5))
+    apply (metis assms(6))
+    apply (metis assms(7) asToHeap.simps(1))
+    apply (metis assms(8) asToHeap.simps(2))
     done
   thus "P1 c e" and "P2 c \<Gamma>" unfolding asToHeap_heapToAssn.
 qed
@@ -249,48 +269,60 @@ 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]:
+lemma exp_induct[case_names Var App Let Lam  Null 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> scrut e1 e2. P scrut \<Longrightarrow> P e1 \<Longrightarrow> P e2 \<Longrightarrow> P (scrut ? e1 : e2)"
   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))
   apply (metis assms(3))
   apply (metis assms(4))
+  apply (metis assms(5))
+  apply (metis assms(6))
   apply auto
   done
 
-lemma  exp_strong_induct_set[case_names Var App Let Lam]:
+lemma  exp_strong_induct_set[case_names Var App Let Lam Null 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)"
   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))
   apply (metis assms(2))
   apply (metis assms(3) split_conv)
   apply (metis assms(4))
+  apply (metis assms(5))
+  apply (metis assms(6))
   apply auto
   done
 
 
-lemma  exp_strong_induct[case_names Var App Let Lam]:
+lemma  exp_strong_induct[case_names Var App Let Lam Null 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> 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)))"])
   apply (metis assms(1))
   apply (metis assms(2))
   apply (metis assms(3))
   apply (metis assms(4))
+  apply (metis assms(5))
+  apply (metis assms(6))
   apply auto
   done
 
@@ -329,6 +361,10 @@ 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_IfThenElse[simp]: "fv (scrut ? e1 : e2)  = fv scrut \<union> fv e1 \<union> fv e2"
+  unfolding fv_def by (auto simp add: exp_assn.supp)
 
 lemma finite_fv_exp[simp]: "finite (fv (e::exp) :: var set)"
   and finite_fv_heap[simp]: "finite (fv (\<Gamma> :: heap) :: var set)"
@@ -459,7 +495,9 @@ nominal_function isLam :: "exp \<Rightarrow> bool" where
   "isLam (Var x) = False" |
   "isLam (Lam [x]. e) = True" |
   "isLam (App e x) = False" |
-  "isLam (Let as e) = False"
+  "isLam (Let as e) = False" |
+  "isLam Null = False" |
+  "isLam (scrut ? e1 : e2) = False"
   unfolding isLam_graph_aux_def eqvt_def
   apply simp
   apply simp
@@ -525,12 +563,14 @@ 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]:
+lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam Null 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>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> 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])
   apply (metis assms(1))
@@ -541,15 +581,19 @@ lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam]:
   apply (metis assms(4))
   apply (metis assms(3))
   apply (metis assms(5))
+  apply (metis assms(6))
+  apply (metis assms(7))
   done
 
-lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam]:
+lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam Null 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> 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])
   apply (metis assms(1))
@@ -560,15 +604,19 @@ lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam]:
   apply (metis assms(4))
   apply (metis assms(3))
   apply (metis assms(5))
+  apply (metis assms(6))
+  apply (metis assms(7))
   done
 
-lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam]:
+lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam Null 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> 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])
   apply (metis assms(1))
@@ -579,6 +627,8 @@ lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam]:
   apply (metis assms(4))
   apply (metis assms(3))
   apply (metis assms(5))
+  apply (metis assms(6))
+  apply (metis assms(7))
   done