Get rid of GVar detour
authorJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 12:37:50 +0000 (12:37 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 12:37:50 +0000 (12:37 +0000)
13 files changed:
Launchbury/Abstract-Denotational-Props.thy
Launchbury/AbstractDenotational.thy
Launchbury/AbstractTransform.thy
Launchbury/ArityAnalysisPreImpl.thy
Launchbury/CoCallAnalysisImpl.thy
Launchbury/DeadCodeRemoval.thy
Launchbury/DeadCodeRemoval2.thy
Launchbury/Denotational-Related.thy
Launchbury/Denotational.thy
Launchbury/ResourcedAdequacy.thy
Launchbury/ResourcedDenotational.thy
Launchbury/Substitution.thy
Launchbury/Terms.thy

index b1d0404..4540aaf 100644 (file)
@@ -74,7 +74,7 @@ proof-
     by (rule ESem_fresh_cong) (auto simp add: lookup_env_restr_eq)
   finally show ?thesis.
 qed
-declare ESem.simps(5)[simp del]
+declare ESem.simps(4)[simp del]
 
 
 subsubsection {* Denotation of Substitution *}
index 999a4ba..cfcc068 100644 (file)
@@ -23,8 +23,6 @@ where
      resource and makes the adequacy proof difficult. *)
 | "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 (Var1 x) = \<bottom>"
-  (* Restrict \<rho> to avoid having to demand set (bn as) \<sharp>* \<rho> *)
 | "ESem (Let as body) = (\<Lambda> \<rho>. tick \<cdot> (ESem body \<cdot> (has_ESem.HSem ESem as \<cdot>  (\<rho> f|` fv (Let as body)))))"
 proof-
 txt {* The following proofs discharge technical obligations generated by the Nominal package. *}
@@ -57,8 +55,8 @@ case (goal4 x e x' e')
   qed
 next
 
-case (goal18 as body as' body')
-  from goal18(9)
+case (goal13 as body as' body')
+  from goal13(9)
   show ?case
   proof (rule eqvt_let_case)
     fix \<pi> :: perm
@@ -73,7 +71,7 @@ case (goal18 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 goal18(2)] refl])
+        by (rule HSem_cong[OF eqvt_at_apply[OF goal13(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 e1eac67..0aeb1e6 100644 (file)
@@ -20,12 +20,10 @@ locale AbstractAnalPropSubst = AbstractAnalProp +
 locale AbstractTransform = AbstractAnalProp +
   constrains AnalLet :: "heap \<Rightarrow> exp \<Rightarrow> 'a::pure_cont_pt \<Rightarrow> 'b::cont_pt"
   fixes TransVar :: "'a \<Rightarrow> var \<Rightarrow> exp"
-  fixes TransVar1 :: "'a \<Rightarrow> var \<Rightarrow> exp"
   fixes TransApp :: "'a \<Rightarrow> exp \<Rightarrow> var \<Rightarrow> exp"
   fixes TransLam :: "'a \<Rightarrow> var \<Rightarrow> exp \<Rightarrow> exp"
   fixes TransLet :: "'b \<Rightarrow> heap \<Rightarrow> exp \<Rightarrow> exp"
   assumes TransVar_eqvt: "\<pi> \<bullet> TransVar = TransVar"
-  assumes TransVar1_eqvt: "\<pi> \<bullet> TransVar1 = TransVar1"
   assumes TransApp_eqvt: "\<pi> \<bullet> TransApp = TransApp"
   assumes TransLam_eqvt: "\<pi> \<bullet> TransLam = TransLam"
   assumes TransLet_eqvt: "\<pi> \<bullet> TransLet = TransLet"
@@ -36,13 +34,12 @@ begin
     "transform a (App e x) = TransApp a (transform (PropApp a) e) x"
   | "transform a (Lam [x]. e) = TransLam a x (transform (PropLam a) e)"
   | "transform a (Var x) = TransVar a x"
-  | "transform a (Var1 x) = TransVar1 a x"
   | "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)"
 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] TransVar1_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
+  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]
   show ?case
   unfolding eqvt_def transform_graph_aux_def
     apply rule
@@ -61,8 +58,8 @@ case goal1
       done
     qed
   next
-case (goal9 a x e a' x' e')
-  from goal9(5)
+case (goal8 a x e a' x' e')
+  from goal8(5)
   have "a' = a" and  "Lam [x]. e = Lam [x']. e'" by simp_all
   from this(2)
   show ?case
@@ -72,20 +69,20 @@ case (goal9 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 goal9(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 goal8(1)], rotated])
       done
     moreover
     assume "supp \<pi> \<sharp>* (Lam [x]. e)" 
     ultimately
     have *: "supp \<pi> \<sharp>* TransLam a x (transform_sumC (PropLam a, e))" by (auto simp add: fresh_star_def fresh_def)
 
-    note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt] TransVar1_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
+    note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt] TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
 
     have "TransLam a (\<pi> \<bullet> x) (transform_sumC (PropLam a, \<pi> \<bullet> 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 goal9(1)]..
+      unfolding eqvt_at_apply'[OF goal8(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))"
@@ -93,16 +90,16 @@ case (goal9 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 (goal18 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] TransVar1_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
+case (goal13 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 goal18(1)]
+  from supp_eqvt_at[OF goal13(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 goal18(9)
+  from goal13(9)
   have "a' = a" and  "Terms.Let as body = Terms.Let as' body'" by simp_all
   from this(2)
   show ?case
@@ -110,7 +107,7 @@ case (goal18 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 goal18(2)], rotated] set_mp[OF SuppTransLet] set_mp[OF supp_map])
+               dest!: set_mp[OF supp_eqvt_at[OF goal13(2)], rotated] set_mp[OF SuppTransLet] set_mp[OF supp_map])
     moreover
     fix \<pi> :: perm
     assume "supp \<pi> \<sharp>* Terms.Let as body"
@@ -120,7 +117,7 @@ case (goal18 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 goal18(2)])
+       by (simp del: Let_eq_iff Pair_eqvt add:  eqvt_at_apply[OF goal13(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
@@ -129,11 +126,11 @@ case (goal18 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 goal18(1)[where aa = "(- \<pi> \<bullet> a)" for a], where p = \<pi>, symmetric])
+        apply (auto simp add: permute_self  dest: eqvt_at_apply''[OF goal13(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 goal18(2), where p = \<pi>] by perm_simp
+      using eqvt_at_apply''[OF goal13(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
@@ -144,7 +141,6 @@ end
 
 locale AbstractTransformSubst = AbstractTransform + AbstractAnalPropSubst +
   assumes TransVar_subst: "(TransVar a v)[x ::= y] = (TransVar a v[x ::v= y])"
-  assumes TransVar1_subst: "(TransVar1 a v)[x ::= y] = (TransVar1 a v[x ::v= y])"
   assumes TransApp_subst: "(TransApp a e v)[x ::= y] = (TransApp a e[x ::= y] v[x ::v= y])"
   assumes TransLam_subst: "atom v \<sharp> (x,y) \<Longrightarrow> (TransLam a v e)[x ::= y] = (TransLam a v[x ::v= y] e[x ::= y])"
   assumes TransLet_subst: "atom ` domA \<Gamma> \<sharp>* (x,y) \<Longrightarrow> (TransLet b \<Gamma> e)[x ::= y] = (TransLet b \<Gamma>[x ::h= y] e[x ::= y])"
@@ -161,7 +157,7 @@ begin
     apply (rule subst_map_transform)
     apply simp
     done
-  qed (case_tac b, simp_all add: TransVar_subst TransVar1_subst TransApp_subst TransLam_subst)
+  qed (simp_all add: TransVar_subst TransApp_subst TransLam_subst)
 end
 
 
@@ -175,7 +171,6 @@ locale AbstractTransformBound = AbstractAnalProp + supp_bounded_transform  +
 begin
   sublocale AbstractTransform PropApp PropLam AnalLet PropLetBody PropLetHeap
       "(\<lambda> a. Var)"
-      "(\<lambda> a. Var1)"
       "(\<lambda> a. App)"
       "(\<lambda> a. Terms.Lam)"
       "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeapTrans b) \<Gamma>) e)"
@@ -184,7 +179,7 @@ begin
   case goal1
   show ?case
   apply default
-  apply ((perm_simp, rule)+)[5]
+  apply ((perm_simp, rule)+)[4]
   apply (auto simp add: exp_assn.supp supp_at_base)[1]
   apply (auto simp add: Let_supp supp_Pair supp_at_base dest: set_mp[OF supp_map_transform])[1]
   done
@@ -192,7 +187,7 @@ begin
 
   lemma isLam_transform[simp]:
     "isLam (transform a e) \<longleftrightarrow> isLam e"
-    by (induction e rule:isLam.induct) (case_tac b, auto)
+    by (induction e rule:isLam.induct) auto
 end
 
 locale AbstractTransformBoundSubst = AbstractAnalPropSubst + AbstractTransformBound + 
@@ -200,7 +195,6 @@ locale AbstractTransformBoundSubst = AbstractAnalPropSubst + AbstractTransformBo
 begin
   sublocale AbstractTransformSubst PropApp PropLam AnalLet PropLetBody PropLetHeap
       "(\<lambda> a. Var)"
-      "(\<lambda> a. Var1)"
       "(\<lambda> a. App)"
       "(\<lambda> a. Terms.Lam)"
       "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeapTrans b) \<Gamma>) e)"
@@ -209,7 +203,7 @@ begin
   case goal1
   show ?case
   apply default
-  apply simp_all[4]
+  apply simp_all[3]
   apply (simp del: Let_eq_iff)
   apply (rule arg_cong[where f = "\<lambda> x. Let x y" for y])
   apply (rule subst_map_transform)
index 597e7c5..eb790b1 100644 (file)
@@ -32,7 +32,7 @@ begin
 nominal_function
   Aexp :: "exp \<Rightarrow> (Arity \<rightarrow> AEnv)"
 where
-  "Aexp (GVar b x) = (\<Lambda> n . esing x \<cdot> (up \<cdot> n))"
+  "Aexp (Var x) = (\<Lambda> n . esing x\<cdot>(up\<cdot>n))"
 | "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)))"
index a825548..8990025 100644 (file)
@@ -70,7 +70,7 @@ lemma cc_restr_predCC'[simp]:
 nominal_function
   cCCexp :: "exp \<Rightarrow> (Arity \<rightarrow> AEnv \<times> CoCalls)" 
 where
-  "cCCexp (GVar b x) =   (\<Lambda> n . (esing x \<cdot> (up \<cdot> n),                                   \<bottom>))"
+  "cCCexp (Var x) =      (\<Lambda> n . (esing x \<cdot> (up \<cdot> n),                                   \<bottom>))"
 | "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)))"
@@ -139,7 +139,7 @@ sublocale CoCallArityAnalysis cCCexp.
 sublocale ArityAnalysis Aexp.
 
 lemma cCCexp_eq[simp]:
-  "cCCexp (GVar b x)\<cdot>n =   (esing x \<cdot> (up \<cdot> n),                                   \<bottom>)"
+  "cCCexp (Var x)\<cdot>n =      (esing x \<cdot> (up \<cdot> n),                                   \<bottom>)"
   "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))"
@@ -148,7 +148,7 @@ declare cCCexp.simps[simp del]
 
 
 lemma Aexp_simps[simp]:
-  "Aexp (GVar b x)\<cdot>n = esing x\<cdot>(up\<cdot>n)"
+  "Aexp (Var x)\<cdot>n = esing x\<cdot>(up\<cdot>n)"
   "Aexp (Lam [x]. e)\<cdot>n = Aexp e\<cdot>(pred\<cdot>n) f|` fv (Lam [x]. e)"
   "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))"
@@ -157,7 +157,7 @@ lemma Aexp_simps[simp]:
 
 
 lemma CCexp_simps[simp]:
-  "CCexp (GVar b x)\<cdot>n = \<bottom>"
+  "CCexp (Var x)\<cdot>n = \<bottom>"
   "CCexp (Lam [x]. e)\<cdot>n = predCC (fv (Lam [x]. e)) (CCexp e)\<cdot>n"
   "CCexp (App e x)\<cdot>n = CCexp e\<cdot>(inc\<cdot>n) \<squnion> ccProd {x} (insert x (fv e))"
   "\<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))"
index 0cf2c1f..731422c 100644 (file)
@@ -7,7 +7,7 @@ nominal_function
 where
   "remove_dead_code (Lam [x]. e) = Lam [x]. remove_dead_code e"
 | "remove_dead_code (App e x) = App (remove_dead_code e) x"
-| "remove_dead_code (GVar b x) = GVar b x"
+| "remove_dead_code (Var x) = Var x"
 | "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))"
index 477346e..5aebab1 100644 (file)
@@ -90,7 +90,7 @@ nominal_function
 where
   "remove_dead_code (Lam [x]. e) = Lam [x]. remove_dead_code e"
 | "remove_dead_code (App e x) = App (remove_dead_code e) x"
-| "remove_dead_code (GVar b x) = GVar b 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)"
 proof-
 case goal1 thus ?case
index a4e06f1..14e375a 100644 (file)
@@ -13,15 +13,9 @@ theorem denotational_semantics_similar:
   shows "\<lbrakk>e\<rbrakk>\<^bsub>\<rho>\<^esub> \<triangleleft>\<triangleright> (\<N>\<lbrakk>e\<rbrakk>\<^bsub>\<sigma>\<^esub>)\<cdot>C\<^sup>\<infinity>"
 using assms
 proof(induct e arbitrary: \<rho> \<sigma> rule:exp_induct)
-  case (Var b v)
-  show ?case
-  proof(cases b)
-    case False hence "b = False" by simp
-    from Var have "\<rho> v \<triangleleft>\<triangleright> (\<sigma> v)\<cdot>C\<^sup>\<infinity>" by cases auto
-    thus ?thesis unfolding `b = False` by simp
-  next
-    case True thus ?thesis by simp
-  qed
+  case (Var v)
+  from Var have "\<rho> v \<triangleleft>\<triangleright> (\<sigma> v)\<cdot>C\<^sup>\<infinity>" by cases auto
+  thus ?case by simp
 next
   case (Lam v e)
   { fix x y
index d419ea7..6054ada 100644 (file)
@@ -18,7 +18,7 @@ lemma ESem_simps_as_defined:
   "\<lbrakk> App e x \<rbrakk>\<^bsub>\<rho>\<^esub>    =  \<lbrakk> e \<rbrakk>\<^bsub>\<rho>\<^esub> \<down>Fn \<rho> x"
   "\<lbrakk> Var x \<rbrakk>\<^bsub>\<rho>\<^esub>      =  \<rho>  x"
   "\<lbrakk> Let as body \<rbrakk>\<^bsub>\<rho>\<^esub> = \<lbrakk>body\<rbrakk>\<^bsub>\<lbrace>as\<rbrace>(\<rho> f|` fv (Let as body))\<^esub>"
-  by (simp_all del: ESem_Lam ESem_Let add: ESem.simps(1,5) )
+  by (simp_all del: ESem_Lam ESem_Let add: ESem.simps(1,4) )
 
 lemma ESem_simps:
   "\<lbrakk> Lam [x]. e \<rbrakk>\<^bsub>\<rho>\<^esub> =  Fn\<cdot>(\<Lambda> v. \<lbrakk> e \<rbrakk>\<^bsub>\<rho>(x := v)\<^esub>)"
index a8ea303..5f5ea02 100644 (file)
@@ -17,28 +17,21 @@ environment with less resources.
 
 lemma restr_can_restrict_env: "(\<N>\<lbrakk> e \<rbrakk>\<^bsub>\<rho>\<^esub>)|\<^bsub>r\<^esub> = (\<N>\<lbrakk> e \<rbrakk>\<^bsub>\<rho>|\<^sup>\<circ>\<^bsub>Cpred\<cdot>r\<^esub>\<^esub>)|\<^bsub>r\<^esub>"
 proof(induction e arbitrary: \<rho> r rule: exp_induct)
-  case (Var x)
+  case (Var x)
   show ?case
-  proof(cases b)
-    case True
-    thus ?thesis by simp
-  next
-    case False hence "b = False" by simp
-    show ?thesis unfolding `b = False`
-    proof(rule C_restr_cong)
-      fix r'
-      assume "r' \<sqsubseteq> r"
-      {
-        fix r''
-        assume "r' = C\<cdot>r''" with `r' \<sqsubseteq> r`
-        have "(Cpred\<cdot>r \<sqinter> r'') = r''"
-          by (metis Cpred.simps below_refl is_meetI monofun_cfun_arg)
-        hence "\<rho> x\<cdot>r'' = (\<rho> x|\<^bsub>Cpred\<cdot>r\<^esub>)\<cdot>r''" by simp
-      }
-      thus "(\<N>\<lbrakk> Var x \<rbrakk>\<^bsub>\<rho>\<^esub>)\<cdot>r' = (\<N>\<lbrakk> Var x \<rbrakk>\<^bsub>\<rho>|\<^sup>\<circ>\<^bsub>Cpred\<cdot>r\<^esub>\<^esub>)\<cdot>r'"
-        unfolding CESem_simps
-        by -(rule C_case_cong, simp)
-    qed
+  proof(rule C_restr_cong)
+    fix r'
+    assume "r' \<sqsubseteq> r"
+    {
+      fix r''
+      assume "r' = C\<cdot>r''" with `r' \<sqsubseteq> r`
+      have "(Cpred\<cdot>r \<sqinter> r'') = r''"
+        by (metis Cpred.simps below_refl is_meetI monofun_cfun_arg)
+      hence "\<rho> x\<cdot>r'' = (\<rho> x|\<^bsub>Cpred\<cdot>r\<^esub>)\<cdot>r''" by simp
+    }
+    thus "(\<N>\<lbrakk> Var x \<rbrakk>\<^bsub>\<rho>\<^esub>)\<cdot>r' = (\<N>\<lbrakk> Var x \<rbrakk>\<^bsub>\<rho>|\<^sup>\<circ>\<^bsub>Cpred\<cdot>r\<^esub>\<^esub>)\<cdot>r'"
+      unfolding CESem_simps
+      by -(rule C_case_cong, simp)
   qed
 next
   case (Lam x e)
@@ -261,30 +254,21 @@ next
   case (Suc n)
   show ?case
   proof(cases e rule:exp_strong_exhaust(1)[where c = "(\<Gamma>,S)", case_names Var App Let Lam])
-  case (Var b x)
-    show ?thesis
-    proof(cases b)
-    case False hence "b = False" by simp
-      let ?e = "the (map_of \<Gamma> x)"
-      from Suc.prems[unfolded Var `b = False`]
-      have "x \<in> domA \<Gamma>" 
-        by (auto intro: ccontr simp add: lookup_HSem_other)
-      hence "map_of \<Gamma> x = Some ?e" by (rule domA_map_of_Some_the)
-      moreover
-      from Suc.prems[unfolded Var `b = False`] `map_of \<Gamma> x = Some ?e` `x \<in> domA \<Gamma>`
-      have "(\<N>\<lbrakk>?e\<rbrakk>\<^bsub>\<N>\<lbrace>\<Gamma>\<rbrace>\<^esub>)\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>" by (auto simp add: lookup_HSem_heap  simp del: app_strict)
-      hence "(\<N>\<lbrakk>?e\<rbrakk>\<^bsub>\<N>\<lbrace>delete x \<Gamma>\<rbrace>\<^esub>)\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>" by (rule add_BH[OF `map_of \<Gamma> x = Some ?e`])
-      from Suc.IH[OF this]
-      obtain \<Delta> v where "delete x \<Gamma> : ?e \<Down>\<^bsub>x # S\<^esub> \<Delta> : v" by blast
-      ultimately
-      have "\<Gamma> : (Var x) \<Down>\<^bsub>S\<^esub> (x,v) #  \<Delta> : v" by (rule Variable)
-      thus ?thesis using Var `b = False` by auto
-    next
-    case True
-      hence "b = True" by simp
-      from Suc.prems[unfolded Var `b = True`] have False by simp
-      thus ?thesis..
-  qed
+  case (Var x)
+    let ?e = "the (map_of \<Gamma> x)"
+    from Suc.prems[unfolded Var]
+    have "x \<in> domA \<Gamma>" 
+      by (auto intro: ccontr simp add: lookup_HSem_other)
+    hence "map_of \<Gamma> x = Some ?e" by (rule domA_map_of_Some_the)
+    moreover
+    from Suc.prems[unfolded Var] `map_of \<Gamma> x = Some ?e` `x \<in> domA \<Gamma>`
+    have "(\<N>\<lbrakk>?e\<rbrakk>\<^bsub>\<N>\<lbrace>\<Gamma>\<rbrace>\<^esub>)\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>" by (auto simp add: lookup_HSem_heap  simp del: app_strict)
+    hence "(\<N>\<lbrakk>?e\<rbrakk>\<^bsub>\<N>\<lbrace>delete x \<Gamma>\<rbrace>\<^esub>)\<cdot>C\<^bsup>n\<^esup> \<noteq> \<bottom>" by (rule add_BH[OF `map_of \<Gamma> x = Some ?e`])
+    from Suc.IH[OF this]
+    obtain \<Delta> v where "delete x \<Gamma> : ?e \<Down>\<^bsub>x # S\<^esub> \<Delta> : v" by blast
+    ultimately
+    have "\<Gamma> : (Var x) \<Down>\<^bsub>S\<^esub> (x,v) #  \<Delta> : v" by (rule Variable)
+    thus ?thesis using Var by auto
   next
   case (App e' x)
     have "finite (set S \<union> fv (\<Gamma>, e'))" by simp
index 32b9792..8caeece 100644 (file)
@@ -22,14 +22,11 @@ lemma CESem_simps:
   "\<N>\<lbrakk> Lam [x]. e \<rbrakk>\<^bsub>\<rho>\<^esub>  = (\<Lambda> (C\<cdot>r). CFn\<cdot>(\<Lambda> v. (\<N>\<lbrakk> e \<rbrakk>\<^bsub>\<rho>(x := v|\<^bsub>r\<^esub>)\<^esub>)|\<^bsub>r\<^esub>))"
   "\<N>\<lbrakk> App e x \<rbrakk>\<^bsub>\<rho>\<^esub>     = (\<Lambda> (C\<cdot>r). ((\<N>\<lbrakk> e \<rbrakk>\<^bsub>\<rho>\<^esub>)\<cdot>r \<down>CFn \<rho> x|\<^bsub>r\<^esub>)\<cdot>r)"
   "\<N>\<lbrakk> Var x \<rbrakk>\<^bsub>\<rho>\<^esub>       = (\<Lambda> (C\<cdot>r). (\<rho>  x) \<cdot> r)"
-  "\<N>\<lbrakk> Var1 x \<rbrakk>\<^bsub>\<rho>\<^esub>      = \<bottom>"
   "\<N>\<lbrakk> Let as body \<rbrakk>\<^bsub>\<rho>\<^esub> = (\<Lambda> (C \<cdot> r). (\<N>\<lbrakk>body\<rbrakk>\<^bsub>\<N>\<lbrace>as\<rbrace>\<rho>\<^esub>) \<cdot> r)"
   by (auto simp add: eta_cfun)
 
 lemma CESem_bot[simp]:"(\<N>\<lbrakk> e \<rbrakk>\<^bsub>\<sigma>\<^esub>)\<cdot>\<bottom> = \<bottom>"
-  apply (nominal_induct e arbitrary: \<sigma> rule: exp_strong_induct)
-  apply (case_tac b)
-  by auto
+  by (nominal_induct e arbitrary: \<sigma> rule: exp_strong_induct) auto
 
 lemma CHSem_bot[simp]:"((\<N>\<lbrace> \<Gamma> \<rbrace>) x)\<cdot>\<bottom> = \<bottom>"
   by (cases "x \<in> domA \<Gamma>") (auto simp add: lookup_HSem_heap lookup_HSem_other)
index bd55b02..264b69e 100644 (file)
@@ -13,7 +13,7 @@ nominal_function  (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. In
 and
   subst_heap :: "heap \<Rightarrow> var \<Rightarrow> var \<Rightarrow> heap" ("_[_::h=_]" [1000,100,100] 1000)
 where
-  "(GVar b x)[y ::= z] = GVar b (x[y ::v= z])"
+  "(Var x)[y ::= z] = Var (x[y ::v= z])"
  |"(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])"
index ea6fb08..58c95aa 100644 (file)
@@ -16,7 +16,7 @@ referenced.
 *}
 
 nominal_datatype exp =
-  GVar bool var
+  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)
@@ -26,9 +26,6 @@ binder
   bn :: "assn \<Rightarrow> atom list"
 where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"
 
-abbreviation Var where "Var == GVar False"
-abbreviation Var1 where "Var1 == GVar True"
-
 notation (latex output) Terms.Var ("_")
 notation (latex output) Terms.App ("_ _")
 notation (latex output) Terms.Lam ("\<lambda>_. _"  [100, 100] 100)
@@ -149,8 +146,8 @@ lemma size_Let[simp]: "size (Let \<Gamma> e) = size_list (\<lambda>p. size (snd
   unfolding Let_def by (auto simp add: split_beta')
 
 lemma Let_distinct[simp]:
-  "GVar s v \<noteq> Let \<Gamma> e"
-  "Let \<Gamma> e \<noteq> GVar s v"
+  "Var v \<noteq> Let \<Gamma> e"
+  "Let \<Gamma> e \<noteq> Var v"
   "App e v \<noteq> Let \<Gamma> e'"
   "Lam [v]. e' \<noteq> Let \<Gamma> e"
   "Let \<Gamma> e \<noteq> Lam [v]. e'"
@@ -186,7 +183,7 @@ lemma Let_eq_iff[simp]:
 
 lemma exp_strong_exhaust:
   fixes c :: "'a :: fs"
-  assumes "(\<And>bool var. y = GVar bool 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"
@@ -203,7 +200,7 @@ And finally the induction rules with @{term Let}.
 *}
 
 lemma exp_heap_induct[case_names Var App Let Lam Nil Cons]:
-  assumes "\<And>b var. P1 (GVar b var)"
+  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)"
@@ -224,7 +221,7 @@ proof-
 qed
 
 lemma exp_heap_strong_induct[case_names Var App Let Lam Nil Cons]:
-  assumes "\<And>b var c. P1 c (GVar b var)"
+  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)"
@@ -253,7 +250,7 @@ goal for @{typ assn}.
 *}
 
 lemma exp_induct[case_names Var App Let Lam]:
-  assumes "\<And>b var. P (GVar b var)"
+  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)"
@@ -267,7 +264,7 @@ lemma exp_induct[case_names Var App Let Lam]:
   done
 
 lemma  exp_strong_induct_set[case_names Var App Let Lam]:
-  assumes "\<And>b var c. P c (GVar b var)"
+  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)"
@@ -283,7 +280,7 @@ lemma  exp_strong_induct_set[case_names Var App Let Lam]:
 
 
 lemma  exp_strong_induct[case_names Var App Let Lam]:
-  assumes "\<And>b var c. P c (GVar b var)"
+  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)"
@@ -326,7 +323,7 @@ lemma fv_supp_heap: "supp (\<Gamma>::heap) = atom ` (fv \<Gamma> :: var set)"
 
 lemma fv_Lam[simp]: "fv (Lam [x]. e) = fv e - {x}"
   unfolding fv_def by (auto simp add: exp_assn.supp)
-lemma fv_Var[simp]: "fv (GVar b x) = {x}"
+lemma fv_Var[simp]: "fv (Var x) = {x}"
   unfolding fv_def by (auto simp add: exp_assn.supp supp_at_base pure_supp)
 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)
@@ -459,7 +456,7 @@ lemma fv_SmartLet[simp]: "fv (SmartLet \<Gamma> e) = (fv \<Gamma> \<union> fv e)
 subsubsection {* A predicate for value expressions *}
 
 nominal_function isLam :: "exp \<Rightarrow> bool" where
-  "isLam (GVar b x) = False" |
+  "isLam (Var x) = False" |
   "isLam (Lam [x]. e) = True" |
   "isLam (App e x) = False" |
   "isLam (Let as e) = False"
@@ -529,7 +526,7 @@ lemma nonrec_eqvt[eqvt]:
   by (erule nonrecE) (auto simp add: nonrec_def)
 
 lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam]:
-  assumes "\<And>b var. P (GVar b var)"
+  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)"
@@ -547,7 +544,7 @@ lemma exp_induct_rec[case_names Var App Let Let_nonrec Lam]:
   done
 
 lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam]:
-  assumes "\<And>b var c. P c (GVar b var)"
+  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)"
@@ -566,7 +563,7 @@ lemma  exp_strong_induct_rec[case_names Var App Let Let_nonrec Lam]:
   done
 
 lemma  exp_strong_induct_rec_set[case_names Var App Let Let_nonrec Lam]:
-  assumes "\<And>b var c. P c (GVar b var)"
+  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)"