Fix end-to-end proof to finally obtain the unmodified semantics
authorJoachim Breitner <mail@joachim-breitner.de>
Wed, 28 Jan 2015 13:02:12 +0000 (13:02 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Wed, 28 Jan 2015 13:02:12 +0000 (13:02 +0000)
Launchbury/AbstractTransform.thy
Launchbury/Arity.thy
Launchbury/ArityConsistent.thy
Launchbury/ArityEtaExpandCorrect.thy
Launchbury/ArityStack.thy
Launchbury/CallArityCorrectEnd2End.thy
Launchbury/CardinalityEtaExpandCorrect.thy
Launchbury/Nominal-Utils.thy
Launchbury/Sestoft.thy
Launchbury/SestoftConf.thy
Launchbury/SestoftGC.thy

index b99432c..c48a9f5 100644 (file)
@@ -141,6 +141,22 @@ case (goal19 a as body a' as' body')
     qed
   qed auto
   nominal_termination by lexicographic_order
+
+  lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
+  proof-
+    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]
+    note transform.eqvt[eqvt]
+    show ?thesis
+      apply (rule supp_fun_app_eqvt)
+      apply (rule eqvtI)
+      apply perm_simp
+      apply (rule reflexive)
+      done
+   qed
+
+  lemma fv_transform: "fv (transform a e) \<subseteq> fv e"
+    unfolding fv_def by (auto dest: set_mp[OF supp_transform])
+
 end
 
 locale AbstractTransformSubst = AbstractTransform + AbstractAnalPropSubst +
@@ -197,6 +213,7 @@ begin
   lemma isVal_transform[simp]:
     "isVal (transform a e) \<longleftrightarrow> isVal e"
     by (induction e rule:isLam.induct) auto
+
 end
 
 locale AbstractTransformBoundSubst = AbstractAnalPropSubst + AbstractTransformBound + 
index 811d339..4371b97 100644 (file)
@@ -116,7 +116,9 @@ lift_definition one_Arity :: Arity is 1.
 instance ..
 end
 
-
+lemma one_is_inc_zero: "1 = inc\<cdot>0"
+  by (simp add: inc_def, transfer, simp)
+  
 lemma Arity_ind:  "P 0 \<Longrightarrow> (\<And> n. P n \<Longrightarrow> P (inc\<cdot>n)) \<Longrightarrow> P n"
   apply (simp add: inc_def)
   apply transfer
index f9e9ffe..41eba9f 100644 (file)
@@ -20,7 +20,6 @@ inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"
 inductive a_consistent :: "astate \<Rightarrow> conf \<Rightarrow> bool" where
   a_consistentI:
   "edom ae \<subseteq> domA \<Gamma> \<union> upds S
-  \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
   \<Longrightarrow> Astack S \<sqsubseteq> a
   \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae
   \<Longrightarrow> stack_consistent as S
@@ -49,9 +48,6 @@ lemma a_consistent_stackD:
   "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> Astack S \<sqsubseteq> a"
   by (rule a_consistentE)
 
-lemma a_consistent_heap_upds_okD:
-  "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)"
-  by (rule a_consistentE)
 
 lemma a_consistent_app\<^sub>1:
   "a_consistent (ae, a, as) (\<Gamma>, App e x, S) \<Longrightarrow> a_consistent (ae, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
@@ -107,6 +103,7 @@ lemma a_consistent_thunk_once:
   assumes "a_consistent (ae, a, as) (\<Gamma>, Var x, S)"
   assumes "map_of \<Gamma> x = Some e"
   assumes [simp]: "ae x = up\<cdot>u"
+  assumes "heap_upds_ok (\<Gamma>, S)"
   shows "a_consistent (env_delete x ae, u, as) (delete x \<Gamma>, e, S)"
 proof-
   from assms(2)
@@ -118,7 +115,7 @@ proof-
   from below_trans[OF Aexp_Var this]
   have "a \<sqsubseteq> u" by simp
 
-  from assms(1)
+  from `heap_upds_ok (\<Gamma>, S)`
   have "x \<notin> upds S" by (auto simp add: a_consistent.simps elim!: heap_upds_okE)
   hence [simp]: "(- {x} \<inter> (domA \<Gamma> \<union> upds S)) = (domA \<Gamma> - {x} \<union> upds S)" by auto
 
index 7015e82..76fab58 100644 (file)
@@ -64,11 +64,11 @@ begin
   by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
 
   lemma foo:
-    fixes c c' R 
-    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,a,as) c"
+    fixes c c'
+    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "heap_upds_ok_conf c" and "consistent (ae,a,as) c"
     shows "\<exists>ae' a' as'. consistent (ae',a',as') c' \<and> a_transform (ae,a,as) c \<Rightarrow>\<^sup>* a_transform (ae',a',as') c'"
-  using assms
-  proof(induction c c' arbitrary: ae a as rule:step_induction)
+  using assms(1,2) heap_upds_ok_invariant assms(3-)
+  proof(induction c c' arbitrary: ae a as rule:step_invariant_induction)
   case (app\<^sub>1 \<Gamma> e x S)
     from app\<^sub>1 have "consistent (ae, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
       by (auto intro: a_consistent_app\<^sub>1)
@@ -90,7 +90,8 @@ begin
     hence "x \<in> thunks \<Gamma>" by auto
     hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
 
-    have "x \<notin> upds S" using thunk by (auto dest!: a_consistent_heap_upds_okD  heap_upds_okE)
+    from `heap_upds_ok_conf (\<Gamma>, Var x, S)`
+    have "x \<notin> upds S"  by (auto dest!: heap_upds_okE)
     
     have "x \<in> edom ae" using thunk by auto
     have "ae x = up\<cdot>0" using thunk `x \<in> thunks \<Gamma>` by (auto)
@@ -152,15 +153,13 @@ begin
     ultimately show ?case by (blast del: consistentI consistentE)
   next
   case (var\<^sub>2 \<Gamma> x e S)
-    have "x \<in> edom ae" using var\<^sub>2 by (auto simp add: a_consistent.simps env_restr_join join_below_iff)
-
     from var\<^sub>2
     have "a_consistent (ae, a, as) (\<Gamma>, e, Upd x # S)" by auto
-    from a_consistent_UpdD[OF this  `x \<in> edom ae`]
+    from a_consistent_UpdD[OF this]
     have "ae x = up\<cdot>0" and "a = 0".
 
     have "a_consistent (ae, a, as) ((x, e) # \<Gamma>, e, S)"
-      using var\<^sub>2 `x \<in> edom ae` by (auto intro!: a_consistent_var\<^sub>2)
+      using var\<^sub>2 by (auto intro!: a_consistent_var\<^sub>2)
     hence "consistent (ae, 0, as) ((x, e) # \<Gamma>, e, S)"
       using var\<^sub>2 `a = 0`
       by (auto simp add: thunks_Cons elim: below_trans)
index ef80f50..eeeadb5 100644 (file)
@@ -13,5 +13,13 @@ lemma Astack_restr_stack_below:
   "Astack (restr_stack V S) \<sqsubseteq> Astack S"
   by (induction V S rule: restr_stack.induct) auto
 
+lemma Astack_map_Dummy[simp]:
+  "Astack (map Dummy l) = 0"
+by (induction l) auto
+
+lemma Astack_append_map_Dummy[simp]:
+  "Astack S' = 0 \<Longrightarrow> Astack (S @ S') = Astack S"
+by (induction S rule: Astack.induct) auto
+
 
 end
index e58e3fc..83db917 100644 (file)
@@ -10,6 +10,7 @@ sublocale CallArityEnd2End.
 lemma end2end:
   "c \<Rightarrow>\<^sup>* c' \<Longrightarrow>
   \<not> boring_step c' \<Longrightarrow>
+  heap_upds_ok_conf c \<Longrightarrow>
   consistent (ae, ce, a, as, r) c \<Longrightarrow>
   \<exists>ae' ce' a' as' r'. consistent  (ae', ce', a', as', r') c' \<and> conf_transform  (ae, ce, a, as, r) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform  (ae', ce', a', as', r') c'"
   by (rule foo)
@@ -24,6 +25,8 @@ proof-
   moreover
   have "\<not> boring_step (\<Gamma>,v,[])" by (simp add: boring_step.simps)
   moreover
+  have "heap_upds_ok_conf ([], e, [])" by simp
+  moreover
   have "consistent (\<bottom>,\<bottom>,0,[],[]) ([], e, [])" using closed by (rule closed_consistent)
   ultimately
   obtain ae ce a as r where
@@ -36,27 +39,34 @@ proof-
 
   from * have "set r \<subseteq> domA \<Gamma>" by auto
 
-  have "conf_transform  (\<bottom>, \<bottom>, 0, [], []) ([],e,[]) = ([], [],transform 0 e,[])" by simp
+  have "conf_transform  (\<bottom>, \<bottom>, 0, [], []) ([],e,[]) = ([],transform 0 e,[])" by simp
   with **
-  have "([], [], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (r, ?\<Gamma>, ?v, [])" by simp
+  have "([], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (?\<Gamma>, ?v, map Dummy (rev r))" by simp
 
   have "isVal ?v" using `isVal v` by simp
 
-  note sestoftUnGC'[OF `([], [], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (r, ?\<Gamma>, ?v, [])` `isVal ?v`]
-  then obtain \<Gamma>' where "([], transform 0 e, []) \<Rightarrow>\<^sup>* (\<Gamma>', ?v, [])" and "?\<Gamma> = restrictA (- set r) \<Gamma>'" and "set r \<subseteq> domA \<Gamma>'" by auto
+  have "fv (transform 0 e) = ({} :: var set)" using closed
+    by (auto dest: set_mp[OF fv_transform])
+
+  note sestoftUnGC'[OF `([], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (?\<Gamma>, ?v, map Dummy (rev r))` `isVal ?v` `fv (transform 0 e) = {}`]
+  then obtain \<Gamma>'
+    where "([], transform 0 e, []) \<Rightarrow>\<^sup>* (\<Gamma>', ?v, [])"
+    and "?\<Gamma> = restrictA (- set r) \<Gamma>'"
+    and "set r \<subseteq> domA \<Gamma>'"
+    by auto
 
   have "card (domA \<Gamma>) = card (domA ?\<Gamma> \<union> (set r \<inter> domA \<Gamma>))"
     by (rule arg_cong[where f = card]) auto
   also have "\<dots> = card (domA ?\<Gamma>) + card (set r \<inter> domA \<Gamma>)"
     by (rule card_Un_disjoint) auto
-  also have "set r \<inter> domA \<Gamma> = set r \<inter> domA \<Gamma>'"
-    using `set r \<subseteq> domA \<Gamma>` `set r \<subseteq> domA \<Gamma>'` by auto
   also note `?\<Gamma> = restrictA (- set r) \<Gamma>'`
+  also have "set r \<inter> domA \<Gamma> = set r \<inter> domA \<Gamma>'"
+    using `set r \<subseteq> domA \<Gamma>`  `set r \<subseteq> domA \<Gamma>'` by auto
   also have "card (domA (restrictA (- set r) \<Gamma>')) + card (set r \<inter> domA \<Gamma>') = card (domA \<Gamma>')"
     by (subst card_Un_disjoint[symmetric]) (auto intro: arg_cong[where f = card])
   finally
   have "card (domA \<Gamma>) = card (domA \<Gamma>')".
-  with `([], transform 0 e, []) \<Rightarrow>\<^sup>* (\<Gamma>', ?v, [])` `isVal ?v`
+  with `([], transform 0 e, []) \<Rightarrow>\<^sup>* (\<Gamma>', ?v, [])`  `isVal ?v`
   show ?thesis by blast
 qed
 
@@ -109,22 +119,20 @@ proof-
   have [simp]: "Aheap [(x, e)] (Var x)\<cdot>1 = esing x\<cdot>(up\<cdot>1)"
     by (simp add: env_restr_join disj)
 
-  have 1: "1 = inc\<cdot>0" apply (simp add: inc_def) apply transfer apply simp done
-  
   have [simp]: "Aeta_expand 1 (App (Var f) g) = (Lam [z]. App (App (Var f) g) z)"
-    apply (simp add: 1 del: exp_assn.eq_iff)
+    apply (simp add: one_is_inc_zero del: exp_assn.eq_iff)
     apply (subst change_Lam_Variable[of z "fresh_var (App (Var f) g)"])
     apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
     done
 
   have [simp]: "Aeta_expand 1 e = (Lam [z]. App e z)"
-    apply (simp add: 1 del: exp_assn.eq_iff)
+    apply (simp add: one_is_inc_zero del: exp_assn.eq_iff)
     apply (subst change_Lam_Variable[of z "fresh_var e"])
     apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj fresh intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
     done
 
   show ?thesis
-    by (simp del: Let_eq_iff add: map_transform_Cons map_transform_Nil disj[symmetric])
+    by (simp del: Let_eq_iff add: map_transform_Cons disj[symmetric])
 qed
 
 
index 6226fab..4b02bd0 100644 (file)
@@ -53,8 +53,11 @@ begin
   fun restr_conf :: "var set \<Rightarrow> conf \<Rightarrow> conf"
     where "restr_conf V (\<Gamma>, e, S) = (restrictA V \<Gamma>, e, restr_stack V S)"
 
-  fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> (var list \<times> conf)"
-  where "conf_transform (ae, ce, a, as, r) c = (r, a_transform (ae, a, as) (restr_conf (- set r) c))"
+  fun add_dummies_conf :: "var list \<Rightarrow> conf \<Rightarrow> conf"
+    where "add_dummies_conf l (\<Gamma>, e, S) = (\<Gamma>, e, S @ map Dummy (rev l))"
+
+  fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
+  where "conf_transform (ae, ce, a, as, r) c = add_dummies_conf r ((a_transform (ae, a, as) (restr_conf (- set r) c)))"
 
   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
     consistentI[intro!]: 
@@ -81,10 +84,10 @@ begin
 
   lemma foo:
     fixes c c'
-    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a,as,r) c"
+    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "heap_upds_ok_conf c" and "consistent (ae,ce,a,as,r) c"
     shows "\<exists>ae' ce' a' as' r'. consistent (ae',ce',a',as',r') c' \<and> conf_transform (ae,ce,a,as,r) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae',ce',a',as',r') c'"
-  using assms
-  proof(induction c c' arbitrary: ae ce a as r rule:step_induction)
+  using assms(1,2) heap_upds_ok_invariant assms(3-)
+  proof(induction c c' arbitrary: ae ce a as r rule:step_invariant_induction)
   case (app\<^sub>1 \<Gamma> e x S)
     have "prognosis ae as (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae as a (\<Gamma>, App e x, S)" by (rule prognosis_App)
     with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a, as, r) (\<Gamma>, e, Arg x # S)"
@@ -115,7 +118,8 @@ begin
     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
     hence [simp]: "x \<notin> set r" using thunk by auto
 
-    have "x \<notin> upds S" using thunk by (auto dest!: a_consistent_heap_upds_okD  heap_upds_okE)
+    from `heap_upds_ok_conf (\<Gamma>, Var x, S)`
+    have "x \<notin> upds S" by (auto dest!:  heap_upds_okE)
 
     have "x \<in> edom ae" using thunk by auto
     then obtain u where "ae x = up\<cdot>u" by (cases "ae x") (auto simp add: edom_def)
@@ -166,21 +170,24 @@ begin
       moreover
 
       from *
-      have "Astack (transform_alts as (restr_stack (- set r) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
+      have **: "Astack (transform_alts as (restr_stack (- set r) S) @ map Dummy (rev r) @ [Dummy x]) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
       
       {
       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` once
       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
         by (simp add: map_of_map_transform)
       hence "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G
-             (r, delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (- set r) S))"
+             add_dummies_conf r (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (- set r) S))"
           by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist simp del: restr_delete)
       also
-      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (x # r, delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (- set r) S))"
-        by (rule r_into_rtranclp, rule)
+      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* add_dummies_conf (x # r) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (- set r) S))"
+        apply (rule r_into_rtranclp)
+        apply (simp add: append_assoc[symmetric] del: append_assoc)
+        apply (rule dropUpd)
+        done
       also
-      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (x # r, delete x (map_transform Aeta_expand ae (map_transform ccTransform ae  (restrictA (- set r) \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (- set r) S))"
-        by (intro normal_trans Aeta_expand_correct `Astack (transform_alts as (restr_stack (- set r) S)) \<sqsubseteq> u`)
+      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* add_dummies_conf (x # r) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae  (restrictA (- set r) \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (- set r) S))"
+        by simp (intro  normal_trans Aeta_expand_correct **)
       also(rtranclp_trans)
       have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u, as, x # r) (delete x \<Gamma>, e, Upd x # S)" 
         by (auto intro!: map_transform_cong simp add:  map_transform_delete[symmetric]  restr_delete_twist Compl_insert)
@@ -218,7 +225,7 @@ begin
         by (simp add: map_of_map_transform)
       with `\<not> isVal e`
       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as, r) (delete x \<Gamma>, e, Upd x # S)"
-        by (auto simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
+        by (auto intro: gc_step.intros simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
       ultimately
       show ?thesis by (blast del: consistentI consistentE)
     qed
@@ -253,8 +260,8 @@ begin
     moreover
 
     from `a_consistent _ _`
-    have "Astack (transform_alts as (restr_stack (- set r) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
-  
+    have **: "Astack (transform_alts as (restr_stack (- set r) S) @ map Dummy (rev r)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD) 
+
     {
     from `isVal e`
     have "isVal (transform u e)" by simp
@@ -265,17 +272,17 @@ begin
       by (simp add: map_of_map_transform)
     ultimately
     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>*
-          (r, (x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (transform u e), transform_alts as (restr_stack (- set r) S))"
+          add_dummies_conf r ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae (restrictA (- set r) \<Gamma>))), Aeta_expand u (transform u e), transform_alts as (restr_stack (- set r) S))"
        by (auto intro!: normal_trans[OF lambda_var] simp add: map_transform_delete simp del: restr_delete)
-    also have "\<dots> = (r, (map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x (restrictA (- set r) \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (- set r) S))"
+    also have "\<dots> = add_dummies_conf r ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x (restrictA (- set r) \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (- set r) S))"
       using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
       by (simp add: map_transform_Cons map_transform_delete restr_delete_twist del: restr_delete)
     also(subst[rotated]) have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, u, as, r) ((x, e) # delete x \<Gamma>, e, S)"
-      by (simp add: restr_delete_twist) (rule normal_trans[OF Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`]])
+      by (simp add: restr_delete_twist) (rule normal_trans[OF Aeta_expand_correct[OF ** ]])
     finally(rtranclp_trans)
     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, u, as, r) ((x, e) # delete x \<Gamma>, e, S)".
     }
-    ultimately show ?case by (blast intro: normal_trans del: consistentI consistentE)
+    ultimately show ?case by (blast del: consistentI consistentE)
   next
   case (var\<^sub>2 \<Gamma> x e S)
     show ?case
@@ -300,7 +307,7 @@ begin
       moreover
       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as, r) ((x, e) # \<Gamma>, e, S)"
         using `ae x = up\<cdot>0` `a = 0` var\<^sub>2 
-        by (auto intro!: step.intros simp add: map_transform_Cons)
+        by (auto intro: gc_step.intros simp add: map_transform_Cons)
       ultimately show ?thesis by (blast del: consistentI consistentE)
     next
       case False[simp]
@@ -357,7 +364,7 @@ begin
 
     {
     have "edom (?ae \<squnion> ae) = edom (?ce \<squnion> ce)"
-      using let\<^sub>1(3) by (auto simp add: edom_cHeap)
+      using let\<^sub>1(4) by (auto simp add: edom_cHeap)
     moreover
     { fix x e'
       assume "x \<in> thunks \<Gamma>"
@@ -417,19 +424,30 @@ begin
   
       from `edom ae \<subseteq> domA \<Gamma> \<union> upds S` `edom ce = edom ae`
       have "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ce" and  "\<And> x. x \<in> domA \<Delta> \<Longrightarrow> x \<notin> edom ae"
-         using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)] 
-         by (auto dest!:  set_mp[OF ups_fv_subset])
+         using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_ups[OF let\<^sub>1(2)]  by auto
       hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (- set r) \<Delta>))
          = map_transform Aeta_expand ?ae (map_transform transform ?ae (restrictA (- set r) \<Delta>))"
          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
+      moreover
+            
+      from  `domA \<Delta> \<inter> domA \<Gamma> = {}`   `domA \<Delta> \<inter> upds S = {}`
+      have "atom ` domA \<Delta> \<sharp>* set r"
+        by (auto simp add: fresh_star_def fresh_at_base fresh_finite_set_at_base dest!: set_mp[OF `set r \<subseteq> domA \<Gamma> \<union> upds S`])
+      hence "atom ` domA \<Delta> \<sharp>* map Dummy (rev r)" 
+        apply -
+        apply (rule eqvt_fresh_star_cong1[where f = "map Dummy"], perm_simp, rule)
+        apply (rule eqvt_fresh_star_cong1[where f = "rev"], perm_simp, rule)
+        apply (auto simp add: fresh_star_def fresh_set)
+        done
       ultimately
       
       
       have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G conf_transform (?ae \<squnion> ae, ?ce \<squnion> ce, a, as, r) (\<Delta> @ \<Gamma>, e, S)"
-        using restr_stack_simp2 let\<^sub>1(1,2) `edom ce = edom ae`
+        using restr_stack_simp2 let\<^sub>1(1,2)  `edom ce = edom ae`
         apply (auto simp add: map_transform_append restrictA_append edom_cHeap restr_stack_simp2[simplified] )
-        apply (rule normal[OF  step.let\<^sub>1])
-        apply (auto dest: set_mp[OF edom_Aheap])
+        apply (rule normal)
+        apply (rule step.let\<^sub>1)
+        apply (auto intro: normal step.let\<^sub>1 dest: set_mp[OF edom_Aheap] simp add: fresh_star_list)
         done
     }
     ultimately
@@ -461,7 +479,7 @@ begin
     }
     moreover
     have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, a', as', r) (\<Gamma>, if b then e1 else e2, S)"
-      by (auto intro:normal  step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
+      by (auto intro: normal step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
index b71aa72..897bec6 100644 (file)
@@ -222,6 +222,10 @@ lemma override_on_eqvt[eqvt]:
   "\<pi> \<bullet> (override_on m1 m2 S) = override_on (\<pi> \<bullet> m1) (\<pi> \<bullet> m2) (\<pi> \<bullet> S)"
   by (auto simp add: override_on_def )
 
+lemma card_eqvt[eqvt]:
+  "\<pi> \<bullet> (card S) = card (\<pi> \<bullet> S)"
+by (cases "finite S", induct rule: finite_induct) (auto simp add: card_insert_if mem_permute_iff permute_pure)
+
 (* Helper lemmas provided by Christian Urban *)
 
 lemma Projl_permute:
index ab3c640..21b3fb9 100644 (file)
@@ -21,34 +21,51 @@ lemma lambda_var: "map_of \<Gamma> x = Some e \<Longrightarrow> isVal e  \<Longr
   by (rule rtranclp_trans[OF r_into_rtranclp r_into_rtranclp])
      (auto intro: var\<^sub>1 var\<^sub>2)
 
+lemma let\<^sub>1_closed:
+  assumes "closed (\<Gamma>, Let \<Delta> e, S)"
+  assumes "domA \<Delta> \<inter> domA \<Gamma> = {}"
+  assumes "domA \<Delta> \<inter> upds S = {}"
+  shows "(\<Gamma>, Let \<Delta> e, S) \<Rightarrow> (\<Delta>@\<Gamma>, e , S)"
+proof
+  from `domA \<Delta> \<inter> domA \<Gamma> = {}` and `domA \<Delta> \<inter> upds S = {}`
+  have "domA \<Delta> \<inter> (domA \<Gamma> \<union> upds S) = {}" by auto
+  with `closed _`
+  have "domA \<Delta> \<inter> fv (\<Gamma>, S) = {}" by auto
+  hence "atom ` domA \<Delta> \<sharp>* (\<Gamma>, S)"
+    by (auto simp add: fresh_star_def fv_def fresh_def)
+  thus "atom` domA \<Delta> \<sharp>* \<Gamma>" and "atom ` domA \<Delta> \<sharp>* S" by (auto simp add: fresh_star_Pair)
+qed
+  
 text {* An induction rule that skips the annoying case of a lambda taken off the heap *}
 
 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>2 refl trans]:
+lemma step_invariant_induction[consumes 4, 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)"
-  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> isVal 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> isVal 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> 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>2:   "\<And>\<Gamma> b e1 e2 S. P (\<Gamma>, Bool b, Alts e1 e2 # S) (\<Gamma>, if b then e1 else e2, S)"
+  assumes "invariant op \<Rightarrow> I"
+  assumes "I c"
+  assumes app\<^sub>1:  "\<And> \<Gamma> e x S . I (\<Gamma>, App e x, S) \<Longrightarrow> P (\<Gamma>, App e x, S)  (\<Gamma>, e , Arg x # S)"
+  assumes app\<^sub>2:  "\<And> \<Gamma> y e x S . I (\<Gamma>, Lam [y]. e, Arg x # S) \<Longrightarrow> 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> isVal e \<Longrightarrow> I (\<Gamma>, Var x, S) \<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> isVal e \<Longrightarrow> I (\<Gamma>, Var x, S) \<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> isVal e \<Longrightarrow> I (\<Gamma>, e, Upd x # S) \<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> I (\<Gamma>, Let \<Delta> e, S) \<Longrightarrow> P (\<Gamma>, Let \<Delta> e, S) (\<Delta>@\<Gamma>, e, S)"
+  assumes if\<^sub>1:   "\<And>\<Gamma> scrut e1 e2 S. I  (\<Gamma>, scrut ? e1 : e2, S) \<Longrightarrow> P (\<Gamma>, scrut ? e1 : e2, S) (\<Gamma>, scrut, Alts e1 e2 # S)"
+  assumes if\<^sub>2:   "\<And>\<Gamma> b e1 e2 S. I  (\<Gamma>, Bool b, Alts e1 e2 # S) \<Longrightarrow> 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'"
 proof-
-  from assms(1)
+  from assms(1,3,4)
   have "P c c' \<or> (boring_step c' \<and> (\<forall> c''. c' \<Rightarrow> c'' \<longrightarrow> P c c''))"
-  proof(induction)
+  proof(induction rule: rtranclp_invariant_induct)
   case base
     have "P c c" by (rule refl)
     thus ?case..
   next
   case (step y z)
-    from step(3)
+    from step(5)
     show ?case
     proof
       assume "P c y"
@@ -58,16 +75,16 @@ proof-
       from `y \<Rightarrow> z`
       show ?thesis
       proof (cases)
-        case app\<^sub>1 hence "P y z" using assms(3) by metis
+        case app\<^sub>1 hence "P y z" using assms(5) `I y` 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
+        case app\<^sub>2 hence "P y z" using assms(6) `I y` by metis
         with `P c y` show ?thesis by (metis t)
       next
         case (var\<^sub>1 \<Gamma> x e S)
         show ?thesis
         proof (cases "isVal e")
-          case False with var\<^sub>1 have "P y z" using assms(5) by metis
+          case False with var\<^sub>1 have "P y z" using assms(7) `I y` by metis
           with `P c y` show ?thesis by (metis t)
         next
           case True
@@ -75,22 +92,22 @@ proof-
 
           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
+          have "P y ((x,e) # delete x \<Gamma>, e , S)" using var\<^sub>1 True assms(8) `I y` 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
+        case var\<^sub>2 hence "P y z" using assms(9) `I y` by metis
         with `P c y` show ?thesis by (metis t)
       next
-        case let\<^sub>1 hence "P y z" using assms(8) by metis
+        case let\<^sub>1 hence "P y z" using assms(10) `I y` by metis
         with `P c y` show ?thesis by (metis t)
       next
-        case if\<^sub>1 hence "P y z" using assms(9) by metis
+        case if\<^sub>1 hence "P y z" using assms(11) `I y` by metis
         with `P c y` show ?thesis by (metis t)
       next
-        case if\<^sub>2 hence "P y z" using assms(10) by metis
+        case if\<^sub>2 hence "P y z" using assms(12) `I y` by metis
         with `P c y` show ?thesis by (metis t)
       qed
     next
@@ -105,5 +122,58 @@ proof-
 qed
 
 
+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)"
+  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> isVal 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> isVal 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> 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>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'"
+by (rule step_invariant_induction[OF _ _ invariant_True, simplified, OF assms])
+
+subsubsection {* Equivariance *}
+
+lemma step_eqvt[eqvt]: "step x y \<Longrightarrow> step (\<pi> \<bullet> x) (\<pi> \<bullet> y)"
+  apply (induction  rule: step.induct)
+  apply (perm_simp, rule step.intros)
+  apply (perm_simp, rule step.intros)
+  apply (perm_simp, rule step.intros)
+  apply (rule permute_boolE[where p = "-\<pi>"], simp add: pemute_minus_self)
+  apply (perm_simp, rule step.intros)
+  apply (rule permute_boolE[where p = "-\<pi>"], simp add: pemute_minus_self)
+  apply (rule permute_boolE[where p = "-\<pi>"], simp add: pemute_minus_self)
+  apply (perm_simp, rule step.intros)
+  apply (rule permute_boolE[where p = "-\<pi>"], simp add: pemute_minus_self)
+  apply (rule permute_boolE[where p = "-\<pi>"], simp add: pemute_minus_self)
+  apply (perm_simp, rule step.intros)
+  apply (perm_simp, rule step.intros)
+  done  
+
+subsubsection {* Invariants *}
+
+lemma closed_invariant:
+  "invariant step closed"
+proof
+  fix c c'
+  assume "c \<Rightarrow> c'" and "closed c"
+  thus "closed c'"
+  by (induction rule: step.induct) (auto simp add: fv_subst_eq dest!: set_mp[OF fv_delete_subset] dest: set_mp[OF map_of_Some_fv_subset])
+qed
+
+lemma heap_upds_ok_invariant:
+  "invariant step heap_upds_ok_conf"
+proof
+  fix c c'
+  assume "c \<Rightarrow> c'" and "heap_upds_ok_conf c"
+  thus "heap_upds_ok_conf c'"
+  by (induction rule: step.induct) auto
+qed
 
 end
index 9250313..77c8414 100644 (file)
@@ -30,6 +30,7 @@ lemma fresh_Dummy[simp]: "a \<sharp> Dummy v = a \<sharp> v" unfolding fresh_def
 lemma fv_Alts[simp]: "fv (Alts e1 e2) = fv e1 \<union> fv e2"  unfolding fv_def by auto
 lemma fv_Arg[simp]: "fv (Arg v) = fv v"  unfolding fv_def by auto
 lemma fv_Upd[simp]: "fv (Upd v) = fv v"  unfolding fv_def by auto
+lemma fv_Dummy[simp]: "fv (Dummy v) = fv v"  unfolding fv_def by auto
 
 instance stack_elem :: fs  by (default, case_tac x) (auto simp add: finite_supp)
 
@@ -47,6 +48,12 @@ fun upds :: "stack \<Rightarrow> var set" where
 | "upds (Upd x # S) = insert x (upds S)"
 | "upds (Arg x # S) = upds S"
 | "upds (Dummy x # S) = upds S"
+fun dummies :: "stack \<Rightarrow> var set" where
+  "dummies [] = {}"
+| "dummies (Alts e1 e2 # S) = dummies S"
+| "dummies (Upd x # S) = dummies S"
+| "dummies (Arg x # S) = dummies S"
+| "dummies (Dummy x # S) = insert x (dummies S)"
 fun flattn :: "stack \<Rightarrow> var list" where
   "flattn [] = []"
 | "flattn (Alts e1 e2 # S) = fv_list e1 @ fv_list e2 @ flattn S"
@@ -66,14 +73,39 @@ lemma set_upds_list[simp]:
 
 lemma ups_fv_subset: "upds S \<subseteq> fv S"
   by (induction S rule: upds.induct) auto
+lemma fresh_distinct_ups: "atom ` V \<sharp>* S \<Longrightarrow> V \<inter> upds S = {}"
+   by (auto dest!: fresh_distinct_fv set_mp[OF ups_fv_subset])
 lemma ap_fv_subset: "ap S \<subseteq> fv S"
   by (induction S rule: upds.induct) auto
+lemma dummies_fv_subset: "dummies S \<subseteq> fv S"
+  by (induction S rule: dummies.induct) auto
 
 lemma fresh_flattn[simp]: "atom (a::var) \<sharp> flattn S \<longleftrightarrow> atom a \<sharp> S"
   by (induction S rule:flattn.induct) (auto simp add: fresh_Nil fresh_Cons fresh_append fresh_fv[OF finite_fv])
 lemma fresh_star_flattn[simp]: "atom ` (as:: var set) \<sharp>* flattn S \<longleftrightarrow> atom ` as \<sharp>* S"
   by (auto simp add: fresh_star_def)
 
+lemma upds_append[simp]: "upds (S@S') = upds S \<union> upds S'"
+  by (induction S rule: upds.induct) auto
+lemma upds_map_Dummy[simp]: "upds (map Dummy l) = {}"
+  by (induction l) auto
+
+lemma upds_list_append[simp]: "upds_list (S@S') = upds_list S @ upds_list S'"
+  by (induction S rule: upds.induct) auto
+lemma upds_list_map_Dummy[simp]: "upds_list (map Dummy l) = []"
+  by (induction l) auto
+
+lemma dummies_append[simp]: "dummies (S@S') = dummies S \<union> dummies S'"
+  by (induction S rule: dummies.induct) auto
+lemma dummies_map_Dummy[simp]: "dummies (map Dummy l) = set l"
+  by (induction l) auto
+
+lemma map_Dummy_inj[simp]: "map Dummy l = map Dummy l' \<longleftrightarrow> l = l'"
+  apply (induction l arbitrary: l')
+  apply (case_tac [!] l')
+  apply auto
+  done
+
 type_synonym conf = "(heap \<times> exp \<times> stack)"
 
 inductive boring_step where
@@ -120,8 +152,61 @@ lemma restr_stack_noop[simp]:
      (auto dest: Upd_eq_restr_stackD2)
   
 
-  
+subsubsection {* Invariants of the semantics *}
+
+inductive invariant :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "(\<And> x y. rel x y \<Longrightarrow> I x \<Longrightarrow> I y) \<Longrightarrow> invariant rel I"
+
+lemmas invariant.intros[case_names step]
+
+lemma invariantE:
+  "invariant rel I \<Longrightarrow> rel x y \<Longrightarrow> I x \<Longrightarrow> I y" by (auto elim: invariant.cases)
 
+lemma invariant_starE:
+  "rtranclp rel x y \<Longrightarrow> invariant rel I \<Longrightarrow>  I x \<Longrightarrow> I y"
+  by (induction rule: rtranclp.induct) (auto elim: invariantE)
+
+lemma invariant_True:
+  "invariant rel (\<lambda> _. True)"
+by (auto intro: invariant.intros)
+
+lemma invariant_conj:
+  "invariant rel I1 \<Longrightarrow> invariant rel I2 \<Longrightarrow> invariant rel (\<lambda> x. I1 x \<and> I2 x)"
+by (auto simp add: invariant.simps)
+
+
+thm rtranclp_induct[no_vars]
+
+lemma rtranclp_invariant_induct[consumes 3, case_names base step]:
+  assumes "r\<^sup>*\<^sup>* a b"
+  assumes "invariant r I"
+  assumes "I a"
+  assumes "P a"
+  assumes "(\<And>y z. r\<^sup>*\<^sup>* a y \<Longrightarrow> r y z \<Longrightarrow> I y \<Longrightarrow> I z \<Longrightarrow> P y \<Longrightarrow> P z)"
+  shows "P b"
+proof-
+  from assms(1,3)
+  have "P b" and "I b"
+  proof(induction)
+    case base
+    from `P a` show "P a".
+    from `I a` show "I a".
+  next
+    case (step y z)
+    with `I a` have "P y" and "I y" by auto
+
+    from assms(2) `r y z` `I y`
+    show "I z" by (rule invariantE)
+
+    from `r\<^sup>*\<^sup>* a y` `r y z` `I y` `I z` `P y`
+    show "P z" by (rule assms(5))
+  qed
+  thus "P b" by-
+qed
+
+
+fun closed :: "conf \<Rightarrow> bool"
+  where "closed (\<Gamma>, e, S) \<longleftrightarrow> fv (\<Gamma>, e, S) \<subseteq> domA \<Gamma> \<union> upds S"
 
 fun heap_upds_ok where "heap_upds_ok (\<Gamma>,S) \<longleftrightarrow> domA \<Gamma> \<inter> upds S = {} \<and> distinct (upds_list S)"
 
@@ -138,7 +223,6 @@ lemma heap_upds_ok_alts1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upd
 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> = {}"
   assumes "domA \<Delta> \<inter> upds S = {}"
   assumes "heap_upds_ok (\<Gamma>,S)"
   shows "heap_upds_ok (\<Delta>@\<Gamma>, S)"
@@ -146,6 +230,13 @@ lemma heap_upds_ok_append:
   unfolding heap_upds_ok.simps
   by auto
 
+lemma heap_upds_ok_let:
+  assumes "atom ` domA \<Delta> \<sharp>* S"
+  assumes "heap_upds_ok (\<Gamma>, S)"
+  shows "heap_upds_ok (\<Delta> @ \<Gamma>, S)"
+using assms(2) fresh_distinct_fv[OF assms(1)]
+by (auto intro: heap_upds_ok_append dest: set_mp[OF ups_fv_subset])
+
 lemma heap_upds_ok_to_stack:
   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
   by (auto)
@@ -184,6 +275,7 @@ lemmas heap_upds_ok_intros[intro] =
   heap_upds_ok_to_heap heap_upds_ok_to_stack 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 heap_upds_ok_delete
   heap_upds_ok_restrictA heap_upds_ok_restr_stack
+  heap_upds_ok_let
 lemmas heap_upds_ok.simps[simp del]
 
 
index 838323c..c796d79 100644 (file)
@@ -2,36 +2,41 @@ theory SestoftGC
 imports Sestoft 
 begin
 
-inductive gc_step :: "(var list \<times> conf) \<Rightarrow> (var list \<times> conf) \<Rightarrow> bool" (infix "\<Rightarrow>\<^sub>G" 50) where
-  normal:  "c \<Rightarrow> c' \<Longrightarrow> (r, c) \<Rightarrow>\<^sub>G (r, c')"
-| dropUpd: "(r, \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (x # r, \<Gamma>, e, S)"
+inductive gc_step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightarrow>\<^sub>G" 50) where
+  normal:  "c \<Rightarrow> c' \<Longrightarrow> c \<Rightarrow>\<^sub>G c'"
+| dropUpd: "(\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (\<Gamma>, e, S @ [Dummy x])"
 
 lemmas gc_step_intros[intro] =
   normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
   normal[OF step.intros(4)] normal[OF step.intros(5)]  dropUpd
 
-
 abbreviation gc_steps (infix "\<Rightarrow>\<^sub>G\<^sup>*" 50) where "gc_steps \<equiv> gc_step\<^sup>*\<^sup>*"
 lemmas converse_rtranclp_into_rtranclp[of gc_step, OF _ r_into_rtranclp, trans]
 
 lemma var_onceI:
   assumes "map_of \<Gamma> x = Some e"
-  shows "(r, \<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (x#r, delete x \<Gamma>, e , S)"
+  shows "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e , S@[Dummy x])"
 proof-
   from assms 
-  have "(r, \<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (r, delete x \<Gamma>, e , Upd x # S)"..
+  have "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e , Upd x # S)"..
   moreover
-  have "\<dots> \<Rightarrow>\<^sub>G  (x #r, delete x \<Gamma>, e , S)"..
+  have "\<dots> \<Rightarrow>\<^sub>G  (delete x \<Gamma>, e, S@[Dummy x])"..
   ultimately
   show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
 qed
 
-lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> (r, c) \<Rightarrow>\<^sub>G\<^sup>* (r, c')"
+lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c \<Rightarrow>\<^sub>G\<^sup>* c'"
   by (induction rule:rtranclp_induct)
      (simp, metis normal rtranclp.rtrancl_into_rtrancl)
 
 fun to_gc_conf :: "var list \<Rightarrow> conf \<Rightarrow> conf"
-  where "to_gc_conf r (\<Gamma>, e, S) = (restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S)"
+  where "to_gc_conf r (\<Gamma>, e, S) = (restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S @ (map Dummy (rev r)))"
+
+lemma restr_stack_map_Dummy[simp]: "restr_stack V (map Dummy l) = map Dummy l"
+  by (induction l) auto
+
+lemma restr_stack_append[simp]: "restr_stack V (l@l') = restr_stack V l @ restr_stack V l'"
+  by (induction l rule: restr_stack.induct) auto
 
 lemma to_gc_conf_append[simp]:
   "to_gc_conf (r@r') c = to_gc_conf r (to_gc_conf r' c)"
@@ -39,9 +44,8 @@ lemma to_gc_conf_append[simp]:
 
 lemma to_gc_conf_eqE[elim!]:
   assumes  "to_gc_conf r c = (\<Gamma>, e, S)"
-  obtains \<Gamma>' S' where "c = (\<Gamma>', e, S')" and "\<Gamma> = restrictA (- set r) \<Gamma>'" and "S = restr_stack (- set r) S'"
-  using assms
-  by (cases c) auto
+  obtains \<Gamma>' S' where "c = (\<Gamma>', e, S')" and "\<Gamma> = restrictA (- set r) \<Gamma>'" and "S = restr_stack (- set r) S' @ map Dummy (rev r)"
+  using assms by (cases c) auto
 
 fun safe_hd :: "'a list \<Rightarrow> 'a option"
  where  "safe_hd (x#_) = Some x"
@@ -50,22 +54,33 @@ fun safe_hd :: "'a list \<Rightarrow> 'a option"
 lemma safe_hd_None[simp]: "safe_hd xs = None \<longleftrightarrow> xs = []"
   by (cases xs) auto
 
-abbreviation r_ok :: "(var list \<times> conf) \<Rightarrow> bool"
-  where "r_ok c \<equiv> set (fst c) \<subseteq> domA (fst (snd c)) \<union> upds (snd (snd (snd c)))"
+abbreviation r_ok :: "var list \<Rightarrow> conf \<Rightarrow> bool"
+  where "r_ok r c \<equiv> set r \<subseteq> domA (fst c) \<union> upds (snd (snd c))"
+
+lemma subset_bound_invariant:
+  "invariant step (r_ok r)"
+proof
+  fix x y
+  assume "x \<Rightarrow> y" and "r_ok r x" thus "r_ok r y"
+  by (induction) auto
+qed
 
+lemma safe_hd_restr_stack[simp]:
+  "Some a = safe_hd (restr_stack V (a # S)) \<longleftrightarrow> restr_stack V (a # S) = a # restr_stack V S"
+  using assms
+  apply (cases a)
+  apply (auto split: if_splits)
+  apply (thin_tac "?P a")
+  apply (induction S rule: restr_stack.induct)
+  apply (auto split: if_splits)
+  done
 
 lemma sestoftUnGCStack:
   assumes "heap_upds_ok (\<Gamma>, S)"
-  assumes "set r \<subseteq> domA \<Gamma> \<union> upds S"
   obtains \<Gamma>' S' where
     "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
-    "heap_upds_ok (\<Gamma>', S')"
     "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
     "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
-    "set r \<subseteq> domA \<Gamma>' \<union> upds S'"
-(*proof(atomize_elim)
-  show "\<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> heap_upds_ok (\<Gamma>', S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or>  safe_hd S' = safe_hd (restr_stack (- set r) S'))"
-*)
 proof-
   show ?thesis
   proof(cases "isVal e")
@@ -84,7 +99,7 @@ proof-
       proof(cases "Some s = safe_hd (restr_stack (- set r) (s#S))")
         case True
         thus ?thesis
-          using `isVal e` `heap_upds_ok (\<Gamma>, s # S)` `set r \<subseteq> domA \<Gamma> \<union> upds (s # S)`
+          using `isVal e` `heap_upds_ok (\<Gamma>, s # S)`
           apply auto
           apply (intro exI conjI)
           apply (rule rtranclp.intros(1))
@@ -99,18 +114,13 @@ proof-
         have [simp]: "x \<notin> domA \<Gamma>" and "heap_upds_ok ((x,e) # \<Gamma>, S)"
           by (auto dest: heap_upds_okE) 
 
-        from `set r \<subseteq> domA \<Gamma> \<union> upds (s # S)`
-        have "set r \<subseteq> domA ((x,e) # \<Gamma>) \<union> upds S" by auto
-        
         have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)" unfolding `s = _` ..
-        also have "\<dots> \<Rightarrow> ((x,e) # \<Gamma>, e, S)" by (rule var\<^sub>2[OF `x \<notin> domA \<Gamma>` `isVal e`])
+        also have "\<dots> \<Rightarrow> ((x,e) # \<Gamma>, e, S)" by (rule step.var\<^sub>2[OF `x \<notin> domA \<Gamma>` `isVal e`])
         also
-        from Cons.IH[OF `heap_upds_ok ((x,e) # \<Gamma>, S)`  `set r \<subseteq> domA ((x,e) # \<Gamma>) \<union> upds S`]
+        from Cons.IH[OF `heap_upds_ok ((x,e) # \<Gamma>, S)` ]
         obtain \<Gamma>' S' where  "((x,e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
-            and res: "heap_upds_ok (\<Gamma>', S')"
-                     "to_gc_conf r ((x,e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
+            and res: "to_gc_conf r ((x,e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
                      "(\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))"
-                     "set r \<subseteq> domA \<Gamma>' \<union> upds S'"
           by blast
         note this(1)
         finally
@@ -120,196 +130,259 @@ proof-
     qed
   qed
 qed
-  
+
+lemma perm_exI_trivial:
+  "P x x \<Longrightarrow> \<exists> \<pi>. P (\<pi> \<bullet> x) x"
+by (rule exI[where x = "0::perm"]) auto
+
+lemma upds_list_restr_stack[simp]:
+  "upds_list (restr_stack V S) = filter (\<lambda> x. x\<in>V) (upds_list S)"
+by (induction S rule: restr_stack.induct) auto
+
+lemma heap_upd_ok_to_gc_conf:
+  "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> to_gc_conf r (\<Gamma>, e, S) = (\<Gamma>'', e'', S'') \<Longrightarrow> heap_upds_ok (\<Gamma>'', S'')"
+by (auto simp add: heap_upds_ok.simps)
 
 lemma sestoftUnGCstep:
-  assumes "to_gc_conf r c \<Rightarrow> d"
+  assumes "to_gc_conf r c \<Rightarrow>\<^sub>G d"
   assumes "heap_upds_ok_conf c"
-  assumes "r_ok (r, c)"
-  shows   "\<exists> c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r c' \<and> heap_upds_ok_conf c' \<and> r_ok (r, c')"
+  assumes "closed c"
+  and "r_ok r c"
+  shows   "\<exists> r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'"
 proof-
   obtain \<Gamma> e S where "c = (\<Gamma>, e, S)" by (cases c) auto
   with assms
-  have "heap_upds_ok (\<Gamma>,S)" and "set r \<subseteq> domA \<Gamma> \<union> upds S" by auto
-  from sestoftUnGCStack[OF this]
+  have "heap_upds_ok (\<Gamma>,S)" and "closed (\<Gamma>, e, S)" and "r_ok r (\<Gamma>, e, S)" by auto
+  from sestoftUnGCStack[OF this(1)]
   obtain \<Gamma>' S' where
     "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
     and *: "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
     and disj: "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
-    and "heap_upds_ok (\<Gamma>', S')"
-    and "set r \<subseteq> domA \<Gamma>' \<union> upds S'" by metis
-  note this(1)
-  also
+    by metis
+
+  from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` heap_upds_ok_invariant]  `heap_upds_ok (\<Gamma>,S)`
+  have "heap_upds_ok (\<Gamma>', S')" by auto
+
+  from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` closed_invariant  `closed (\<Gamma>, e, S)` ]
+  have "closed (\<Gamma>', e, S')" by auto
+
+  from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` subset_bound_invariant `r_ok r (\<Gamma>, e, S)` ]
+  have "r_ok r (\<Gamma>', e, S')" by auto
 
   from assms(1)[unfolded `c =_ ` *]
-  have "\<exists> \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'')  \<and> d = to_gc_conf r (\<Gamma>'', e'', S'') \<and> heap_upds_ok (\<Gamma>'', S'') \<and> set r \<subseteq> domA \<Gamma>'' \<union> upds S''"
-  proof(cases rule: step.cases)
-    case app\<^sub>1
-    thus ?thesis
-      using `heap_upds_ok (\<Gamma>', S')` and `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
-      apply auto
-      apply (intro exI conjI)
-      apply (rule step.intros)
-      apply auto
-      done
-  next
-    case app\<^sub>2
-    thus ?thesis
-      using disj  `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
-      apply (cases S')
-      apply auto
-      apply (intro exI conjI)
-      apply (rule step.intros)
-      apply auto
-      done
-  next
-    case var\<^sub>1
-    thus ?thesis
-      using `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
-      apply auto
-      apply (intro exI conjI)
-      apply (rule step.intros)
-      apply (auto simp add: restr_delete_twist)
-      done
-  next
-    case var\<^sub>2
-    thus ?thesis
-      using disj `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
-      apply (cases S')
-      apply auto
-      apply (intro exI conjI)
-      apply (rule step.intros)
-      apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
-      done
-  next
-    case (let\<^sub>1 \<Delta>'' \<Gamma>'' S'' e')
-    thus ?thesis
-      using `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
-      apply auto
-      apply (intro exI conjI)
-      apply (rule step.intros)
-      apply (auto simp add: restrictA_append)
-      sorry
-  next
-    case if\<^sub>1
-    thus ?thesis
-      using `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
-      apply auto
-      apply (intro exI conjI)
-      apply (rule step.intros)
-      apply (auto)
-      done
+  have "\<exists> r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')"
+  proof(cases rule: gc_step.cases)
+    case normal
+    hence "\<exists> \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')"
+    proof(cases rule: step.cases)
+      case app\<^sub>1
+      thus ?thesis
+        apply auto
+        apply (intro exI conjI)
+        apply (rule  step.intros)
+        apply auto
+        done
+    next
+      case (app\<^sub>2 \<Gamma> y ea x S)
+      thus ?thesis
+        using disj 
+        apply (cases S')
+        apply auto
+        apply (intro exI conjI)
+        apply (rule step.intros)
+        apply auto
+        done
+    next
+      case var\<^sub>1
+      thus ?thesis
+        apply auto
+        apply (intro  exI conjI)
+        apply (rule step.intros)
+        apply (auto simp add: restr_delete_twist)
+        done
+    next
+      case var\<^sub>2
+      thus ?thesis
+        using disj 
+        apply (cases S')
+        apply auto
+        apply (intro exI conjI)
+        apply (rule step.intros)
+        apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
+        done
+    next
+      case (let\<^sub>1 \<Delta>'' \<Gamma>'' S'' e')
+
+      from `closed (\<Gamma>', e, S')` let\<^sub>1
+      have "closed (\<Gamma>', Let \<Delta>'' e', S')" by simp
+
+      from fresh_distinct[OF let\<^sub>1(3)] fresh_distinct_fv[OF let\<^sub>1(4)]
+      have "domA \<Delta>'' \<inter> domA \<Gamma>'' = {}" and "domA \<Delta>'' \<inter> upds S'' = {}"  and "domA \<Delta>'' \<inter> dummies S'' = {}" 
+        by (auto dest: set_mp[OF ups_fv_subset] set_mp[OF dummies_fv_subset])
+      moreover
+      from let\<^sub>1(1)
+      have "domA \<Gamma>' \<union> upds S' \<subseteq> domA \<Gamma>'' \<union> upds S'' \<union> dummies S''"
+        by auto
+      ultimately
+      have disj: "domA \<Delta>'' \<inter> domA \<Gamma>' = {}" "domA \<Delta>'' \<inter> upds S' = {}"
+        by auto
+      
+      from `domA \<Delta>'' \<inter> dummies S'' = {}` let\<^sub>1(1)
+      have "domA \<Delta>'' \<inter> set r = {}" by auto
+      hence [simp]: "restrictA (- set r) \<Delta>'' = \<Delta>''"
+        by (auto intro: restrictA_noop)
+
+      from let\<^sub>1(1-3)
+      show ?thesis
+        apply auto
+        apply (intro  exI[where x = "r"] exI[where x = "\<Delta>'' @ \<Gamma>'"] exI[where x = "S'"] conjI)
+        apply (rule let\<^sub>1_closed[OF `closed (\<Gamma>', Let \<Delta>'' e', S')` disj])
+        apply (auto simp add: restrictA_append)
+        done
+    next
+      case if\<^sub>1
+      thus ?thesis
+        apply auto
+        apply (intro exI[where x = "0::perm"] exI conjI)
+        unfolding permute_zero
+        apply (rule step.intros)
+        apply (auto)
+        done
+    next
+      case if\<^sub>2
+      thus ?thesis
+        using disj
+        apply (cases S')
+        apply auto
+        apply (intro exI exI conjI)
+        apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
+        apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
+        apply (intro exI conjI)
+        apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
+        apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
+        done
+    qed
+    with invariantE[OF subset_bound_invariant _ `r_ok r (\<Gamma>', e, S')`]
+    show ?thesis by blast
   next
-    case if\<^sub>2
-    thus ?thesis
-      using disj `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
-      apply (cases S')
-      apply auto
-      apply (intro exI conjI)
-      apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
-      apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
-      apply (intro exI conjI)
-      apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
-      apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
-      done
+  case (dropUpd \<Gamma>'' e'' x S'')
+    from `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
+    have "x \<notin> set r" by (auto dest!: arg_cong[where f = upds])
+    
+    from `heap_upds_ok (\<Gamma>', S')` and `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
+    have "heap_upds_ok (\<Gamma>'', Upd x # S'')" by (rule heap_upd_ok_to_gc_conf)
+    hence [simp]: "x \<notin> domA \<Gamma>''" "x \<notin> upds S''" by (auto dest: heap_upds_ok_upd)
+
+    have "to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x]@ r) (\<Gamma>', e, S')" by simp
+    also have "\<dots> = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))" by (rule to_gc_conf_append)
+    also have "\<dots> = to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'')" unfolding `to_gc_conf r (\<Gamma>', e, S') = _`..
+    also have "\<dots> = (\<Gamma>'', e'', S''@[Dummy x])" by (auto intro: restrictA_noop)
+    also have "\<dots> = d" using ` d= _` by simp
+    finally have "to_gc_conf (x # r) (\<Gamma>', e, S') = d".
+    moreover
+    from `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
+    have "x \<in> upds S'" by (auto dest!: arg_cong[where f = upds])
+    with `r_ok r (\<Gamma>', e, S')`
+    have "r_ok (x # r) (\<Gamma>', e, S')" by auto
+    moreover
+    note `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
+    ultimately
+    show ?thesis by fastforce
   qed
-  then obtain \<Gamma>'' e'' S''
-    where "(\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'')"
-    and "d = to_gc_conf r (\<Gamma>'', e'', S'')"
-    and "heap_upds_ok (\<Gamma>'', S'')"
-    and "set r \<subseteq> domA \<Gamma>'' \<union> upds S''"
-    by blast
-  note this(1)
-  finally
-  have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')".
-  with `d = _` `heap_upds_ok (\<Gamma>'', S'')` `set r \<subseteq> domA \<Gamma>'' \<union> upds S''`
+  then obtain r' \<Gamma>'' e'' S''
+    where "(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')"
+    and "d = to_gc_conf r' (\<Gamma>'', e'', S'')"
+    and "r_ok r' (\<Gamma>'', e'', S'')"
+    by metis 
+
+  from  `(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')` and `(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')`
+  have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')" by (rule rtranclp_trans)
+  with `d = _` `r_ok r' _`
   show ?thesis unfolding `c = _` by auto
 qed
 
 
 lemma sestoftUnGC:
-  assumes "(r, to_gc_conf r c) \<Rightarrow>\<^sub>G\<^sup>* (r', d)" and "heap_upds_ok_conf c" and "r_ok (r, c)"
-  shows   "\<exists> c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> heap_upds_ok_conf c' \<and> r_ok (r', c')"
+  assumes "(to_gc_conf r c) \<Rightarrow>\<^sub>G\<^sup>* d" and "heap_upds_ok_conf c" and "closed c" and "r_ok r c"
+  shows   "\<exists> r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'"
 using assms
-proof(induction r' "d"  rule: rtranclp_induct2)
-  case refl
+proof(induction rule: rtranclp_induct)
+  case base
   thus ?case by blast
 next
-  case (step r' d' r'' d'')
-  then obtain c' where "c \<Rightarrow>\<^sup>* c'" and "d' = to_gc_conf r' c'" and "heap_upds_ok_conf c'" and "r_ok (r', c')" by auto
-  with step
-  have "(r', to_gc_conf r' c') \<Rightarrow>\<^sub>G (r'', d'')" by simp
-  hence "\<exists> c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> heap_upds_ok_conf c'' \<and> r_ok (r'', c'')"
-  proof(cases rule: gc_step.cases)
-    case normal
-    from sestoftUnGCstep[OF normal(2) `heap_upds_ok_conf c'` `r_ok (r',c')`] `r'' = r'`
-    show ?thesis by auto
-  next
-    case (dropUpd \<Gamma> e x S)
-    from `to_gc_conf r' c' = (\<Gamma>, e, Upd x # S)`
-    have "x \<notin> set r'" by (auto dest: Upd_eq_restr_stackD)
-    
-    from `heap_upds_ok_conf c'` and `to_gc_conf r' c' = (\<Gamma>, e, Upd x # S)`
-    have "heap_upds_ok (\<Gamma>, Upd x # S)" by fastforce
-    hence [simp]: "x \<notin> domA \<Gamma>" "x \<notin> upds S" by (auto dest: heap_upds_ok_upd)
-
-    from `to_gc_conf r' c' = (\<Gamma>, e, Upd x # S)`
-    have "Upd x # S = restr_stack (- set r') (snd (snd c'))"  by auto
-    from arg_cong[where f = upds, OF this]
-    have "x \<in> upds (snd (snd c'))" by auto
-    with `r_ok (r', c')` have "r_ok (x # r', c')" by auto
-
-    have "to_gc_conf (x # r') c' = to_gc_conf ([x]@ r') c'" by simp
-    also have "\<dots> = to_gc_conf [x] (to_gc_conf r' c')" by (rule to_gc_conf_append)
-    also have "\<dots> = to_gc_conf [x] (\<Gamma>, e, Upd x # S)" unfolding `to_gc_conf r' c' = _`..
-    also have "\<dots> = (\<Gamma>, e, S)" by (auto intro: restrictA_noop)
-    finally have "to_gc_conf (x # r') c' = (\<Gamma>, e, S)".
-    with dropUpd  `heap_upds_ok_conf c'` `r_ok (x # r', c')`
-    show ?thesis by fastforce
-  qed
-  then obtain c'' where "c' \<Rightarrow>\<^sup>* c''" and "d'' = to_gc_conf r'' c''" and "heap_upds_ok_conf c''" and "r_ok (r'', c'')" by auto
-  with `c \<Rightarrow>\<^sup>* c'` `c' \<Rightarrow>\<^sup>* c''`
+  case (step d' d'')
+  then obtain r' c' where "c \<Rightarrow>\<^sup>*  c'" and "d' = to_gc_conf r' c'" and "r_ok r' c'"  by auto
+
+  from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` heap_upds_ok_invariant]  `heap_upds_ok _`
+  have "heap_upds_ok_conf c'".
+
+  from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` closed_invariant]  `closed _` 
+  have "closed c'".
+
+  from step `d' = to_gc_conf r' c'`
+  have "to_gc_conf r' c' \<Rightarrow>\<^sub>G d''" by simp
+  from this `heap_upds_ok_conf c'` `closed c'` `r_ok r' c'`
+  have "\<exists> r'' c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> r_ok r'' c''"
+    by (rule sestoftUnGCstep)
+  then obtain r'' c'' where "c' \<Rightarrow>\<^sup>* c''" and "d'' = to_gc_conf r'' c''" and "r_ok r'' c''" by auto
+  
+  from `c' \<Rightarrow>\<^sup>*  c''` `c \<Rightarrow>\<^sup>*  c'`
   have "c \<Rightarrow>\<^sup>* c''" by auto
-  with `d'' = _` `heap_upds_ok_conf c''` `r_ok (r'', c'')`
+  with `d'' = _` `r_ok r'' c''`
   show ?case by blast
 qed
+
+lemma dummies_unchanged_invariant:
+  "invariant step (\<lambda> (\<Gamma>, e, S) . dummies S = V)" (is "invariant _ ?I")
+proof
+  fix c c'
+  assume "c \<Rightarrow> c'" and "?I c"
+  thus "?I c'" by (induction) auto
+qed
   
 lemma sestoftUnGC':
-  assumes "([], [], e, []) \<Rightarrow>\<^sub>G\<^sup>* (r, \<Gamma>, e', [])"
+  assumes "([], e, []) \<Rightarrow>\<^sub>G\<^sup>* (\<Gamma>, e', map Dummy r)"
   assumes "isVal e'"
+  assumes "fv e = ({}::var set)"
   shows   "\<exists> \<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''"
 proof-
- from sestoftUnGC[where r = "[]" and c = "([], e, [])", simplified, OF assms(1)]
- obtain \<Gamma>' S'
+ from sestoftUnGC[where r = "[]" and c = "([], e, [])", simplified, OF assms(1,3)]
+ obtain r' \<Gamma>' S'
   where "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')"
-    and "\<Gamma> = restrictA (- set r) \<Gamma>'"
-    and "restr_stack (- set r) S' = []"
-    and "heap_upds_ok (\<Gamma>', S')"
-    and "set r \<subseteq> domA \<Gamma>' \<union> upds S'"
+    and "\<Gamma> = restrictA (- set r') \<Gamma>'"
+    and "map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')"
+    and "r_ok r' (\<Gamma>', e', S')"
     by auto
+
+  from invariant_starE[OF `([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')` dummies_unchanged_invariant]
+  have "dummies S' = {}" by auto
+  with  `map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')`
+  have "restr_stack (- set r') S' = []" and [simp]: "r = rev r'"
+  by (induction S' rule: restr_stack.induct) (auto split: if_splits)
+  
+  from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` heap_upds_ok_invariant]
+  have "heap_upds_ok (\<Gamma>', S')" by auto
  
-  from `isVal e'` sestoftUnGCStack[where e = e', OF `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`]
+  from `isVal e'` sestoftUnGCStack[where e = e', OF `heap_upds_ok (\<Gamma>', S')` ]
   obtain \<Gamma>'' S''
     where "(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')"
-    and   "heap_upds_ok (\<Gamma>'', S'')"
     and "to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')"
     and "safe_hd S'' = safe_hd (restr_stack (- set r) S'')"
-    and "set r \<subseteq> domA \<Gamma>'' \<union> upds S''"
     by metis
-  from this (3,4) `restr_stack (- set r) S' = []`
+
+  from this (2,3) `restr_stack (- set r') S' = []`
   have "S'' = []" by auto
-  from `([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')` and `(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')` and `S'' = []`
-  have "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', [])" by auto
+
+  from  `([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')`  and `(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')` and `S'' = []`
+  have "([], e, []) \<Rightarrow>\<^sup>*  (\<Gamma>'', e', [])" by auto
   moreover
   have "\<Gamma> = restrictA (- set r) \<Gamma>''" using `to_gc_conf r _ = _` `\<Gamma> = _` by auto
   moreover
-  from `set r \<subseteq> domA \<Gamma>'' \<union> upds S''` `S'' = []`
-  have "set r \<subseteq> domA \<Gamma>''" by simp
+  from invariant_starE[OF `(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')` subset_bound_invariant `r_ok r' (\<Gamma>', e', S')`]
+  have "set r \<subseteq> domA \<Gamma>''" using `S'' = []` by auto
   ultimately
   show ?thesis by blast
 qed
 
-
 end