Correctness via card, ugly proof from GCstep to step (up to renaming)
authorJoachim Breitner <mail@joachim-breitner.de>
Mon, 26 Jan 2015 09:39:21 +0000 (09:39 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Mon, 26 Jan 2015 09:39:21 +0000 (09:39 +0000)
Launchbury/ArityConsistent.thy
Launchbury/CallArityCorrectEnd2End.thy
Launchbury/CardinalityEtaExpandCorrect.thy
Launchbury/SestoftConf.thy
Launchbury/SestoftGC.thy

index 7d3919e..f9e9ffe 100644 (file)
@@ -178,7 +178,6 @@ qed
 
 lemma 
   assumes "a_consistent (ae, a, as) (\<Gamma>, e, Upd x # S)"
 
 lemma 
   assumes "a_consistent (ae, a, as) (\<Gamma>, e, Upd x # S)"
-  and "x \<in> edom ae"
   shows a_consistent_var\<^sub>2: "a_consistent (ae, a, as) ((x, e) # \<Gamma>, e, S)" 
     and a_consistent_UpdD: "ae x = up\<cdot>0""a = 0"
     using assms
   shows a_consistent_var\<^sub>2: "a_consistent (ae, a, as) ((x, e) # \<Gamma>, e, S)" 
     and a_consistent_UpdD: "ae x = up\<cdot>0""a = 0"
     using assms
index 76d6c9f..e58e3fc 100644 (file)
@@ -10,41 +10,54 @@ sublocale CallArityEnd2End.
 lemma end2end:
   "c \<Rightarrow>\<^sup>* c' \<Longrightarrow>
   \<not> boring_step c' \<Longrightarrow>
 lemma end2end:
   "c \<Rightarrow>\<^sup>* c' \<Longrightarrow>
   \<not> boring_step c' \<Longrightarrow>
-  consistent (ae, ce, a, as) c \<Longrightarrow>
-  \<exists>ae' ce' a' as'. consistent  (ae', ce', a', as') c' \<and> conf_transform  (ae, ce, a, as) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform  (ae', ce', a', as') c'"
+  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)
 
 lemma end2end_closed:
   assumes closed: "fv e = ({} :: var set)"
   assumes "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>,v,[])"
   by (rule foo)
 
 lemma end2end_closed:
   assumes closed: "fv e = ({} :: var set)"
   assumes "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>,v,[])"
-  assumes "isLam v"
-  shows "\<exists> \<Gamma>' v'. length \<Gamma>' \<le> length \<Gamma> \<and> isLam v' \<and> ([], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (\<Gamma>',v',[])"
+  assumes "isVal v"
+  shows "\<exists> \<Gamma>' v' r. card (domA \<Gamma>) = card (domA \<Gamma>') \<and> isVal v' \<and> ([], transform 0 e, []) \<Rightarrow>\<^sup>* (\<Gamma>',v',[])"
 proof-
   note assms(2)
   moreover
   have "\<not> boring_step (\<Gamma>,v,[])" by (simp add: boring_step.simps)
   moreover
 proof-
   note assms(2)
   moreover
   have "\<not> boring_step (\<Gamma>,v,[])" by (simp add: boring_step.simps)
   moreover
-  have "consistent (\<bottom>,\<bottom>,0,[]) ([], e, [])" using closed by (rule closed_consistent)
+  have "consistent (\<bottom>,\<bottom>,0,[],[]) ([], e, [])" using closed by (rule closed_consistent)
   ultimately
   ultimately
-  obtain ae ce a as where
-    *: "consistent  (ae, ce, a, as) (\<Gamma>,v,[])" and
-    **: "conf_transform  (\<bottom>, \<bottom>, 0, []) ([],e,[]) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a, as) (\<Gamma>,v,[])"
+  obtain ae ce a as where
+    *: "consistent  (ae, ce, a, as, r) (\<Gamma>,v,[])" and
+    **: "conf_transform  (\<bottom>, \<bottom>, 0, [], []) ([],e,[]) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a, as, r) (\<Gamma>,v,[])"
     by (metis end2end)
 
     by (metis end2end)
 
-  let ?\<Gamma> = "map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))"
+  let ?\<Gamma> = "map_transform Aeta_expand ae (map_transform transform ae (restrictA (-set r) \<Gamma>))"
   let ?v = "transform a v"
 
   let ?v = "transform a v"
 
-  show ?thesis
-  proof(intro exI conjI)
-    show "length ?\<Gamma> \<le> length \<Gamma>"
-      by (simp add:  order_trans[OF length_restrictA_le])
-
-    have "conf_transform  (\<bottom>, \<bottom>, 0, []) ([],e,[]) = ([],transform 0 e,[])" by simp
-    with **
-    show "([], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (?\<Gamma>, ?v, [])" by simp
-
-    show "isLam (transform a v)" using `isLam v` by simp
-  qed
+  from * have "set r \<subseteq> domA \<Gamma>" by auto
+
+  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 "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 "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 "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`
+  show ?thesis by blast
 qed
 
 lemma fresh_var_eqE[elim_format]: "fresh_var e = x \<Longrightarrow> x \<notin>  fv e"
 qed
 
 lemma fresh_var_eqE[elim_format]: "fresh_var e = x \<Longrightarrow> x \<notin>  fv e"
index 30077d5..6226fab 100644 (file)
@@ -26,7 +26,7 @@ begin
   interpretation supp_bounded_transform transform
     by default (auto simp add: fresh_def supp_transform) 
 
   interpretation supp_bounded_transform transform
     by default (auto simp add: fresh_def supp_transform) 
 
-  type_synonym tstate = "(AEnv \<times> (var \<Rightarrow> two) \<times> Arity \<times> Arity list)"
+  type_synonym tstate = "(AEnv \<times> (var \<Rightarrow> two) \<times> Arity \<times> Arity list \<times> var list)"
 
   fun transform_alts :: "Arity list \<Rightarrow> stack \<Rightarrow> stack"
     where 
 
   fun transform_alts :: "Arity list \<Rightarrow> stack \<Rightarrow> stack"
     where 
@@ -53,22 +53,24 @@ 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 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> conf"
-  where "conf_transform (ae, ce, a, as) c = a_transform (ae, a, as) (restr_conf (edom ce) c)"
-
+  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))"
 
   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
     consistentI[intro!]: 
 
   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
     consistentI[intro!]: 
-    "a_consistent (ae, a, as) (restr_conf (edom ce) (\<Gamma>, e, S))
+    "a_consistent (ae, a, as) (restr_conf (- set r) (\<Gamma>, e, S))
     \<Longrightarrow> edom ae = edom ce
     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
     \<Longrightarrow> edom ae = edom ce
     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
-    \<Longrightarrow> consistent (ae, ce, a, as) (\<Gamma>, e, S)"  
+    \<Longrightarrow> set r \<inter> edom ce = {}
+    \<Longrightarrow> set r \<subseteq> domA \<Gamma> \<union> upds S
+    \<Longrightarrow> upds S - edom ce \<subseteq> set r
+    \<Longrightarrow> consistent (ae, ce, a, as, r) (\<Gamma>, e, S)"  
   inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (\<Gamma>, e, S)"
 
   lemma closed_consistent:
     assumes "fv e = ({}::var set)"
   inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (\<Gamma>, e, S)"
 
   lemma closed_consistent:
     assumes "fv e = ({}::var set)"
-    shows "consistent (\<bottom>, \<bottom>, 0, []) ([], e, [])"
+    shows "consistent (\<bottom>, \<bottom>, 0, [], []) ([], e, [])"
   proof-
     from assms
     have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
   proof-
     from assms
     have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
@@ -78,17 +80,17 @@ begin
   qed
 
   lemma foo:
   qed
 
   lemma foo:
-    fixes c c' R 
-    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a,as) c"
-    shows "\<exists>ae' ce' a' as'. consistent (ae',ce',a',as') c' \<and> conf_transform (ae,ce,a,as) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae',ce',a',as') c'"
+    fixes c c'
+    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step 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
   using assms
-  proof(induction c c' arbitrary: ae ce a as rule:step_induction)
+  proof(induction c c' arbitrary: ae ce a as r rule:step_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)
   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) (\<Gamma>, e, Arg x # S)"
+    with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a, as, r) (\<Gamma>, e, Arg x # S)"
       by (auto intro: a_consistent_app\<^sub>1 elim: below_trans)
     moreover
       by (auto intro: a_consistent_app\<^sub>1 elim: below_trans)
     moreover
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, App e x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
+    have "conf_transform (ae, ce, a, as, r) (\<Gamma>, App e x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, inc\<cdot>a, as, r) (\<Gamma>, e, Arg x # S)"
       by simp rule
     ultimately
     show ?case by (blast del: consistentI consistentE)
       by simp rule
     ultimately
     show ?case by (blast del: consistentI consistentE)
@@ -97,10 +99,10 @@ begin
     have "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as a (\<Gamma>, (Lam [y]. e), Arg x # S)"
        by (rule prognosis_subst_Lam)
     then
     have "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as a (\<Gamma>, (Lam [y]. e), Arg x # S)"
        by (rule prognosis_subst_Lam)
     then
-    have "consistent (ae, ce, pred\<cdot>a, as) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
+    have "consistent (ae, ce, pred\<cdot>a, as, r) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
       by (auto 4 3 intro: a_consistent_app\<^sub>2 elim: below_trans)
     moreover
       by (auto 4 3 intro: a_consistent_app\<^sub>2 elim: below_trans)
     moreover
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, pred \<cdot> a, as) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
+    have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, pred \<cdot> a, as, r) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
     ultimately
     show ?case by (blast  del: consistentI consistentE)
   next
     ultimately
     show ?case by (blast  del: consistentI consistentE)
   next
@@ -111,6 +113,7 @@ begin
     from thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
     from below_trans[OF prognosis_called fun_belowD[OF this] ]
     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
     from thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
     from below_trans[OF prognosis_called fun_belowD[OF this] ]
     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)
 
 
     have "x \<notin> upds S" using thunk by (auto dest!: a_consistent_heap_upds_okD  heap_upds_okE)
 
@@ -144,7 +147,7 @@ begin
       have eq: "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) = prognosis ae as u (delete x \<Gamma>, e, Upd x # S)"
         by (rule prognosis_env_cong) simp
 
       have eq: "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) = prognosis ae as u (delete x \<Gamma>, e, Upd x # S)"
         by (rule prognosis_env_cong) simp
 
-      have [simp]: "restr_stack (edom ce - {x}) S = restr_stack (edom ce) S" 
+      have [simp]: "restr_stack (- set r - {x}) S = restr_stack (- set r) S"
         using `x \<notin> upds S` by (auto intro: restr_stack_cong)
     
       have "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
         using `x \<notin> upds S` by (auto intro: restr_stack_cong)
     
       have "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
@@ -153,35 +156,36 @@ begin
         by (rule below_env_deleteI)
       moreover
 
         by (rule below_env_deleteI)
       moreover
 
-      have *: "a_consistent (env_delete x ae, u, as) (delete x (restrictA (edom ce) \<Gamma>), e, restr_stack (edom ce) S)" using thunk `ae x = up\<cdot>u`
-          by (auto intro!: a_consistent_thunk_once simp del: restr_delete)
+      have *: "a_consistent (env_delete x ae, u, as) (delete x (restrictA (- set r) \<Gamma>), e, restr_stack (- set r) S)"
+        using thunk `ae x = up\<cdot>u`
+        by (auto intro!: a_consistent_thunk_once simp del: restr_delete)
       ultimately
 
       ultimately
 
-      have "consistent (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" using thunk
-        by (auto  simp add:   restr_delete_twist elim:below_trans )
+      have "consistent (env_delete x ae, env_delete x ce, u, as, x # r) (delete x \<Gamma>, e, Upd x # S)" using thunk
+        by (auto simp add: restr_delete_twist Compl_insert elim:below_trans )
       moreover
 
       from *
       moreover
 
       from *
-      have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
+      have "Astack (transform_alts as (restr_stack (- set r) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
       
       {
       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` once
       
       {
       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 (edom ce) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
+      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)
         by (simp add: map_of_map_transform)
-      hence "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G
-             (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (edom ce) S))"
+      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))"
           by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist simp del: restr_delete)
       also
           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>* (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (edom ce) S))"
+      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)
       also
         by (rule r_into_rtranclp, rule)
       also
-      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae  (restrictA (edom ce) \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (edom ce) S))"
-        by (intro normal_trans Aeta_expand_correct `Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u`)
+      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`)
       also(rtranclp_trans)
       also(rtranclp_trans)
-      have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" 
-        by (auto intro!: map_transform_cong simp add:  map_transform_delete[symmetric]  restr_delete_twist)
+      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)
       finally(back_subst)
       finally(back_subst)
-      have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)".
+      have "conf_transform (ae, ce, a, as, r) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (env_delete x ae, env_delete x ce, u, as, x # r) (delete x \<Gamma>, e, Upd x # S)".
       }
       ultimately
       show ?thesis by (blast del: consistentI consistentE)
       }
       ultimately
       show ?thesis by (blast del: consistentI consistentE)
@@ -202,18 +206,18 @@ begin
       
       have "prognosis ae as 0 (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> ce" using *[unfolded `u=0`] thunk by (auto elim: below_trans)
       moreover
       
       have "prognosis ae as 0 (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> ce" using *[unfolded `u=0`] thunk by (auto elim: below_trans)
       moreover
-      have "a_consistent (ae, 0, as) (delete x (restrictA (edom ce) \<Gamma>), e, Upd x # restr_stack (edom ce) S)" using thunk `ae x = up\<cdot>0`
+      have "a_consistent (ae, 0, as) (delete x (restrictA (- set r) \<Gamma>), e, Upd x # restr_stack (- set r) S)" using thunk `ae x = up\<cdot>0`
         by (auto intro!: a_consistent_thunk_0 simp del: restr_delete)
       ultimately
         by (auto intro!: a_consistent_thunk_0 simp del: restr_delete)
       ultimately
-      have "consistent (ae, ce, 0, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`
+      have "consistent (ae, ce, 0, as, r) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`
         by (auto simp add:  restr_delete_twist)
       moreover
   
       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0` many
         by (auto simp add:  restr_delete_twist)
       moreover
   
       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0` many
-      have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))) x = Some (transform 0 e)"
+      have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) \<Gamma>))) x = Some (transform 0 e)"
         by (simp add: map_of_map_transform)
       with `\<not> isVal e`
         by (simp add: map_of_map_transform)
       with `\<not> isVal e`
-      have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as) (delete x \<Gamma>, e, Upd x # S)"
+      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)
       ultimately
       show ?thesis by (blast del: consistentI consistentE)
         by (auto simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
       ultimately
       show ?thesis by (blast del: consistentI consistentE)
@@ -227,6 +231,9 @@ begin
     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
     then obtain c where "ce x = up\<cdot>c" by (cases "ce x") (auto simp add: edom_def)
 
     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
     then obtain c where "ce x = up\<cdot>c" by (cases "ce x") (auto simp add: edom_def)
 
+    from lamvar
+    have [simp]: "x \<notin> set r" by auto
+
     then have "x \<in> edom ae" using lamvar by auto
     then obtain  u where "ae x = up\<cdot>u"  by (cases "ae x") (auto simp add: edom_def)
 
     then have "x \<in> edom ae" using lamvar by auto
     then obtain  u where "ae x = up\<cdot>u"  by (cases "ae x") (auto simp add: edom_def)
 
@@ -238,15 +245,15 @@ begin
     also have "\<dots> \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
     finally have *: "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by this simp_all
     moreover
     also have "\<dots> \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
     finally have *: "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by this simp_all
     moreover
-    have "a_consistent (ae, u, as) ((x,e) # delete x (restrictA (edom ce) \<Gamma>), e, restr_stack (edom ce) S)" using lamvar `ae x = up\<cdot>u`
+    have "a_consistent (ae, u, as) ((x,e) # delete x (restrictA (- set r) \<Gamma>), e, restr_stack (- set r) S)" using lamvar `ae x = up\<cdot>u`
       by (auto intro!: a_consistent_lamvar simp del: restr_delete)
     ultimately
       by (auto intro!: a_consistent_lamvar simp del: restr_delete)
     ultimately
-    have "consistent (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
+    have "consistent (ae, ce, u, as, r) ((x, e) # delete x \<Gamma>, e, S)"
       using lamvar edom_mono[OF *] by (auto simp add:  thunks_Cons restr_delete_twist elim: below_trans)
     moreover
 
     from `a_consistent _ _`
       using lamvar edom_mono[OF *] by (auto simp add:  thunks_Cons restr_delete_twist elim: below_trans)
     moreover
 
     from `a_consistent _ _`
-    have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
+    have "Astack (transform_alts as (restr_stack (- set r) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
   
     {
     from `isVal e`
   
     {
     from `isVal e`
@@ -254,19 +261,19 @@ begin
     hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
     moreover
     from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
     hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
     moreover
     from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
-    have "map_of (map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
+    have "map_of (map_transform Aeta_expand ae (map_transform transform ae (restrictA (- set r) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
       by (simp add: map_of_map_transform)
     ultimately
       by (simp add: map_of_map_transform)
     ultimately
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>*
-          ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))), Aeta_expand u (transform u e), transform_alts as (restr_stack (edom ce) S))"
-       by (auto intro: lambda_var simp add: map_transform_delete simp del: restr_delete)
-    also have "\<dots> = ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x (restrictA (edom ce) \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
+    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))"
+       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))"
       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)
       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>\<^sup>* conf_transform (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
-      by (simp add: restr_delete_twist) (rule Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`])
+    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`]])
     finally(rtranclp_trans)
     finally(rtranclp_trans)
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* conf_transform (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)".
+    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)
   next
     }
     ultimately show ?case by (blast intro: normal_trans del: consistentI consistentE)
   next
@@ -274,28 +281,25 @@ begin
     show ?case
     proof(cases "x \<in> edom ce")
       case True[simp]
     show ?case
     proof(cases "x \<in> edom ce")
       case True[simp]
-      hence "ce x \<noteq> \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
-      from True have "x \<in> edom ae" using var\<^sub>2 by auto
-      obtain c where "ce x = up\<cdot>c" using `ce x \<noteq> \<bottom>` by (cases "ce x") auto
-  
+      hence [simp]: "x \<notin> set r" using var\<^sub>2 by auto
+
       from var\<^sub>2
       from var\<^sub>2
-      have "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, e, Upd x # restr_stack (edom ce) S)" by auto
-      from a_consistent_UpdD[OF this  `x \<in> edom ae`]
+      have "a_consistent (ae, a, as) (restrictA (- set r) \<Gamma>, e, Upd x # restr_stack (-set r) S)" by auto
+      from a_consistent_UpdD[OF this]
       have "ae x = up\<cdot>0" and "a = 0".
   
       from `isVal e` `x \<notin> domA \<Gamma>`
       have *: "prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
       moreover
       have "ae x = up\<cdot>0" and "a = 0".
   
       from `isVal e` `x \<notin> domA \<Gamma>`
       have *: "prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
       moreover
-      have "a_consistent (ae, a, as) ((x, e) # restrictA (edom ce) \<Gamma>, e, restr_stack (edom ce) S)"
+      have "a_consistent (ae, a, as) ((x, e) # restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S)"
         using var\<^sub>2 by (auto intro!: a_consistent_var\<^sub>2)
       ultimately
         using var\<^sub>2 by (auto intro!: a_consistent_var\<^sub>2)
       ultimately
-      have "consistent (ae, ce, 0, as) ((x, e) # \<Gamma>, e, S)"
+      have "consistent (ae, ce, 0, as, r) ((x, e) # \<Gamma>, e, S)"
         using var\<^sub>2 `a = 0`
         by (auto simp add: thunks_Cons elim: below_trans)
       moreover
         using var\<^sub>2 `a = 0`
         by (auto simp add: thunks_Cons elim: below_trans)
       moreover
-      have "conf_transform (ae, ce, a, as) (\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, as) ((x, e) # \<Gamma>, e, S)"
-        using `ae x = up\<cdot>0` `a = 0` var\<^sub>2 `ce x = up\<cdot>c`
+      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)
       ultimately show ?thesis by (blast del: consistentI consistentE)
     next
         by (auto intro!: step.intros simp add: map_transform_Cons)
       ultimately show ?thesis by (blast del: consistentI consistentE)
     next
@@ -305,23 +309,22 @@ begin
       from False have "x \<notin> edom ae" using var\<^sub>2 by auto
       hence [simp]: "ae x = \<bottom>" by (auto simp add: edom_def)
 
       from False have "x \<notin> edom ae" using var\<^sub>2 by auto
       hence [simp]: "ae x = \<bottom>" by (auto simp add: edom_def)
 
+      from False have [simp]: "x \<in> set r" using var\<^sub>2 by auto
       
       have "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a ((x, e) # \<Gamma>, e, Upd x # S)" by (rule prognosis_upd)
       
       have "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a ((x, e) # \<Gamma>, e, Upd x # S)" by (rule prognosis_upd)
-      also
-       
-      from `ae x = \<bottom>`
-      have "prognosis ae as a ((x, e) # \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae as a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
-        by (rule prognosis_not_called)
-      also have  "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
+      also have "\<dots> \<sqsubseteq> prognosis ae as a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
+        using `ae x = \<bottom>` by (rule prognosis_not_called)
+      also have "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
       finally
       have *: "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, e, Upd x # S)" by this simp
       then
       finally
       have *: "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, e, Upd x # S)" by this simp
       then
-      have "consistent (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
-        by (auto simp add: thunks_Cons  elim:below_trans)
+      have "consistent (ae, ce, a, as, r) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
+        by (auto simp add: thunks_Cons  elim:below_trans a_consistent_var\<^sub>2)
       moreover
       moreover
-      have "conf_transform (ae, ce, a, as) (\<Gamma>, e, Upd x # S) = conf_transform (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)"
-        by(simp add: map_transform_restrA[symmetric])
-      ultimately show ?thesis by (auto del: consistentI consistentE simp del:conf_transform.simps)
+      have "conf_transform (ae, ce, a, as, r) (\<Gamma>, e, Upd x # S) = conf_transform (ae, ce, a, as, r) ((x, e) # \<Gamma>, e, S)"
+        by (auto simp add: map_transform_restrA[symmetric])
+      ultimately show ?thesis
+        by (fastforce del: consistentI consistentE simp del:conf_transform.simps)
     qed
   next
     case (let\<^sub>1 \<Delta> \<Gamma> e S)
     qed
   next
     case (let\<^sub>1 \<Delta> \<Gamma> e S)
@@ -346,6 +349,12 @@ begin
     have [simp]: "restrictA (edom ae \<union> edom (Aheap \<Delta> e\<cdot>a)) \<Gamma> = restrictA (edom ae) \<Gamma>"
       by (auto intro: restrictA_cong dest!: set_mp[OF edom_Aheap]) 
 
     have [simp]: "restrictA (edom ae \<union> edom (Aheap \<Delta> e\<cdot>a)) \<Gamma> = restrictA (edom ae) \<Gamma>"
       by (auto intro: restrictA_cong dest!: set_mp[OF edom_Aheap]) 
 
+    have "set r \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
+    have [simp]: "restrictA (- set r) \<Delta> = \<Delta>"
+      apply (rule restrictA_noop)
+      apply auto
+      by (metis IntI UnE `set r \<subseteq> domA \<Gamma> \<union> upds S` `domA \<Delta> \<inter> domA \<Gamma> = {}` `domA \<Delta> \<inter> upds S = {}` contra_subsetD empty_iff)
+
     {
     have "edom (?ae \<squnion> ae) = edom (?ce \<squnion> ce)"
       using let\<^sub>1(3) by (auto simp add: edom_cHeap)
     {
     have "edom (?ae \<squnion> ae) = edom (?ce \<squnion> ce)"
       using let\<^sub>1(3) by (auto simp add: edom_cHeap)
@@ -380,27 +389,29 @@ begin
     finally have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
     }
     moreover
     finally have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
     }
     moreover
-    
-    have "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Let \<Delta> e, restr_stack (edom ce) S)"
+
+    have "a_consistent (ae, a, as) (restrictA (- set r) \<Gamma>, Let \<Delta> e, restr_stack (- set r) S)"
       using let\<^sub>1 by auto
       using let\<^sub>1 by auto
-    hence "a_consistent (?ae \<squnion> ae, a, as) (\<Delta> @ restrictA (edom ce) \<Gamma>, e, restr_stack (edom ce) S)"
+    hence "a_consistent (?ae \<squnion> ae, a, as) (\<Delta> @ restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S)"
       using let\<^sub>1(1,2) `edom ae \<inter> domA \<Delta> = {}` 
       by (auto intro!:  a_consistent_let simp del: join_comm)
       using let\<^sub>1(1,2) `edom ae \<inter> domA \<Delta> = {}` 
       by (auto intro!:  a_consistent_let simp del: join_comm)
-    hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (edom (?ae \<squnion> ae)) (\<Delta> @ restrictA (edom ce) \<Gamma>), e, restr_stack (edom ce) S)"
-      by (rule a_consistent_restrictA[OF _ order_refl])
-    hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (edom (?ce \<squnion> ce)) (\<Delta> @ \<Gamma>), e, restr_stack (edom (?ce \<squnion> ce)) S)"
-      by (simp add: restrictA_append restr_stack_simp2[simplified] edom_cHeap `edom ce = edom ae` Int_Un_distrib2)
+    hence "a_consistent (?ae \<squnion> ae, a, as) (restrictA (- set r) (\<Delta> @ \<Gamma>), e, restr_stack (- set r) S)"
+      by (simp add: restrictA_append)
+    moreover
+    have "set r \<inter> edom ce = {}" and "upds S - edom ce \<subseteq> set r" and "set r \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
+    hence "set r \<inter> edom (?ce \<squnion> ce) = {}" and "upds S - edom (?ce \<squnion> ce) \<subseteq> set r"  and "set r \<subseteq> domA \<Gamma> \<union> upds S"
+      apply (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
+      by (metis IntI UnE `domA \<Delta> \<inter> domA \<Gamma> = {}` `domA \<Delta> \<inter> upds S = {}` contra_subsetD empty_iff)
     ultimately
     ultimately
-    have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a, as) (\<Delta> @ \<Gamma>, e, S)"
-      by auto
+    have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a, as, r) (\<Delta> @ \<Gamma>, e, S)" by auto
     }
     moreover
     {
       have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
         using fresh_distinct[OF let\<^sub>1(1)]
         by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
     }
     moreover
     {
       have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
         using fresh_distinct[OF let\<^sub>1(1)]
         by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
-      hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (edom (?ce \<squnion> ce)) \<Gamma>))
-         = map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))"
+      hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (-set r) \<Gamma>))
+         = map_transform Aeta_expand ae (map_transform transform ae (restrictA (-set r) \<Gamma>))"
          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
       moreover
   
          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
       moreover
   
@@ -408,16 +419,16 @@ begin
       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])
       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])
-      hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) (restrictA (edom (?ce \<squnion> ce)) \<Delta>))
-         = map_transform Aeta_expand ?ae (map_transform transform ?ae (restrictA (edom ?ce) \<Delta>))"
+      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)
       ultimately
       
       
          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
       ultimately
       
       
-      have "conf_transform (ae, ce, a, as) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (?ae \<squnion> ae, ?ce \<squnion> ce, a, as) (\<Delta> @ \<Gamma>, e, S)"
+      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] map_transform_restrA)
-        apply (rule let_and_restrict)
+        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])
         done
     }
         apply (auto dest: set_mp[OF edom_Aheap])
         done
     }
@@ -428,16 +439,16 @@ begin
     have "prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
     hence "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
       by (rule below_trans[OF prognosis_IfThenElse])
     have "prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
     hence "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
       by (rule below_trans[OF prognosis_IfThenElse])
-    hence "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+    hence "consistent (ae, ce, 0, a#as, r) (\<Gamma>, scrut, Alts e1 e2 # S)"
       using if\<^sub>1  by (auto dest: a_consistent_if\<^sub>1)
     moreover
       using if\<^sub>1  by (auto dest: a_consistent_if\<^sub>1)
     moreover
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+    have "conf_transform (ae, ce, a, as, r) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, a#as, r) (\<Gamma>, scrut, Alts e1 e2 # S)"
       by (auto intro: normal step.intros)
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
     case (if\<^sub>2 \<Gamma> b e1 e2 S)
       by (auto intro: normal step.intros)
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
     case (if\<^sub>2 \<Gamma> b e1 e2 S)
-    hence "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Bool b, Alts e1 e2 # restr_stack (edom ce) S)" by auto
+    hence "a_consistent (ae, a, as) (restrictA (- set r) \<Gamma>, Bool b, Alts e1 e2 # restr_stack (-set r) S)" by auto
     then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
       by (rule a_consistent_alts_on_stack)
 
     then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
       by (rule a_consistent_alts_on_stack)
 
@@ -445,22 +456,24 @@ begin
     have "prognosis ae (a'#as') 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
     hence "prognosis ae as' a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
     then
     have "prognosis ae (a'#as') 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
     hence "prognosis ae as' a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
     then
-    have "consistent (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" 
+    have "consistent (ae, ce, a', as', r) (\<Gamma>, if b then e1 else e2, S)" 
       using if\<^sub>2 by (auto dest!: a_consistent_if\<^sub>2)
     }
     moreover
       using if\<^sub>2 by (auto dest!: a_consistent_if\<^sub>2)
     }
     moreover
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)"
+    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])
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
       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
-    case refl thus ?case by auto
+    case refl thus ?case by force
   next
     case (trans c c' c'')
       from trans(3)[OF trans(5)]
   next
     case (trans c c' c'')
       from trans(3)[OF trans(5)]
-      obtain ae' ce' a' as' where "consistent (ae', ce', a', as') c'" and *: "conf_transform (ae, ce, a, as) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae', ce', a', as') c'" by blast
+      obtain ae' ce' a' as' r'
+      where "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 blast
       from trans(4)[OF this(1)]
       from trans(4)[OF this(1)]
-      obtain ae'' ce'' a'' as'' where "consistent (ae'', ce'', a'', as'') c''" and **: "conf_transform (ae', ce', a', as') c' \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae'', ce'', a'', as'') c''" by blast
+      obtain ae'' ce'' a'' as'' r''
+      where "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 blast
       from this(1) rtranclp_trans[OF * **]
       show ?case by blast
   qed
       from this(1) rtranclp_trans[OF * **]
       show ?case by blast
   qed
index c41c46a..9250313 100644 (file)
@@ -80,8 +80,54 @@ inductive boring_step where
   "isVal e \<Longrightarrow> boring_step (\<Gamma>, e, Upd x # S)"
 
 
   "isVal e \<Longrightarrow> boring_step (\<Gamma>, e, Upd x # S)"
 
 
+fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
+  where "restr_stack V [] = []"
+      | "restr_stack V (Alts e1 e2 # S) = Alts e1 e2 # restr_stack V S"
+      | "restr_stack V (Arg x # S) = Arg x # restr_stack V S"
+      | "restr_stack V (Upd x # S) = (if x \<in> V then Upd x # restr_stack V S else restr_stack V S)"
+      | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"
+
+lemma restr_stack_cong:
+  "(\<And> x. x \<in> upds S \<Longrightarrow> x \<in> V \<longleftrightarrow> x \<in> V') \<Longrightarrow> restr_stack V S = restr_stack V' S"
+  by (induction V S rule: restr_stack.induct) auto
+
+lemma upds_restr_stack[simp]: "upds (restr_stack V S) = upds S \<inter> V"
+  by (induction V S rule: restr_stack.induct) auto
+
+lemma fresh_star_restict_stack[intro]:
+  "a \<sharp>* S \<Longrightarrow> a \<sharp>* restr_stack V S"
+  by (induction V S rule: restr_stack.induct) (auto simp add: fresh_star_Cons)
+
+lemma restr_stack_restr_stack[simp]:
+  "restr_stack V (restr_stack V' S) = restr_stack (V \<inter> V') S"
+  by (induction V S rule: restr_stack.induct) auto
+
+lemma Upd_eq_restr_stackD:
+  assumes "Upd x # S = restr_stack V S'"
+  shows "x \<in> V"
+  using arg_cong[where f = upds, OF assms]
+  by auto
+lemma Upd_eq_restr_stackD2:
+  assumes "restr_stack V S' = Upd x # S"
+  shows "x \<in> V"
+  using arg_cong[where f = upds, OF assms]
+  by auto
+
+
+lemma restr_stack_noop[simp]:
+  "restr_stack V S = S \<longleftrightarrow> upds S \<subseteq> V"
+  by (induction V S rule: restr_stack.induct)
+     (auto dest: Upd_eq_restr_stackD2)
+  
+
+  
+
+
 fun heap_upds_ok where "heap_upds_ok (\<Gamma>,S) \<longleftrightarrow> domA \<Gamma> \<inter> upds S = {} \<and> distinct (upds_list S)"
 
 fun heap_upds_ok where "heap_upds_ok (\<Gamma>,S) \<longleftrightarrow> domA \<Gamma> \<inter> upds S = {} \<and> distinct (upds_list S)"
 
+abbreviation heap_upds_ok_conf :: "conf \<Rightarrow> bool"
+  where "heap_upds_ok_conf c \<equiv> heap_upds_ok (fst c, snd (snd c))"
+
 lemma heap_upds_okE: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> upds S"
   by auto
 
 lemma heap_upds_okE: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> upds S"
   by auto
 
@@ -104,6 +150,10 @@ 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)
 
   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
   by (auto)
 
+lemma heap_upds_ok_to_stack':
+  "map_of \<Gamma> x = Some e \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
+  by (metis Domain.DomainI domA_def fst_eq_Domain heap_upds_ok_to_stack map_of_is_SomeD)
+
 lemma heap_upds_ok_delete:
   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, S)"
   by auto
 lemma heap_upds_ok_delete:
   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, S)"
   by auto
@@ -112,6 +162,11 @@ lemma heap_upds_ok_restrictA:
   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (restrictA V \<Gamma>, S)"
   by auto
 
   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (restrictA V \<Gamma>, S)"
   by auto
 
+lemma heap_upds_ok_restr_stack:
+  "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>, restr_stack V S)"
+  apply auto
+  by (induction V S rule: restr_stack.induct) auto
+
 lemma heap_upds_ok_to_heap:
   "heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> heap_upds_ok ((x,e) # \<Gamma>, S)"
   by auto
 lemma heap_upds_ok_to_heap:
   "heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> heap_upds_ok ((x,e) # \<Gamma>, S)"
   by auto
@@ -120,26 +175,16 @@ lemma heap_upds_ok_reorder:
   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok ((x,e) # delete x \<Gamma>, S)"
   by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)
 
   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok ((x,e) # delete x \<Gamma>, S)"
   by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)
 
-lemmas heap_upds_ok_intros[intro] = heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_reorder heap_upds_ok_app1 heap_upds_ok_app2 heap_upds_ok_alts1 heap_upds_ok_alts2 heap_upds_ok_delete heap_upds_ok_restrictA
-lemmas heap_upds_ok.simps[simp del]
-
-fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
-  where "restr_stack V [] = []"
-      | "restr_stack V (Alts e1 e2 # S) = Alts e1 e2 # restr_stack V S"
-      | "restr_stack V (Arg x # S) = Arg x # restr_stack V S"
-      | "restr_stack V (Upd x # S) = (if x \<in> V then Upd x # restr_stack V S else restr_stack V S)"
-      | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"
-
-lemma restr_stack_cong:
-  "(\<And> x. x \<in> upds S \<Longrightarrow> x \<in> V \<longleftrightarrow> x \<in> V') \<Longrightarrow> restr_stack V S = restr_stack V' S"
-  by (induction V S rule: restr_stack.induct) auto
+lemma heap_upds_ok_upd:
+"heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> x \<notin> domA \<Gamma> \<and> x \<notin> upds S"
+  by auto
 
 
-lemma upds_restr_stack[simp]: "upds (restr_stack V S) = upds S \<inter> V"
-  by (induction V S rule: restr_stack.induct) auto
 
 
-lemma fresh_star_restict_stack[intro]:
-  "a \<sharp>* S \<Longrightarrow> a \<sharp>* restr_stack V S"
-  by (induction V S rule: restr_stack.induct) (auto simp add: fresh_star_Cons)
+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
+lemmas heap_upds_ok.simps[simp del]
 
 
 end
 
 
 end
index 3d199e4..838323c 100644 (file)
@@ -2,14 +2,13 @@ theory SestoftGC
 imports Sestoft 
 begin
 
 imports Sestoft 
 begin
 
-inductive gc_step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightarrow>\<^sub>G" 50) where
-  normal:  "c \<Rightarrow> c' \<Longrightarrow> c \<Rightarrow>\<^sub>G c'"
-| drop:    "(\<Gamma>, e, S) \<Rightarrow>\<^sub>G (restrictA V \<Gamma>, e, S)"
-| dropUpd: "(\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (\<Gamma>, e, S)"
+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)"
 
 lemmas gc_step_intros[intro] =
   normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
 
 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)] drop dropUpd
+  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>*"
 
 
 abbreviation gc_steps (infix "\<Rightarrow>\<^sub>G\<^sup>*" 50) where "gc_steps \<equiv> gc_step\<^sup>*\<^sup>*"
@@ -17,36 +16,299 @@ lemmas converse_rtranclp_into_rtranclp[of gc_step, OF _ r_into_rtranclp, trans]
 
 lemma var_onceI:
   assumes "map_of \<Gamma> x = Some e"
 
 lemma var_onceI:
   assumes "map_of \<Gamma> x = Some e"
-  shows "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e , S)"
+  shows "(r, \<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (x#r, delete x \<Gamma>, e , S)"
 proof-
   from assms 
 proof-
   from assms 
-  have "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e , Upd x # S)"..
+  have "(r, \<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (r, delete x \<Gamma>, e , Upd x # S)"..
   moreover
   moreover
-  have "\<dots> \<Rightarrow>\<^sub>G  (delete x \<Gamma>, e , S)"..
+  have "\<dots> \<Rightarrow>\<^sub>G  (x #r, delete x \<Gamma>, e , S)"..
   ultimately
   show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
 qed
 
   ultimately
   show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
 qed
 
-lemma let_and_restrict:
-  assumes "atom ` domA \<Delta> \<sharp>* \<Gamma>" and "atom ` domA \<Delta> \<sharp>* S"
-  assumes "V \<subseteq> domA \<Delta>"
-  shows "(\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G\<^sup>* (restrictA V \<Delta> @ \<Gamma>, e, S)"
+lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> (r, c) \<Rightarrow>\<^sub>G\<^sup>* (r, 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)"
+
+lemma to_gc_conf_append[simp]:
+  "to_gc_conf (r@r') c = to_gc_conf r (to_gc_conf r' c)"
+  by (cases c) auto
+
+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
+
+fun safe_hd :: "'a list \<Rightarrow> 'a option"
+ where  "safe_hd (x#_) = Some x"
+     |  "safe_hd [] = None"
+
+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)))"
+
+
+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-
 proof-
-  from assms(1,2) have "(\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G (\<Delta> @ \<Gamma>, e, S)"..
-  also
-  have "\<dots> \<Rightarrow>\<^sub>G (restrictA (V \<union> domA \<Gamma>) (\<Delta> @ \<Gamma>), e, S)"..
+  show ?thesis
+  proof(cases "isVal e")
+    case False
+    thus ?thesis using assms  by -(rule that, auto)
+  next
+    case True
+    from that assms 
+    show ?thesis
+    apply (atomize_elim)
+    proof(induction S arbitrary: \<Gamma>)
+      case Nil thus ?case by (fastforce)
+    next
+      case (Cons s S)
+      show ?case
+      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)`
+          apply auto
+          apply (intro exI conjI)
+          apply (rule rtranclp.intros(1))
+          apply auto
+          done
+      next
+        case False
+        then obtain x where [simp]: "s = Upd x" and [simp]: "x \<in> set r"
+          by(cases s) (auto split: if_splits)
+      
+        from `heap_upds_ok (\<Gamma>, s # S)` `s = Upd x`
+        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
+        from Cons.IH[OF `heap_upds_ok ((x,e) # \<Gamma>, S)`  `set r \<subseteq> domA ((x,e) # \<Gamma>) \<union> upds 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')"
+                     "(\<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
+        have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')".
+        thus ?thesis  using res by auto
+      qed
+    qed
+  qed
+qed
+  
+
+lemma sestoftUnGCstep:
+  assumes "to_gc_conf r c \<Rightarrow> 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')"
+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]
+  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
   also
-  from fresh_distinct[OF assms(1)]
-  have "restrictA (V \<union> domA \<Gamma>) \<Delta> = restrictA V \<Delta>" by (induction \<Delta>) auto
-  hence "restrictA (V \<union> domA \<Gamma>) (\<Delta> @ \<Gamma>) = restrictA V \<Delta> @ \<Gamma>"
-    by (simp add: restrictA_append restrictA_noop)
-  finally show ?thesis.
+
+  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
+  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
+  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''`
+  show ?thesis unfolding `c = _` by auto
 qed
 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')"
+using assms
+proof(induction r' "d"  rule: rtranclp_induct2)
+  case refl
+  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
 
 
-lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c \<Rightarrow>\<^sub>G\<^sup>* c'"
-  by (induction rule:rtranclp_induct) (auto dest: normal)
+    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''`
+  have "c \<Rightarrow>\<^sup>* c''" by auto
+  with `d'' = _` `heap_upds_ok_conf c''` `r_ok (r'', c'')`
+  show ?case by blast
+qed
+  
+lemma sestoftUnGC':
+  assumes "([], [], e, []) \<Rightarrow>\<^sub>G\<^sup>* (r, \<Gamma>, e', [])"
+  assumes "isVal e'"
+  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'
+  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'"
+    by auto
+  from `isVal e'` sestoftUnGCStack[where e = e', OF `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds 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' = []`
+  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
+  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
+  ultimately
+  show ?thesis by blast
+qed
 
 
 end
 
 
 end