Separate Arity consistency from Cardinality consistency
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 20 Jan 2015 14:32:01 +0000 (14:32 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Tue, 20 Jan 2015 14:32:01 +0000 (14:32 +0000)
12 files changed:
Launchbury/ArityAnalysisAbinds.thy
Launchbury/ArityAnalysisStack.thy [new file with mode: 0644]
Launchbury/ArityConsistent.thy [new file with mode: 0644]
Launchbury/ArityEtaExpandCorrect.thy
Launchbury/CallArityCorrectEnd2End.thy
Launchbury/CardinalityEtaExpandCorrect.thy
Launchbury/DeadCodeRemoval2CorrectSestoft.thy
Launchbury/Env.thy
Launchbury/SestoftConf.thy
Launchbury/SestoftCorrect.thy
Launchbury/TransformTools.thy
Launchbury/TrivialArityAnal.thy

index b86974b..d8481d1 100644 (file)
@@ -118,6 +118,13 @@ next
     by auto
 qed
 
+lemma ABinds_restr_subset: "S \<subseteq> S' \<Longrightarrow> ABinds (restrictA S \<Gamma>)\<cdot>ae \<sqsubseteq> ABinds (restrictA S' \<Gamma>)\<cdot>ae"
+  by (induct \<Gamma> rule: ABinds.induct)
+     (auto simp add: join_below_iff  restr_delete_twist intro: below_trans[OF _ join_above2])
+
+lemma ABinds_restrict_edom: "ABinds (restrictA (edom ae) \<Gamma>)\<cdot>ae = ABinds \<Gamma>\<cdot>ae"
+  by (induct \<Gamma> rule: ABinds.induct) (auto simp add: edom_def restr_delete_twist)
+  
 lemma ABinds_restrict_below: "ABinds (restrictA S \<Gamma>)\<cdot>ae \<sqsubseteq> ABinds \<Gamma>\<cdot>ae"
   by (induct \<Gamma> rule: ABinds.induct)
      (auto simp add: join_below_iff  restr_delete_twist intro: below_trans[OF _ join_above2] simp del: fun_meet_simp join_comm)
diff --git a/Launchbury/ArityAnalysisStack.thy b/Launchbury/ArityAnalysisStack.thy
new file mode 100644 (file)
index 0000000..243cab5
--- /dev/null
@@ -0,0 +1,22 @@
+theory ArityAnalysisStack
+imports "SestoftConf" "ArityAnalysisSig"
+begin
+
+context ArityAnalysis
+begin
+  fun AEstack :: "Arity list \<Rightarrow> stack \<Rightarrow> AEnv"
+    where 
+      "AEstack _ [] = \<bottom>"
+    | "AEstack (a#as) (Alts e1 e2 # S) = Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a \<squnion> AEstack as S"
+    | "AEstack as (Upd x # S) = esing x\<cdot>(up\<cdot>0) \<squnion> AEstack as S"
+    | "AEstack as (Arg x # S) = esing x\<cdot>(up\<cdot>0) \<squnion> AEstack as S"
+    | "AEstack as (_ # S) = AEstack as S"
+end
+
+context EdomArityAnalysis
+begin
+  lemma edom_AEstack: "edom (AEstack as S) \<subseteq> fv S"
+    by (induction as S rule: AEstack.induct) (auto simp del: fun_meet_simp dest!: set_mp[OF Aexp_edom])
+end
+
+end
diff --git a/Launchbury/ArityConsistent.thy b/Launchbury/ArityConsistent.thy
new file mode 100644 (file)
index 0000000..e14d025
--- /dev/null
@@ -0,0 +1,269 @@
+theory ArityConsistent
+imports  CardinalityAnalysisSpec ArityStack ArityAnalysisStack
+begin
+
+context CorrectArityAnalysisLet
+begin
+
+type_synonym astate = "(AEnv \<times> Arity \<times> Arity list)"
+
+inductive stack_consistent :: "Arity list \<Rightarrow> stack \<Rightarrow> bool"
+  where 
+    "stack_consistent [] []"
+  | "Astack S \<sqsubseteq> a \<Longrightarrow> stack_consistent as S \<Longrightarrow> stack_consistent (a#as) (Alts e1 e2 # S)"
+  | "stack_consistent as S \<Longrightarrow> stack_consistent as (Upd x # S)"
+  | "stack_consistent as S \<Longrightarrow> stack_consistent as (Arg x # S)"
+inductive_simps stack_consistent_foo[simp]:
+  "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)"
+inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"
+
+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
+  \<Longrightarrow> a_consistent (ae, a, as) (\<Gamma>, e, S)"  
+inductive_cases a_consistentE: "a_consistent (ae, a, as) (\<Gamma>, e, S)"
+
+lemma a_consistent_restrictA:
+  assumes "a_consistent (ae, a, as) (\<Gamma>, e, S)"
+  assumes "edom ae \<subseteq> V"
+  shows "a_consistent (ae, a, as) (restrictA V \<Gamma>, e, S)"
+proof-
+  have "domA \<Gamma> \<inter> V \<union> upds S \<subseteq> domA \<Gamma> \<union> upds S" by auto
+  note * = below_trans[OF env_restr_mono2[OF this]]
+  
+  show " a_consistent (ae, a, as) (restrictA V \<Gamma>, e, S)"
+    using assms
+    by (auto simp add: a_consistent.simps env_restr_join join_below_iff ABinds_restrict_edom
+                  intro: * below_trans[OF env_restr_mono[OF ABinds_restrict_below]])
+qed
+
+lemma a_consistent_edom_subsetD:
+  "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> edom ae \<subseteq> domA \<Gamma> \<union> upds S"
+  by (rule a_consistentE)
+
+lemma a_consistent_stackD:
+  "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> Astack S \<sqsubseteq> a"
+  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)"
+  by (auto simp add: join_below_iff env_restr_join a_consistent.simps
+           dest!: below_trans[OF env_restr_mono[OF Aexp_App]]
+           elim: below_trans)
+
+lemma a_consistent_app\<^sub>2:
+  assumes "a_consistent (ae, a, as) (\<Gamma>, (Lam [y]. e), Arg x # S)"
+  shows "a_consistent (ae, (pred\<cdot>a), as) (\<Gamma>, e[y::=x], S)"
+proof-
+  have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` (domA \<Gamma> \<union> upds S)  \<sqsubseteq> (env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<squnion> esing x\<cdot>(up\<cdot>0)) f|` (domA \<Gamma> \<union> upds S)" by (rule env_restr_mono[OF Aexp_subst])
+  also have "\<dots> =  env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) f|` (domA \<Gamma> \<union> upds S) \<squnion> esing x\<cdot>(up\<cdot>0) f|` (domA \<Gamma> \<union> upds S)" by (simp add: env_restr_join)
+  also have "env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<sqsubseteq> Aexp (Lam [y]. e)\<cdot>a" by (rule Aexp_Lam)
+  also have "\<dots> f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" using assms  by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
+  also have "esing x\<cdot>(up\<cdot>0) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" using assms
+    by (cases "x\<in>edom ae") (auto simp add: env_restr_join join_below_iff a_consistent.simps)
+  also have "ae \<squnion> ae = ae" by simp
+  finally
+  have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by this simp_all
+  thus ?thesis using assms
+    by (auto elim: below_trans edom_mono  simp add: join_below_iff env_restr_join a_consistent.simps)
+qed
+
+lemma a_consistent_thunk_0:
+  assumes "a_consistent (ae, a, as) (\<Gamma>, Var x, S)"
+  assumes "map_of \<Gamma> x = Some e"
+  assumes "ae x = up\<cdot>0"
+  shows "a_consistent (ae, 0, as) (delete x \<Gamma>, e, Upd x # S)"
+proof-
+  from assms(2)
+  have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
+
+  from assms(3)
+  have [simp]: "x \<in> edom ae" by (auto simp add: edom_def)
+
+  have "x \<in> domA \<Gamma>" by (metis assms(2) domI dom_map_of_conv_domA)
+  hence [simp]: "insert x (domA \<Gamma> - {x} \<union> upds S)  = (domA \<Gamma> \<union> upds S)"
+    by auto
+
+  from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>0`
+  have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>0 = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
+  moreover have "(\<dots> \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
+    using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
+  ultimately have "((ABinds (delete x \<Gamma>))\<cdot>ae \<squnion> Aexp e\<cdot>0 \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by simp
+  then
+  show ?thesis
+     using `ae x = up\<cdot>0` assms(1)
+     by (auto simp add: join_below_iff env_restr_join  a_consistent.simps)
+qed
+
+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"
+  shows "a_consistent (env_delete x ae, u, as) (delete x \<Gamma>, e, S)"
+proof-
+  from assms(2)
+  have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
+
+  from assms(1) have "Aexp (Var x)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
+  from fun_belowD[where x = x, OF this] 
+  have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> up\<cdot>u" by simp
+  from below_trans[OF Aexp_Var this]
+  have "a \<sqsubseteq> u" by simp
+
+  from assms(1)
+  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
+
+  have "Astack S \<sqsubseteq> u" using assms(1) `a \<sqsubseteq> u`
+    by (auto elim: below_trans simp add: a_consistent.simps)
+  
+  from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
+  have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
+  moreover
+  have "(\<dots> \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
+    using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
+  ultimately
+  have "((ABinds (delete x \<Gamma>))\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by simp
+  hence "((ABinds (delete x \<Gamma>))\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
+    by (auto simp add: join_below_iff env_restr_join elim:  below_trans[OF env_restr_mono[OF monofun_cfun_arg[OF env_delete_below_arg]]])
+  hence "env_delete x (((ABinds (delete x \<Gamma>))\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S)) \<sqsubseteq> env_delete x ae"
+    by (rule env_delete_mono)
+  hence "(((ABinds (delete x \<Gamma>))\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA (delete x \<Gamma>) \<union> upds S)) \<sqsubseteq> env_delete x ae"
+    by (simp add: env_delete_restr)
+  then
+  show ?thesis
+     using `ae x = up\<cdot>u` `Astack S \<sqsubseteq> u` assms(1)
+     by (auto simp add: join_below_iff env_restr_join  a_consistent.simps elim : below_trans)
+qed
+
+lemma a_consistent_lamvar:
+  assumes "a_consistent (ae, a, as) (\<Gamma>, Var x, S)"
+  assumes "map_of \<Gamma> x = Some e"
+  assumes [simp]: "ae x = up\<cdot>u"
+  shows "a_consistent (ae, u, as) ((x,e)# delete x \<Gamma>, e, S)"
+proof-
+  have [simp]: "x \<in> domA \<Gamma>" by (metis assms(2) domI dom_map_of_conv_domA)
+  have [simp]: "insert x (domA \<Gamma> \<union> upds S) = (domA \<Gamma> \<union> upds S)" 
+    by auto
+
+  from assms(1) have "Aexp (Var x)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
+  from fun_belowD[where x = x, OF this] 
+  have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> up\<cdot>u" by simp
+  from below_trans[OF Aexp_Var this]
+  have "a \<sqsubseteq> u" by simp
+
+  have "Astack S \<sqsubseteq> u" using assms(1) `a \<sqsubseteq> u`
+    by (auto elim: below_trans simp add: a_consistent.simps)
+  
+  from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
+  have "ABinds ((x,e) # delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
+  moreover
+  have "(\<dots> \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
+    using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
+  ultimately
+  have "((ABinds ((x,e) # delete x \<Gamma>))\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by simp
+  then
+  show ?thesis
+     using `ae x = up\<cdot>u` `Astack S \<sqsubseteq> u` assms(1)
+     by (auto simp add: join_below_iff env_restr_join  a_consistent.simps)
+qed
+
+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
+    by (auto simp add: join_below_iff env_restr_join a_consistent.simps 
+               elim:below_trans[OF env_restr_mono[OF ABinds_delete_below]])
+
+lemma a_consistent_let:
+  assumes "a_consistent (ae, a, as) (\<Gamma>, Let \<Delta> e, S)"
+  assumes "atom ` domA \<Delta> \<sharp>* \<Gamma>"
+  assumes "atom ` domA \<Delta> \<sharp>* S"
+  assumes "edom ae \<inter> domA \<Delta> = {}"
+  shows "a_consistent (Aheap \<Delta> e\<cdot>a \<squnion> ae, a, as) (\<Delta> @ \<Gamma>, e, S)"
+proof-
+  txt {*
+    First some boring stuff about scope:
+  *}
+  
+  have [simp]: "\<And> S. S \<subseteq> domA \<Delta> \<Longrightarrow> ae f|` S = \<bottom>" using assms(4) by auto
+  have [simp]: "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)"
+    by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
+
+  have [simp]: "Aheap \<Delta> e\<cdot>a f|` domA \<Gamma> = \<bottom>"
+    using fresh_distinct[OF assms(2)]
+    by (auto intro: env_restr_empty dest!: set_mp[OF edom_Aheap])
+
+  have [simp]: "ABinds \<Gamma>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Gamma>\<cdot>ae"
+    by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
+
+  have [simp]: "ABinds \<Gamma>\<cdot>ae f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S)  = ABinds \<Gamma>\<cdot>ae f|` (domA \<Gamma> \<union> upds S)" 
+    using fresh_distinct_fv[OF assms(2)]
+    by (auto intro: env_restr_cong dest!: set_mp[OF edom_AnalBinds])
+
+  have [simp]: "AEstack as S f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S) = AEstack as S f|` (domA \<Gamma> \<union> upds S)" 
+    using fresh_distinct_fv[OF assms(3)]
+    by (auto intro: env_restr_cong dest!:  set_mp[OF edom_AEstack])
+
+  have [simp]: "Aexp (Let \<Delta> e)\<cdot>a f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S) = Aexp (Terms.Let \<Delta> e)\<cdot>a f|` (domA \<Gamma> \<union> upds S)"
+    by (rule env_restr_cong) (auto dest!: set_mp[OF Aexp_edom])
+  
+  have [simp]: "Aheap \<Delta> e\<cdot>a f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S) = Aheap \<Delta> e\<cdot>a "
+    by (rule env_restr_useless) (auto dest!: set_mp[OF edom_Aheap])
+
+  have "((ABinds \<Gamma>)\<cdot>ae \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
+  moreover
+  have" Aexp (Let \<Delta> e)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"  using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
+  moreover
+  have "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a" by (rule Aexp_Let)
+  ultimately
+  have "(ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` (domA (\<Delta>@\<Gamma>) \<union> upds S) \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> ae"
+    by (auto 4 4 simp add: env_restr_join Abinds_append_disjoint[OF fresh_distinct[OF assms(2)]] join_below_iff
+                 simp del: join_comm
+                 elim: below_trans below_trans[OF env_restr_mono])
+  moreover
+  note fresh_distinct[OF assms(2)]
+  moreover
+  from fresh_distinct_fv[OF assms(3)]
+  have  "domA \<Delta> \<inter> upds S = {}" by (auto dest!: set_mp[OF ups_fv_subset])
+  ultimately
+  show ?thesis using assms(1)
+    by (auto simp add: a_consistent.simps dest!: set_mp[OF edom_Aheap] intro: heap_upds_ok_append)
+qed
+
+lemma a_consistent_if\<^sub>1:
+  assumes "a_consistent (ae, a, as) (\<Gamma>, scrut ? e1 : e2, S)"
+  shows "a_consistent (ae, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+proof-
+  from assms
+  have "Aexp (scrut ? e1 : e2)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by (auto simp add: a_consistent.simps env_restr_join join_below_iff)
+  hence "(Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
+    by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]])
+  thus ?thesis
+    using assms
+    by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
+qed
+
+lemma a_consistent_if\<^sub>2:
+  assumes "a_consistent (ae, a, a'#as') (\<Gamma>, Bool b, Alts e1 e2 # S)"
+  shows "a_consistent (ae, a', as') (\<Gamma>, if b then e1 else e2, S)"
+using assms by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
+
+lemma a_consistent_alts_on_stack:
+  assumes "a_consistent (ae, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S)"
+  obtains a' as' where "as = a' # as'" "a = 0"
+using assms by (auto simp add: a_consistent.simps)
+
+lemma closed_a_consistent:
+  "fv e = ({}::var set) \<Longrightarrow> a_consistent (\<bottom>, 0, []) ([], e, [])"
+  by (auto simp add: edom_empty_iff_bot a_consistent.simps  dest!: set_mp[OF Aexp_edom])
+
+end
+
+end
index 74cc60e..66a3e18 100644 (file)
@@ -1,16 +1,16 @@
 theory ArityEtaExpandCorrect
-imports ArityEtaExpand  ArityAnalysisSpec ArityEtaExpansionSestoft AbstractTransform ConstOn
+imports ArityEtaExpand ArityConsistent ArityAnalysisSpec ArityEtaExpansionSestoft AbstractTransform ConstOn
 begin
 
 locale CardinalityArityTransformation = CorrectArityAnalysisLetNoCard
 begin
-
   sublocale AbstractTransformBoundSubst
     "\<lambda> a . inc\<cdot>a"
     "\<lambda> a . pred\<cdot>a"
     "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
     "fst"
     "snd"
+    "\<lambda> _. 0"
     "Aeta_expand"
     "snd"
   apply default
@@ -18,7 +18,7 @@ begin
   apply (rule subst_Aeta_expand)
   done
 
-  abbreviation aTransform where "aTransform \<equiv> transform"
+  abbreviation ccTransform where "ccTransform \<equiv> transform"
 
   lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
     by (induction rule: transform.induct)
@@ -26,249 +26,251 @@ begin
   interpretation supp_bounded_transform transform
     by default (auto simp add: fresh_def supp_transform) 
 
-  fun conf_transform :: "(AEnv \<times> Arity) \<Rightarrow> conf \<Rightarrow> conf"
-  where "conf_transform (ae,  a) (\<Gamma>, e, S) =
-    (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>), 
-     transform a e,
-     S)"
+  fun transform_alts :: "Arity list \<Rightarrow> stack \<Rightarrow> stack"
+    where 
+      "transform_alts _ [] = []"
+    | "transform_alts (a#as) (Alts e1 e2 # S) = (Alts (ccTransform a e1) (ccTransform a e2)) # transform_alts as S"
+    | "transform_alts as (x # S) = x # transform_alts as S"
+
+  lemma transform_alts_Nil[simp]: "transform_alts [] S = S"
+    by (induction  S) auto
+
+  lemma Astack_transform_alts[simp]:
+    "Astack (transform_alts as S) = Astack S"
+   by (induction rule: transform_alts.induct) auto
+
+  lemma fresh_star_transform_alts[intro]: "a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S"
+   by (induction as S  rule: transform_alts.induct) (auto simp add: fresh_star_Cons)
 
-  inductive consistent :: "(AEnv \<times> Arity) \<Rightarrow> conf \<Rightarrow> bool" where
+  fun a_transform :: "astate \<Rightarrow> conf \<Rightarrow> conf"
+  where "a_transform (ae, a, as) (\<Gamma>, e, S) =
+    (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>), 
+     ccTransform a e,
+     transform_alts as  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)"
+
+  inductive consistent :: "astate \<Rightarrow> conf \<Rightarrow> bool" where
     consistentI[intro!]: 
-    "edom ae \<subseteq> domA \<Gamma> \<union> upds S
+    "a_consistent (ae, a, as) (\<Gamma>, e, S)
     \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
-    \<Longrightarrow> Astack S \<sqsubseteq> a
-    \<Longrightarrow> ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a \<sqsubseteq> ae
-    \<Longrightarrow> const_on ae (thunks \<Gamma>) (up\<cdot>0)
-    \<Longrightarrow> const_on ae (ap S) (up\<cdot>0)
-    \<Longrightarrow> const_on ae (upds S) (up\<cdot>0)
-    \<Longrightarrow> consistent (ae, a) (\<Gamma>, e, S)"  
-  inductive_cases consistentE[elim!]: "consistent (ae, a) (\<Gamma>, e, S)"
-  
+    \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow>  ae x = up\<cdot>0)
+    \<Longrightarrow> consistent (ae, a, as) (\<Gamma>, e, S)"  
+  inductive_cases consistentE[elim!]: "consistent (ae, a, as) (\<Gamma>, e, S)"
+
+  lemma closed_consistent:
+    assumes "fv e = ({}::var set)"
+    shows "consistent (\<bottom>, 0, []) ([], e, [])"
+  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) c"
-    shows "\<exists>ae' ce' a'. consistent (ae',a') c' \<and> conf_transform (ae,a) c \<Rightarrow>\<^sup>* conf_transform (ae',a') c'"
+    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step 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 rule:step_induction)
+  proof(induction c c' arbitrary: ae a as rule:step_induction)
   case (app\<^sub>1 \<Gamma> e x S)
-    from app\<^sub>1 have "consistent (ae, inc\<cdot>a) (\<Gamma>, e, Arg x # S)"
-      by (auto simp add: join_below_iff  dest!: below_trans[OF Aexp_App] elim: below_trans)
+    from app\<^sub>1 have "consistent (ae, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
+      by (auto intro: a_consistent_app\<^sub>1)
     moreover
-    have "conf_transform (ae, a) (\<Gamma>, App e x, S) \<Rightarrow> conf_transform (ae, inc\<cdot>a) (\<Gamma>, e, Arg x # S)"
+    have "a_transform (ae, a, as) (\<Gamma>, App e x, S) \<Rightarrow> a_transform (ae, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
       by simp rule
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
-case (app\<^sub>2 \<Gamma> y e x S)
-  {
-  have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) \<sqsubseteq> env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<squnion> esing x\<cdot>(up\<cdot>0)" by (rule Aexp_subst)
-  also have "env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<sqsubseteq> Aexp (Lam [y]. e)\<cdot>a" by (rule Aexp_Lam)
-  also have "\<dots> \<sqsubseteq> ae" using app\<^sub>2 by (auto simp add: join_below_iff)
-  also have "esing x\<cdot>(up\<cdot>0) \<sqsubseteq> ae" using app\<^sub>2 by auto
-  also have "ae \<squnion> ae = ae" by simp
-  finally  have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) \<sqsubseteq> ae" by this simp_all
-  }
-  then
-  have "consistent (ae, pred\<cdot>a) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
-    by (auto elim: below_trans edom_mono  simp add: join_below_iff)
-  moreover
-  have "conf_transform (ae, a) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow> conf_transform (ae, pred \<cdot> a) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
-  ultimately
-  show ?case by (blast  del: consistentI consistentE)
-next
-case (thunk \<Gamma> x e S)
-  hence "x \<in> thunks \<Gamma>" by auto
-  hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
-  hence "x \<notin> upds S" using thunk by (auto elim!: heap_upds_okE)
-
-  from thunk have "Aexp (Var x)\<cdot>a \<sqsubseteq> ae" by (auto simp add: join_below_iff)
-  from below_trans[OF Aexp_Var fun_belowD[OF this] ]
-  have "up\<cdot>a \<sqsubseteq> ae x".    
-  then obtain u where "ae x = up\<cdot>u" and "a \<sqsubseteq> u" by (cases "ae x") auto
-  hence [simp]: "x \<in> edom ae" by (simp add: edom_def)
-
-  have "ae x = up\<cdot>0" using thunk `x \<in> thunks \<Gamma>` by (auto)
-  hence "u = 0" using `ae x = up\<cdot>u` by simp
-
+  case (app\<^sub>2 \<Gamma> y e x S)
+    have "consistent (ae, pred\<cdot>a, as) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
+      by (auto 4 3 intro: a_consistent_app\<^sub>2)
+    moreover
+    have "a_transform (ae, a, as) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow> a_transform (ae, pred \<cdot> a, as) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
+    ultimately
+    show ?case by (blast  del: consistentI consistentE)
+  next
+  case (thunk \<Gamma> x e S)
+    hence "x \<in> thunks \<Gamma>" by auto
+    hence [simp]: "x \<in> domA \<Gamma>" by (rule set_mp[OF thunks_domA])
+    hence "x \<notin> upds S" using thunk by (auto elim!: heap_upds_okE)
+    
+    have "x \<in> edom ae" using thunk by auto
   
-  from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
-  have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by auto
-  also have "\<dots> \<sqsubseteq> ae" using thunk by (auto simp add: join_below_iff)
-  finally have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u \<sqsubseteq> ae".
-  hence "consistent (ae, 0) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`
-    by (auto intro!: const_onI)
-  moreover
-
-  from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0`
-  have "map_of (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)) x = Some (transform 0 e)"
-    by (simp add: map_of_map_transform)
-  with `\<not> isVal e`
-  have "conf_transform (ae, a) (\<Gamma>, Var x, S) \<Rightarrow> conf_transform (ae, 0) (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 ?case by (blast del: consistentI consistentE)
-next
-case (lamvar \<Gamma> x e S)
-  from lamvar have [simp]: "x \<in> domA \<Gamma>" by auto (metis domI dom_map_of_conv_domA)
-  from lamvar have "Aexp (Var x)\<cdot>a \<sqsubseteq> ae" by (auto simp add: join_below_iff)
-  from below_trans[OF Aexp_Var fun_belowD[OF this] ]
-  have "up\<cdot>a \<sqsubseteq> ae x".
-  then obtain u where "ae x = up\<cdot>u" and "a \<sqsubseteq> u" by (cases "ae x") auto
-
-  from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
-  have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by auto
-  also have "\<dots> \<sqsubseteq> ae" using lamvar by (auto simp add: join_below_iff)
-  finally have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u \<sqsubseteq> ae".
-
-  have "consistent (ae, u) ((x, e) # delete x \<Gamma>, e, S)"
-    using lamvar `ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u \<sqsubseteq> ae`  `ae x = up\<cdot>u` 
-    by (auto simp add: join_below_iff thunks_Cons split:if_splits intro: below_trans[OF _ `a \<sqsubseteq> u`] intro!: const_onI)
-  moreover
-
-  have "Astack S \<sqsubseteq> u" using lamvar  below_trans[OF _ `a \<sqsubseteq> u`] by auto
-
-  {
-  from `isVal e`
-  have "isVal (transform u e)" by simp
-  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`  `isVal (transform u e)`
-  have "map_of (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)) x = Some (Aeta_expand u (transform u e))"
-    by (simp add: map_of_map_transform)
-  ultimately
-  have "conf_transform (ae, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>*
-        ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)), Aeta_expand u  (transform u e), 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 \<Gamma>))), Aeta_expand u (transform u e), S)"
-    using `ae x = up \<cdot> u` `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, u) ((x, e) # delete x \<Gamma>, e, S)"
-    by simp (rule Aeta_expand_correct[OF `Astack S \<sqsubseteq> u`])
-  finally(rtranclp_trans)
-  have "conf_transform (ae, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* conf_transform (ae, u) ((x, e) # delete x \<Gamma>, e, S)".
-  }
-  ultimately show ?case by (blast del: consistentI consistentE)
-next
-case (var\<^sub>2 \<Gamma> x e S)
-
-  have "ae x = up\<cdot>a" using var\<^sub>2 by auto
+    have "ae x = up\<cdot>0" using thunk `x \<in> thunks \<Gamma>` by (auto)
 
-  have "Astack (Upd x # S) \<sqsubseteq> a" using var\<^sub>2 by auto
-  hence "a = 0" by auto
+    have "a_consistent (ae, 0, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>0`
+      by (auto intro!: a_consistent_thunk_0 simp del: restr_delete)
+    hence "consistent (ae, 0, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>0` 
+      by (auto simp add:  restr_delete_twist)
+    moreover
+  
+    from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0`
+    have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)) x = Some (transform 0 e)"
+      by (simp add: map_of_map_transform)
+    with `\<not> isVal e`
+    have "a_transform (ae, a, as) (\<Gamma>, Var x, S) \<Rightarrow> a_transform (ae, 0, as) (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 ?case by (blast del: consistentI consistentE)
+  next
+  case (lamvar \<Gamma> x e S)
+    from lamvar(1) have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
 
-  have "consistent (ae, 0) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
-    by (auto simp add: join_below_iff thunks_Cons split:if_splits)
-  moreover
-  have "conf_transform (ae, a) (\<Gamma>, e, Upd x # S) \<Rightarrow> conf_transform (ae, 0) ((x, e) # \<Gamma>, e, S)"
-    using `ae x = up\<cdot>a` `a = 0` var\<^sub>2
-    by (auto intro!: step.intros simp add: map_transform_Cons)
-  ultimately show ?case by (blast del: consistentI consistentE)
-next
-  case (let\<^sub>1 \<Delta> \<Gamma> e S)
+    have "up\<cdot>a \<sqsubseteq> (Aexp (Var x)\<cdot>a f|` (domA \<Gamma> \<union> upds S)) x"
+      by (simp) (rule Aexp_Var)
+    also from lamvar have "Aexp (Var x)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
+    finally
+    obtain u where "ae x = up\<cdot>u" by (cases "ae x") (auto simp add: edom_def)
+    hence "x \<in> edom ae" by (auto simp add: edomIff)
 
-  let ?ae = "Aheap \<Delta> e\<cdot>a"
-  let ?new = "(domA (\<Delta> @ \<Gamma>) \<union> upds S - (domA \<Gamma> \<union> upds S))"
-  have new: "?new = domA \<Delta>"
-    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 "a_consistent (ae, u, as) ((x,e) # delete x \<Gamma>, e, S)" using lamvar `ae x = up\<cdot>u`
+      by (auto intro!: a_consistent_lamvar simp del: restr_delete)
+    hence "consistent (ae, u, as) ((x, e) # delete x \<Gamma>, e, S)"
+      using lamvar by (auto simp add:  thunks_Cons restr_delete_twist elim: below_trans)
+    moreover
 
-  have "domA \<Delta> \<inter> upds S = {}" using fresh_distinct_fv[OF let\<^sub>1(2)] by (auto dest: set_mp[OF ups_fv_subset])
-  hence *: "\<And> x. x \<in> upds S \<Longrightarrow> x \<notin> edom ?ae" by (auto dest!: set_mp[OF edom_Aheap])
+    from `a_consistent _ _`
+    have "Astack (transform_alts as S) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
+  
+    {
+    from `isVal e`
+    have "isVal (transform u e)" by simp
+    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`  `isVal (transform u e)`
+    have "map_of (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)) x = Some (Aeta_expand u (transform u e))"
+      by (simp add: map_of_map_transform)
+    ultimately
+    have "a_transform (ae, 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 \<Gamma>)), Aeta_expand u (transform u e), transform_alts as S)"
+       by (auto intro: lambda_var simp del: restr_delete)
+    also have "\<dots> = ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x \<Gamma>))), Aeta_expand u (transform u e), transform_alts as S)"
+      using `ae x = up \<cdot> u` `isVal (transform u e)`
+      by (simp add: map_transform_Cons map_transform_delete  del: restr_delete)
+    also(subst[rotated]) have "\<dots> \<Rightarrow>\<^sup>* a_transform (ae, u, as) ((x, e) # delete x \<Gamma>, e, S)"
+      by (simp add: restr_delete_twist) (rule Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`])
+    finally(rtranclp_trans)
+    have "a_transform (ae, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* a_transform (ae, u, as) ((x, e) # delete x \<Gamma>, e, S)".
+    }
+    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)
 
-  have restr_stack_simp: "restr_stack (edom (?ae \<squnion> ae)) S = restr_stack (edom ae) S"
-    by (auto intro: restr_stack_cong dest!: *)
+    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`]
+    have "ae x = up\<cdot>0" and "a = 0".
 
-  have "edom ae \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
-  from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
-  have [simp]: "ae f|` domA \<Delta> = \<bottom>"
-    using  fresh_distinct[OF let\<^sub>1(1)] by (auto dest: set_mp[OF ups_fv_subset])
+    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)
+    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)
+    moreover
+    have "a_transform (ae, a, as) (\<Gamma>, e, Upd x # S) \<Rightarrow> a_transform (ae, 0, as) ((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 ?case by (blast del: consistentI consistentE)
+  next
+    case (let\<^sub>1 \<Delta> \<Gamma> e S)
+    let ?ae = "Aheap \<Delta> e\<cdot>a"
+  
+    have "domA \<Delta> \<inter> upds S = {}" using fresh_distinct_fv[OF let\<^sub>1(2)] by (auto dest: set_mp[OF ups_fv_subset])
+    hence *: "\<And> x. x \<in> upds S \<Longrightarrow> x \<notin> edom ?ae" by (auto simp add:  dest!: set_mp[OF edom_Aheap])
+    have restr_stack_simp2: "restr_stack (edom (?ae \<squnion> ae)) S = restr_stack (edom ae) S"
+      by (auto intro: restr_stack_cong dest!: *)
 
-  from  fresh_distinct[OF let\<^sub>1(1)]
-   have [simp]: "?ae f|` domA \<Gamma> = \<bottom>" by (auto dest!: set_mp[OF edom_Aheap])
+    have "edom ae \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by (auto dest!: a_consistent_edom_subsetD)
+    from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
+    have "edom ae \<inter> domA \<Delta> = {}" by (auto dest: set_mp[OF ups_fv_subset])
 
-  {
-  have "edom (?ae \<squnion> ae) \<subseteq> domA (\<Delta> @ \<Gamma>) \<union> upds S"
-    using let\<^sub>1(3) by (auto dest: set_mp[OF edom_Aheap])
-  moreover
-  have "const_on (?ae \<squnion> ae) (thunks \<Gamma>) (up\<cdot>0)" using let\<^sub>1 by fastforce
-  moreover
-  { fix x e'
-    assume "x \<in> thunks \<Delta>" 
-    hence "x \<notin> domA \<Gamma>" and "x \<notin> upds S"
-      using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
-      by (auto dest!: set_mp[OF thunks_domA] set_mp[OF ups_fv_subset])
-    hence "(?ae \<squnion> ae) x = up \<cdot> 0" using `x \<in> thunks \<Delta>` by (auto simp add: Aheap_heap3)
-  }
-  hence "const_on (?ae \<squnion> ae) (thunks \<Delta>) (up\<cdot>0)" by auto
-  moreover
-  have "const_on ae (ap S) (up\<cdot>0)" using let\<^sub>1 by auto  
-  hence "const_on (?ae \<squnion> ae) (ap S) (up\<cdot>0)" by fastforce
-  moreover
-  have "const_on ae (upds S) (up\<cdot>0)" using let\<^sub>1 by auto
-  hence "const_on (?ae \<squnion> ae) (upds S) (up\<cdot>0)"  by fastforce
-  moreover
-  have "Astack S \<sqsubseteq> a" unfolding restr_stack_simp using let\<^sub>1 by auto
-  moreover
-  have "heap_upds_ok (\<Gamma>, S)" using let\<^sub>1 by auto
-  with fresh_distinct[OF let\<^sub>1(1)]  `domA \<Delta> \<inter> upds S = {}`
-  have "heap_upds_ok (\<Delta> @ \<Gamma>, S)" by (rule heap_upds_ok_append)
-  moreover
-  {
-  have "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)"
-    by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
-  moreover
-  have "ABinds \<Gamma>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Gamma>\<cdot>ae"
-    by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
-  ultimately
-  have "ABinds (\<Delta> @ \<Gamma>) \<cdot> (Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a = (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a) \<squnion> ABinds \<Gamma>\<cdot>ae"
-    by (simp add: Abinds_append_disjoint[OF fresh_distinct[OF let\<^sub>1(1)]])
-  also have "\<dots> \<sqsubseteq> (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a) \<squnion> ABinds \<Gamma>\<cdot>ae" by (rule join_mono[OF Aexp_Let below_refl])
-  also have "\<dots> = Aheap \<Delta> e\<cdot>a \<squnion> (Aexp (Let \<Delta> e)\<cdot>a \<squnion> ABinds \<Gamma>\<cdot>ae)" by simp
-  also have "Aexp (Let \<Delta> e)\<cdot>a \<squnion> ABinds \<Gamma>\<cdot>ae \<sqsubseteq> ae" using let\<^sub>1 by auto
-  finally
-  have "ABinds (\<Delta> @ \<Gamma>) \<cdot> (Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> ae"  by this simp
-  }
-  ultimately
-  have "consistent (?ae \<squnion> ae, a) (\<Delta> @ \<Gamma>, e, S) " by auto
-  }
-  moreover
-  {
-    have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae"
-      using fresh_distinct[OF let\<^sub>1(1)]
-      by (auto dest!: set_mp[OF edom_Aheap])
-    hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) \<Gamma>)
-       = map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)"
-       by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
+    {
+    { fix x e'
+      assume "x \<in> thunks \<Gamma>"
+      with let\<^sub>1
+      have "(?ae \<squnion> ae) x = up\<cdot>0" by auto
+    }
     moreover
-
-    from let\<^sub>1 have *: "edom ae \<subseteq> domA \<Gamma> \<union> upds S" by auto
-    have "\<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 *] set_mp[OF ups_fv_subset])
-    hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) \<Delta>)
-       = map_transform Aeta_expand ?ae (map_transform transform ?ae \<Delta>)"
-       by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
+    { fix x e'
+      assume "x \<in> thunks \<Delta>" 
+      hence "(?ae \<squnion> ae) x = up\<cdot>0" by (auto simp add: Aheap_heap3)
+    }
+    moreover
+    have "heap_upds_ok (\<Gamma>, S)" using let\<^sub>1 by auto
+    with fresh_distinct[OF let\<^sub>1(1)]  `domA \<Delta> \<inter> upds S = {}`
+    have "heap_upds_ok (\<Delta> @ \<Gamma>, S)" by (rule heap_upds_ok_append)
+    moreover
+    
+    have "a_consistent (ae, a, as) (\<Gamma>, Let \<Delta> e, S)"
+      using let\<^sub>1 by auto
+    hence "a_consistent (?ae \<squnion> ae, a, as) (\<Delta> @ \<Gamma>, e, S)"
+      using let\<^sub>1(1,2) `edom ae \<inter> domA \<Delta> = {}` 
+      by (auto intro!:  a_consistent_let simp del: join_comm)
     ultimately
+    have "consistent (?ae \<squnion> ae, a, as) (\<Delta> @ \<Gamma>, e, S)"
+      by auto
+    }
+    moreover
+    {
+      have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae"
+        using fresh_distinct[OF let\<^sub>1(1)]
+        by (auto dest!: set_mp[OF edom_Aheap])
+      hence "map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) \<Gamma>)
+         = map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)"
+         by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
+      moreover
+  
+      from `edom ae \<subseteq> domA \<Gamma> \<union> upds S`
+      have  "\<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) \<Delta>)
+         = map_transform Aeta_expand ?ae (map_transform transform ?ae \<Delta>)"
+         by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
+      ultimately
+      
+      
+      have "a_transform (ae, a, as) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow> a_transform (?ae \<squnion> ae,  a, as) (\<Delta> @ \<Gamma>, e, S)"
+        using restr_stack_simp2 let\<^sub>1(1,2)
+        apply (auto simp add: map_transform_append restrictA_append  restr_stack_simp2[simplified] map_transform_restrA)
+        apply (rule step.let\<^sub>1)
+        apply (auto dest: set_mp[OF edom_Aheap])
+        done
+    }
+    ultimately
+    show ?case by (blast del: consistentI consistentE)
+  next
+    case (if\<^sub>1 \<Gamma> scrut e1 e2 S)
+    have "consistent (ae, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+      using if\<^sub>1  by (auto dest: a_consistent_if\<^sub>1)
+    moreover
+    have "a_transform (ae,  a, as) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow> a_transform (ae, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+      by (auto intro: 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) (\<Gamma>, Bool b, Alts e1 e2 # S)" by auto
+    then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
+      by (rule a_consistent_alts_on_stack)
 
-    have "conf_transform (ae, a) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow> conf_transform (?ae \<squnion> ae, a) (\<Delta> @ \<Gamma>, e, S)"
-      using  let\<^sub>1(1,2)
-      by (fastforce intro!: step.intros simp add: map_transform_append  dest: set_mp[OF edom_Aheap])
-  }
-  ultimately
-  show ?case by (blast del: consistentI consistentE)
-next
-  case refl thus ?case by auto
-next
-  case (trans c c' c'')
-    from trans(3)[OF trans(5)]
-    obtain ae' a' where "consistent (ae', a') c'" and *: "conf_transform (ae, a) c \<Rightarrow>\<^sup>* conf_transform (ae', a') c'" by blast
-    from trans(4)[OF this(1)]
-    obtain ae'' a'' where "consistent (ae'', a'') c''" and **: "conf_transform (ae', a') c' \<Rightarrow>\<^sup>* conf_transform (ae'', a'') c''" by blast
-    from this(1) rtranclp_trans[OF * **]
-    show ?case by blast
-qed
-
+    have "consistent (ae, a', as') (\<Gamma>, if b then e1 else e2, S)" 
+      using if\<^sub>2 by (auto dest!: a_consistent_if\<^sub>2)
+    moreover
+    have "a_transform (ae, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow> a_transform (ae,  a', as') (\<Gamma>, if b then e1 else e2, S)"
+      by (auto intro: 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
+  next
+    case (trans c c' c'')
+      from trans(3)[OF trans(5)]
+      obtain ae' a' as' where "consistent (ae', a', as') c'" and *: "a_transform (ae, a, as) c \<Rightarrow>\<^sup>* a_transform (ae', a', as') c'" by blast
+      from trans(4)[OF this(1)]
+      obtain ae'' a'' as'' where "consistent (ae'', a'', as'') c''" and **: "a_transform (ae', a', as') c' \<Rightarrow>\<^sup>* a_transform (ae'', a'', as'') c''" by blast
+      from this(1) rtranclp_trans[OF * **]
+      show ?case by blast
+  qed
 end
 
-
 end
index 151693e..76d6c9f 100644 (file)
@@ -10,8 +10,8 @@ sublocale CallArityEnd2End.
 lemma end2end:
   "c \<Rightarrow>\<^sup>* c' \<Longrightarrow>
   \<not> boring_step c' \<Longrightarrow>
-  consistent (ae, ce, a) c \<Longrightarrow>
-  \<exists>ae' ce' a'. consistent  (ae', ce', a') c' \<and> conf_transform  (ae, ce, a) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform  (ae', ce', a') c'"
+  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'"
   by (rule foo)
 
 lemma end2end_closed:
@@ -24,22 +24,22 @@ proof-
   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
-  obtain ae ce a where
-    *: "consistent  (ae, ce, a) (\<Gamma>,v,[])" and
-    **: "conf_transform  (\<bottom>, \<bottom>, 0) ([],e,[]) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a) (\<Gamma>,v,[])"
+  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,[])"
     by (metis end2end)
 
-  let ?\<Gamma> = "restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))"
+  let ?\<Gamma> = "map_transform Aeta_expand ae (map_transform transform ae (restrictA (edom ce) \<Gamma>))"
   let ?v = "transform a v"
 
   show ?thesis
   proof(intro exI conjI)
-    show "length (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))) \<le> length \<Gamma>"
-      by (rule order_trans[OF length_restrictA_le]) simp
+    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
+    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
 
index 3b1cb7b..2300068 100644 (file)
@@ -1,5 +1,5 @@
 theory CardinalityEtaExpandCorrect
-imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft ArityAnalysisStack 
+imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft ArityAnalysisStack  ArityConsistent
 begin
 
 context CardinalityPrognosisCorrect
@@ -44,32 +44,26 @@ begin
   lemma fresh_star_transform_alts[intro]: "a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S"
    by (induction as S  rule: transform_alts.induct) (auto simp add: fresh_star_Cons)
 
-  fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
-  where "conf_transform (ae, ce, a, as) (\<Gamma>, e, S) =
-    (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)), 
+  fun a_transform :: "astate \<Rightarrow> conf \<Rightarrow> conf"
+  where "a_transform (ae, a, as) (\<Gamma>, e, S) =
+    (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>), 
      ccTransform a e,
-     transform_alts as (restr_stack (edom ce) S))"
+     transform_alts as  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)"
 
-  inductive stack_consistent :: "Arity list \<Rightarrow> stack \<Rightarrow> bool"
-    where 
-      "stack_consistent [] []"
-    | "Astack S \<sqsubseteq> a \<Longrightarrow> stack_consistent as S \<Longrightarrow> stack_consistent (a#as) (Alts e1 e2 # S)"
-    | "stack_consistent as S \<Longrightarrow> stack_consistent as (Upd x # S)"
-    | "stack_consistent as S \<Longrightarrow> stack_consistent as (Arg x # S)"
-  inductive_simps stack_consistent_foo[simp]:
-    "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)"
-  inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"
 
   inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
     consistentI[intro!]: 
-    "edom ce \<subseteq> domA \<Gamma> \<union> upds S
+    "a_consistent (ae, a, as) (restr_conf (edom ce) (\<Gamma>, e, S))
     \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
     \<Longrightarrow> edom ae = edom ce
-    \<Longrightarrow> Astack (restr_stack (edom ce) S) \<sqsubseteq> a
     \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
-    \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae
     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
-    \<Longrightarrow> stack_consistent as (restr_stack (edom ce) S)
     \<Longrightarrow> consistent (ae, ce, a, as) (\<Gamma>, e, S)"  
   inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (\<Gamma>, e, S)"
 
@@ -78,15 +72,10 @@ begin
     shows "consistent (\<bottom>, \<bottom>, 0, []) ([], e, [])"
   proof-
     from assms
-    have "edom (Aexp e\<cdot>0) = {}"
-      by (auto dest!: set_mp[OF Aexp_edom])
-    moreover
-    from assms
     have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
      by (auto dest!: set_mp[OF edom_prognosis])
-    ultimately
-    show ?thesis
-      by (auto simp add: edom_empty_iff_bot)
+    thus ?thesis
+      by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
   qed
 
   lemma foo:
@@ -98,7 +87,7 @@ begin
   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)"
-      by (cases "x \<in> edom ce") (auto simp add: join_below_iff env_restr_join dest!: below_trans[OF env_restr_mono[OF Aexp_App]] elim: below_trans)
+      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)"
       by simp rule
@@ -108,20 +97,9 @@ begin
   case (app\<^sub>2 \<Gamma> y e x S)
     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)
-    moreover
-    {
-    have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` edom ce  \<sqsubseteq> (env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<squnion> esing x\<cdot>(up\<cdot>0)) f|` edom ce" by (rule env_restr_mono[OF Aexp_subst])
-    also have "\<dots> =  env_delete y ((Aexp e)\<cdot>(pred\<cdot>a))  f|` edom ce \<squnion> esing x\<cdot>(up\<cdot>0)  f|` edom ce" by (simp add: env_restr_join)
-    also have "env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<sqsubseteq> Aexp (Lam [y]. e)\<cdot>a" by (rule Aexp_Lam)
-    also have "\<dots> f|` edom ce \<sqsubseteq> ae" using app\<^sub>2 by (auto simp add: join_below_iff env_restr_join)
-    also have "esing x\<cdot>(up\<cdot>0) f|` edom ce  \<sqsubseteq> ae" using app\<^sub>2
-      by (cases "x\<in>edom ce") (auto simp add: env_restr_join join_below_iff)
-    also have "ae \<squnion> ae = ae" by simp
-    finally  have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` edom ce \<sqsubseteq> ae" by this simp_all
-    }
-    ultimately
+    then
     have "consistent (ae, ce, pred\<cdot>a, as) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
-      by (auto elim: below_trans edom_mono  simp add: join_below_iff env_restr_join)
+      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
     ultimately
@@ -135,22 +113,10 @@ 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)
+
+    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)
   
-    from thunk
-    have "Aexp (Var x)\<cdot>a  f|` edom ce \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join)
-    from fun_belowD[where x = x, OF this] 
-    have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> ae x" by simp
-    from below_trans[OF  Aexp_Var this]
-    have "up\<cdot>a \<sqsubseteq> ae x".    
-    then obtain u where "ae x = up\<cdot>u" and "a \<sqsubseteq> u" by (cases "ae x") auto
-    hence [simp]: "x \<in> edom ae" by (simp add: edom_def)
-
-    have "Astack (restr_stack (edom ce) S) \<sqsubseteq> u" using thunk `a \<sqsubseteq> u` by (auto elim: below_trans)
-  
-    from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
-    have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
-    moreover have "(\<dots> \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" using thunk by (auto simp add: join_below_iff env_restr_join)
-    ultimately have "(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" by simp
 
     show ?case
     proof(cases "ce x" rule:two_cases)
@@ -160,9 +126,6 @@ begin
     next
       case once
 
-      note `ae x = up\<cdot>u` 
-      moreover
-  
       from `prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce`
       have "prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
         using once by (metis (mono_tags) fun_belowD)
@@ -190,40 +153,33 @@ begin
         by (rule below_env_deleteI)
       moreover
 
-      have "ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) = ABinds (delete x \<Gamma>)\<cdot>ae" by (rule Abinds_env_cong) simp
-      with `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|\` edom ce \<sqsubseteq> ae`
-      have "(ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u  \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" by simp
-      from env_restr_mono[where S = "-{x}", OF this]
-      have "(ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u  \<squnion> AEstack as S) f|` edom (env_delete x ce) \<sqsubseteq> env_delete x ae"
-        by (auto simp add: Diff_eq Int_commute env_delete_restr)
-
+      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)
       ultimately
 
-      have "consistent (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" using thunk `a \<sqsubseteq> u`
-        by (auto simp add: join_below_iff env_restr_join insert_absorb restr_delete_twist elim:below_trans below_trans[OF env_restr_mono2, rotated])
-        
-        
+      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 )
       moreover
 
-      from `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`
-      have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by simp
+      from *
+      have "Astack (transform_alts as (restr_stack (edom ce) S)) \<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 \<Gamma>)) x = Some (Aeta_expand u (transform u e))"
+      have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
         by (simp add: map_of_map_transform)
       hence "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G
-             (restrictA (edom ce) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (edom ce) S))"
+             (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))"
           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>* (restrictA (edom ce) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (edom ce) S))"
+      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))"
         by (rule r_into_rtranclp, rule)
       also
-      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (restrictA (edom ce)  (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (edom ce) S))"
+      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`)
       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 simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist)
+        by (auto intro!: map_transform_cong simp add:  map_transform_delete[symmetric]  restr_delete_twist)
       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)".
       }
@@ -246,14 +202,15 @@ 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
-      note `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u  \<squnion> AEstack as S) f|\` edom ce \<sqsubseteq> ae`
+      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`
+        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`
-        by (auto simp add: env_restr_join join_below_iff)
+        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 \<Gamma>)) x = Some (transform 0 e)"
+      have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (edom ce) \<Gamma>))) x = Some (transform 0 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)"
@@ -263,24 +220,16 @@ begin
     qed
   next
   case (lamvar \<Gamma> x e S)
+    from lamvar(1) have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
+
     from lamvar 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)
     then obtain c where "ce x = up\<cdot>c" by (cases "ce x") (auto simp add: edom_def)
 
-    from lamvar have [simp]: "x \<in> domA \<Gamma>" by auto (metis domI dom_map_of_conv_domA)
-    from lamvar have "Aexp (Var x)\<cdot>a f|` edom ce \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join)
-    from fun_belowD[where x = x, OF this] 
-    have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> ae x" by simp
-    from below_trans[OF Aexp_Var this]
-    have "up\<cdot>a \<sqsubseteq> ae x".
-    then obtain u where "ae x = up\<cdot>u" and "a \<sqsubseteq> u" by (cases "ae x") auto
-    hence "x \<in> edom ae" by (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)
 
-    from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
-    have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
-    moreover have "\<dots> f|` edom ce \<sqsubseteq> ae" using lamvar by (auto simp add: join_below_iff env_restr_join)
-    ultimately have "(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u) f|` edom ce \<sqsubseteq> ae" by simp
 
     have "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae as u (\<Gamma>, e, S)"
       using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
@@ -288,13 +237,16 @@ begin
        using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isVal e`  by (rule prognosis_Var_lam)
     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`
+      by (auto intro!: a_consistent_lamvar simp del: restr_delete)
+    ultimately
     have "consistent (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
-      using lamvar `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u) f|\` edom ce \<sqsubseteq> ae`   `ae x = up\<cdot>u` edom_mono[OF *]
-      by (auto simp add: join_below_iff env_restr_join thunks_Cons restr_delete_twist split:if_splits intro: below_trans[OF _ `a \<sqsubseteq> u`] below_trans[OF *])
+      using lamvar edom_mono[OF *] by (auto simp add:  thunks_Cons restr_delete_twist elim: below_trans)
     moreover
-  
-    have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" using lamvar below_trans[OF _ `a \<sqsubseteq> u`] by auto
+
+    from `a_consistent _ _`
+    have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by (auto elim: a_consistent_stackD)
   
     {
     from `isVal e`
@@ -302,17 +254,17 @@ 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)`
-    have "map_of (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))) x = Some (Aeta_expand u (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))"
       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 (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
+          ((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> = (restrictA (edom ce) ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
+    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))"
       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 (rule Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`])
+      by (simp add: restr_delete_twist) (rule Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`])
     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)".
     }
@@ -323,22 +275,27 @@ begin
     proof(cases "x \<in> edom ce")
       case True[simp]
       hence "ce x \<noteq> \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
-      hence "ae x = up\<cdot>a" using var\<^sub>2 by (auto simp add: env_restr_join join_below_iff)
-  
+      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
   
-      have "Astack (Upd x # S) \<sqsubseteq> a" using var\<^sub>2 by auto
-      hence "a = 0" by auto
+      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 "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)"
+        using var\<^sub>2 by (auto intro!: a_consistent_var\<^sub>2)
+      ultimately
       have "consistent (ae, ce, 0, as) ((x, e) # \<Gamma>, e, S)"
-        using var\<^sub>2
-        by (auto simp add: join_below_iff env_restr_join thunks_Cons split:if_splits elim:below_trans[OF *])
+        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>a` `a = 0` var\<^sub>2 `ce x = up\<cdot>c`
+        using `ae x = up\<cdot>0` `a = 0` var\<^sub>2 `ce x = up\<cdot>c`
         by (auto intro!: step.intros simp add: map_transform_Cons)
       ultimately show ?thesis by (blast del: consistentI consistentE)
     next
@@ -358,53 +315,38 @@ begin
       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
       have "consistent (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
-        by (auto simp add: join_below_iff env_restr_join `ce x = \<bottom>` thunks_Cons split:if_splits elim:below_trans[OF *])
+        by (auto simp add: thunks_Cons  elim:below_trans)
       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)
+      ultimately show ?thesis by (auto del: consistentI consistentE simp del:conf_transform.simps)
     qed
   next
     case (let\<^sub>1 \<Delta> \<Gamma> e S)
-  
     let ?ae = "Aheap \<Delta> e\<cdot>a"
-    let ?new = "(domA (\<Delta> @ \<Gamma>) \<union> upds S - (domA \<Gamma> \<union> upds S))"
-    have new: "?new = domA \<Delta>"
-      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])
-  
     let ?ce = "cHeap \<Delta> e\<cdot>a"
   
     have "domA \<Delta> \<inter> upds S = {}" using fresh_distinct_fv[OF let\<^sub>1(2)] by (auto dest: set_mp[OF ups_fv_subset])
-    hence *: "\<And> x. x \<in> upds S \<Longrightarrow> x \<notin> edom ?ce" by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
-  
-    have restr_stack_simp2: "restr_stack (edom (?ce \<squnion> ce)) S = restr_stack (edom ce) S"
+    hence *: "\<And> x. x \<in> upds S \<Longrightarrow> x \<notin> edom ?ae" by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
+    have restr_stack_simp2: "restr_stack (edom (?ae \<squnion> ae)) S = restr_stack (edom ae) S"
       by (auto intro: restr_stack_cong dest!: *)
+
+    have "edom ce = edom ae" using let\<^sub>1 by auto
   
-    have "edom ae \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
+    have "edom ae \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by (auto dest!: a_consistent_edom_subsetD)
     from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
     have "edom ae \<inter> domA \<Delta> = {}" by (auto dest: set_mp[OF ups_fv_subset])
-    hence [simp]: "\<And> S. S \<subseteq> domA \<Delta> \<Longrightarrow> ae f|` S = \<bottom>" by auto
 
-    have "edom ce \<subseteq> domA \<Gamma> \<union> upds S" using let\<^sub>1 by auto
-    from set_mp[OF this] fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
-    have "edom ce \<inter> domA \<Delta> = {}"
-       by (auto dest: set_mp[OF ups_fv_subset])
+    from `edom ae \<inter> domA \<Delta> = {}`
+    have [simp]: "edom (Aheap \<Delta> e\<cdot>a) \<inter> edom ae = {}" by (auto dest!: set_mp[OF edom_Aheap]) 
 
     from fresh_distinct[OF let\<^sub>1(1)]
-    have "edom ?ae \<inter> domA \<Gamma> = {}" by (auto dest: set_mp[OF edom_Aheap])
-    hence "edom ?ce \<inter> domA \<Gamma> = {}" by (simp add: edom_cHeap)
+    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]) 
 
-  
-    from  fresh_distinct[OF let\<^sub>1(1)]
-    have [simp]: "\<And> S. S \<subseteq> domA \<Gamma> \<Longrightarrow> ?ae f|` S = \<bottom>" by (auto dest!: set_mp[OF edom_Aheap])
-  
     {
-    have "edom (?ce \<squnion> ce) \<subseteq> domA (\<Delta> @ \<Gamma>) \<union> upds S"
-      using let\<^sub>1(3) by (auto simp add: edom_cHeap dest: set_mp[OF edom_Aheap])
-    moreover
     have "edom (?ae \<squnion> ae) = edom (?ce \<squnion> ce)"
       using let\<^sub>1(3) by (auto simp add: edom_cHeap)
     moreover
@@ -424,24 +366,13 @@ begin
       hence "x \<notin> domA \<Gamma>" and "x \<notin> upds S"
         using fresh_distinct[OF let\<^sub>1(1)] fresh_distinct_fv[OF let\<^sub>1(2)]
         by (auto dest!: set_mp[OF thunks_domA] set_mp[OF ups_fv_subset])
-      hence "x \<notin> edom ce" using let\<^sub>1 by auto
+      hence "x \<notin> edom ce" using `edom ae \<subseteq> domA \<Gamma> \<union> upds S` `edom ce = edom ae` by auto
       hence [simp]: "ce x = \<bottom>"  by (auto simp add: edomIff)
   
       assume "many \<sqsubseteq> (?ce \<squnion> ce) x" with `x \<in> thunks \<Delta>`
       have "(?ae \<squnion> ae) x = up\<cdot>0" by (auto simp add: Aheap_heap3)
     }
     moreover
-    have [simp]: "ap S \<inter> edom (cHeap \<Delta> e\<cdot>a) = {}"
-      using fresh_distinct_fv[OF let\<^sub>1(2)] 
-      by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap] set_mp[OF ap_fv_subset])
-
-    have "stack_consistent as (restr_stack (edom ce) S)" using let\<^sub>1 by auto 
-    hence "stack_consistent as (restr_stack (edom (?ce \<squnion> ce)) S)" unfolding restr_stack_simp2.
-    moreover
-    have "Astack (restr_stack (edom (?ce \<squnion> ce)) S) \<sqsubseteq> a" unfolding restr_stack_simp2 using let\<^sub>1 by auto
-    moreover
-    have "edom (?ce \<squnion> ce) \<subseteq> edom (?ae \<squnion> ae)" using let\<^sub>1 by (auto simp add: edom_cHeap)
-    moreover
     {
     from let\<^sub>1(1,2) `edom ae \<subseteq> domA \<Gamma> \<union> upds S`
     have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> prognosis ae as a (\<Gamma>, Let \<Delta> e, S)" by (rule prognosis_Let)
@@ -453,33 +384,16 @@ begin
     with fresh_distinct[OF let\<^sub>1(1)]  `domA \<Delta> \<inter> upds S = {}`
     have "heap_upds_ok (\<Delta> @ \<Gamma>, S)" by (rule heap_upds_ok_append)
     moreover
-    {
-    have "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)"
-      by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
-    moreover
-    have "ABinds \<Gamma>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Gamma>\<cdot>ae"
-      by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
-    moreover
-    have "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a" by (rule Aexp_Let)
-    moreover
-    have "(ABinds \<Gamma>\<cdot>ae \<squnion> Aexp (Let \<Delta> e)\<cdot>a \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae" using let\<^sub>1 by auto
-    moreover
-    have "Aexp (Terms.Let \<Delta> e)\<cdot>a f|` (edom ce \<union> edom (cHeap \<Delta> e\<cdot>a)) = Aexp (Terms.Let \<Delta> e)\<cdot>a f|` edom ce"
-      by (rule env_restr_cong) (auto simp add: edom_cHeap dest!: set_mp[OF Aexp_edom]  set_mp[OF edom_Aheap])
-    moreover
-    have "ABinds \<Gamma>\<cdot>ae f|` (edom ce \<union> edom (cHeap \<Delta> e\<cdot>a)) = ABinds \<Gamma>\<cdot>ae f|` edom ce" 
-      using fresh_distinct_fv[OF let\<^sub>1(1)]
-      by (auto intro: env_restr_cong  simp add: edom_cHeap dest!: set_mp[OF Aexp_edom]  set_mp[OF edom_Aheap] set_mp[OF edom_AnalBinds])
-    moreover
-    thm env_restr_cong
-    have "AEstack as S f|` (edom ce \<union> edom (cHeap \<Delta> e\<cdot>a)) = AEstack as S f|` (edom ce)" 
-      using fresh_distinct_fv[OF let\<^sub>1(2)]
-      by (auto intro: env_restr_cong simp add: edom_cHeap dest!: set_mp[OF edom_Aheap] set_mp[OF edom_AEstack])
-    ultimately
-    have "(ABinds (\<Delta> @ \<Gamma>) \<cdot> (Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` edom (?ce \<squnion> ce) \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> ae"
-      by (simp only: join_assoc[symmetric] restrictA_append Abinds_append_disjoint[OF fresh_distinct[OF let\<^sub>1(1)]] join_below_iff env_restr_join)
-         (auto 4 4 simp add: join_below_iff env_restr_join intro: below_trans[OF env_restr_below_self] elim!: below_trans[OF env_restr_mono] below_trans)
-    }
+    
+    have "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Let \<Delta> e, restr_stack (edom ce) S)"
+      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)"
+      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)
     ultimately
     have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a, as) (\<Delta> @ \<Gamma>, e, S)"
       by auto
@@ -489,40 +403,37 @@ begin
       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 "restrictA (edom (?ce \<squnion> ce)) (map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) \<Gamma>))
-         = restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))"
+      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>))"
          by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
       moreover
   
-      from let\<^sub>1 have *: "edom ce \<subseteq> domA \<Gamma> \<union> upds S"  "edom ae \<subseteq> domA \<Gamma> \<union> upds S" by auto
+      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 *(1)] set_mp[OF *(2)] set_mp[OF ups_fv_subset])
-      hence "restrictA (edom (?ce \<squnion> ce)) (map_transform Aeta_expand (?ae \<squnion> ae) (map_transform transform (?ae \<squnion> ae) \<Delta>))
-         = restrictA (edom ?ce) (map_transform Aeta_expand ?ae (map_transform transform ?ae \<Delta>))"
+         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>))"
          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)"
-        using restr_stack_simp2 let\<^sub>1(1,2)
-        by (fastforce intro!: let_and_restrict simp  add: map_transform_append restrictA_append  edom_cHeap  dest: set_mp[OF edom_Aheap])
+        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 dest: set_mp[OF edom_Aheap])
+        done
     }
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
     case (if\<^sub>1 \<Gamma> scrut e1 e2 S)
-    {
-    have "Aexp (scrut ? e1 : e2)\<cdot>a f|` edom ce \<sqsubseteq> ae" using if\<^sub>1 by (auto simp add: env_restr_join join_below_iff)
-    hence "(Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a) f|` edom ce \<sqsubseteq> ae"
-      by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]])
-    moreover
     have "prognosis ae 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])
-    ultimately
-    have "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
-      using if\<^sub>1  by (auto simp add: env_restr_join join_below_iff)
-    }
+    hence "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+      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)"
       by (auto intro: normal step.intros)
@@ -530,15 +441,16 @@ begin
     show ?case by (blast del: consistentI consistentE)
   next
     case (if\<^sub>2 \<Gamma> b e1 e2 S)
-    from if\<^sub>2 obtain a' as' where [simp]: "as = a' # as'" by auto
-    from if\<^sub>2 have [simp]: "a = 0" by auto
+    hence "a_consistent (ae, a, as) (restrictA (edom ce) \<Gamma>, Bool b, Alts e1 e2 # restr_stack (edom ce) S)" by auto
+    then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
+      by (rule a_consistent_alts_on_stack)
 
     {
     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)" 
-      using if\<^sub>2 by (auto simp add: env_restr_join join_below_iff)
+      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)"
index f380a08..160076c 100644 (file)
@@ -314,8 +314,21 @@ theorem DeadCodeRemovalCorrectSteps:
 using assms
   by (induction rule: rtranclp_induct)(fastforce dest: DeadCodeRemovalCorrectStep)+
 
+
+lemma set_clearjunk: "set (clearjunk \<Gamma>) \<subseteq> set \<Gamma>"
+  by (induction \<Gamma>) (auto simp add: clearjunk_delete dest: set_mp[OF set_delete_subset])
+
+lemma set_map_run: "set (map_ran f \<Gamma>) = (\<lambda> (x,e). (x,f x e)) ` set \<Gamma>"
+  by (induction \<Gamma>) auto
+
+lemma remove_dead_code_bool_free:
+  "bool_free e \<Longrightarrow> bool_free (remove_dead_code e)"
+by (nominal_induct e rule: exp_strong_induct_set)
+   (auto 4 3 simp add: restrict_reachable_def set_map_run dest!: set_mp[OF set_restrictA] set_mp[OF set_clearjunk])
+
 corollary
   assumes "[] : e \<Down>\<^bsub>L\<^esub> \<Delta> : z"
+  assumes "bool_free e"
    shows  "\<exists> \<Delta>' z'. [] : remove_dead_code e \<Down>\<^bsub>L\<^esub> \<Delta>' : z'"
 proof-
   let "?S" = "map Dummy L"
@@ -326,7 +339,7 @@ proof-
   have "([], e, ?S) \<Rightarrow>\<^sup>* (\<Delta>, z, ?S)".
   moreover
   have "([], e, ?S) \<triangleright> (rdcH {} [], remove_dead_code e, rdcS ?S)" by (rule dc_rel.intros) auto
-  hence "([], e, ?S) \<triangleright> ([], remove_dead_code e, rdcS  ?S)" by simp
+  hence "([], e, ?S) \<triangleright> ([], remove_dead_code e, rdcS ?S)" by simp
   ultimately
   obtain \<Delta>' z' T' where "(\<Delta>, z, ?S) \<triangleright> (\<Delta>', z', T')" and "([], remove_dead_code e, rdcS  ?S) \<Rightarrow>\<^sup>* (\<Delta>', z', T')"
     by (metis DeadCodeRemovalCorrectSteps)
@@ -334,6 +347,10 @@ proof-
   from dummy_stack_balanced[OF * this]
   obtain T where "bal ([], remove_dead_code e, rdcS ?S) T (\<Delta>', remove_dead_code z, rdcS ?S)".
   moreover
+  have "bool_free_stack ?S" by (induction L) (auto intro: bool_free_stack.intros)
+  with remove_dead_code_bool_free[OF assms(2)]
+  have "bool_free_conf ([], remove_dead_code e, rdcS ?S)" by auto
+  moreover
   have "isLam z" using assms(1) by (induction) simp
   hence "isLam (remove_dead_code z)" by (rule isLam_remove_dead_code)
   ultimately
index 156eae8..81d292e 100644 (file)
@@ -220,6 +220,16 @@ lemma env_delete_env_restr_swap:
   "env_delete x (env_restr S e) = env_restr S (env_delete x e)"
   by (metis (erased, hide_lams) env_delete_def env_restr_fun_upd env_restr_fun_upd_other fun_upd_triv lookup_env_restr_eq)
 
+lemma env_delete_mono:
+  "m \<sqsubseteq> m' \<Longrightarrow> env_delete x m \<sqsubseteq> env_delete x m'"
+  unfolding env_delete_restr
+  by (rule env_restr_mono)
+  
+lemma env_delete_below_arg:
+  "env_delete x m \<sqsubseteq> m"
+  unfolding env_delete_restr
+  by (rule env_restr_below_self)
+
 subsubsection {* Merging of two functions *}
 
 text {*
index bb93a19..c41c46a 100644 (file)
@@ -104,15 +104,23 @@ 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)
 
+lemma heap_upds_ok_delete:
+  "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, S)"
+  by auto
+
+lemma heap_upds_ok_restrictA:
+  "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (restrictA V \<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)
+  by auto
 
 lemma heap_upds_ok_reorder:
   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok ((x,e) # delete x \<Gamma>, S)"
   by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)
 
-lemmas heap_upds_ok_intros[intro] = heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_reorder heap_upds_ok_app1 heap_upds_ok_app2 heap_upds_ok_alts1 heap_upds_ok_alts2
+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"
index 90c9dba..8a2f57f 100644 (file)
@@ -1,5 +1,5 @@
 theory SestoftCorrect
-imports Sestoft Launchbury BalancedTraces
+imports BalancedTraces Launchbury Sestoft
 begin
 
 
@@ -82,8 +82,113 @@ lemma lambda_stop:
   apply (auto elim!: step.cases)
   done
 
+nominal_function bool_free :: "exp \<Rightarrow> bool" where
+    "bool_free (Lam [x]. e) \<longleftrightarrow> bool_free e"
+  | "bool_free (Var x) \<longleftrightarrow> True"
+  | "bool_free (App e x) \<longleftrightarrow> bool_free e"
+  | "bool_free (Terms.Let \<Gamma> e) \<longleftrightarrow> (\<forall> (x, e) \<in> set \<Gamma>. bool_free e) \<and> bool_free e"
+  | "bool_free (Bool b) \<longleftrightarrow> False"
+  | "bool_free (scrut ? e\<^sub>1 : e\<^sub>2) \<longleftrightarrow> False"
+proof-
+case goal1 thus ?case
+  unfolding bool_free_graph_aux_def eqvt_def 
+  apply rule
+  apply perm_simp
+  apply rule
+  done
+next
+case goal3 thus ?case
+  by (metis Terms.Let_def exp_assn.exhaust(1) heapToAssn_asToHeap)
+next
+case (goal4 x e x' e')
+  from goal4(5)
+  show ?case
+  proof (rule eqvt_lam_case)
+    fix \<pi> :: perm
+    assume "supp \<pi> \<sharp>* Lam [x]. e"
+      
+    have "bool_free_sumC (\<pi> \<bullet> e) = \<pi> \<bullet> bool_free_sumC e"
+        by (simp add: pemute_minus_self eqvt_at_apply'[OF goal4(1)])
+    also have "\<dots> = bool_free_sumC e" by (simp add: permute_pure)
+    finally show  "bool_free_sumC (\<pi> \<bullet> e) = bool_free_sumC e".
+  qed
+next
+case (goal19 as body as' body')
+  from goal19(9)
+  show ?case
+  proof (rule eqvt_let_case)
+    fix \<pi> :: perm
+  
+    from goal19(2,4) have eqvt_at1: "eqvt_at bool_free_sumC body" by auto
+
+    assume assm: "supp \<pi> \<sharp>* Let as body"
+    
+    have "(\<forall> (x,e)\<in>set (\<pi> \<bullet> as). bool_free_sumC e) \<longleftrightarrow> - \<pi> \<bullet> (\<forall> (x,e)\<in>set (\<pi> \<bullet> as). bool_free_sumC e)"
+      by (simp add: permute_pure unpermute_def)
+      thm unpermute_def
+    also have "\<dots> = (\<forall> (x,e)\<in>set as. (- \<pi> \<bullet> bool_free_sumC) e)"
+      by perm_simp (simp add: pemute_minus_self)
+    also have "\<dots> = (\<forall> (x,e)\<in>set as. bool_free_sumC e)"
+      apply (rule ball_cong[OF refl])
+      apply (rule prod.case_cong[OF refl])
+      apply (rule eqvt_at_apply)
+      apply (metis goal19(1))
+      done
+    finally
+    have "(\<forall> (x,e)\<in>set (\<pi> \<bullet> as). bool_free_sumC e) \<longleftrightarrow> (\<forall> (x,e)\<in>set as. bool_free_sumC e)".
+    moreover
+    have "bool_free_sumC (\<pi> \<bullet> body) \<longleftrightarrow>  bool_free_sumC body" 
+      by (metis (full_types) True_eqvt eqvt_at1  eqvt_at_apply' eqvt_bound)
+    ultimately
+    show "((\<forall>a\<in>set (\<pi> \<bullet> as). case a of (x, x0) \<Rightarrow> bool_free_sumC x0) \<and> bool_free_sumC (\<pi> \<bullet> body)) =
+         ((\<forall>a\<in>set as. case a of (x, x0) \<Rightarrow> bool_free_sumC x0) \<and> bool_free_sumC body)" by simp
+  qed
+qed auto
+nominal_termination (eqvt) by lexicographic_order
+
+lemma bool_free_SmartLet[simp]:
+  "bool_free (SmartLet \<Gamma> e) \<longleftrightarrow> (\<forall> (x, e) \<in> set \<Gamma>. bool_free e) \<and> bool_free e"
+by (auto simp add: SmartLet_def)
+
+lemma Ball_subst[simp]:
+  "(\<forall>p\<in>set (\<Gamma>[y::h=x]). f p) \<longleftrightarrow> (\<forall>p\<in>set \<Gamma>. case p of (z,e) \<Rightarrow> f (z, e[y::=x]))"
+  by (induction \<Gamma>) auto
+
+lemma [simp]: "bool_free e[y::=x] \<longleftrightarrow> bool_free e"
+  by (nominal_induct e avoiding: x y rule: exp_strong_induct_set) (auto  simp add: fresh_star_Pair)
+
+inductive bool_free_stack :: "stack \<Rightarrow> bool" where
+  "bool_free_stack []"
+  | "bool_free_stack S \<Longrightarrow> bool_free_stack (Upd x # S)"
+  | "bool_free_stack S \<Longrightarrow> bool_free_stack (Arg x # S)"
+  | "bool_free_stack S \<Longrightarrow> bool_free_stack (Dummy x # S)"
+
+inductive_simps bool_free_stack_simps: "bool_free_stack []"  "bool_free_stack (s # S)"
+
+fun bool_free_conf :: "conf \<Rightarrow> bool" where
+  "bool_free_conf (\<Gamma>, e, S) \<longleftrightarrow> (\<forall> (x, e) \<in> set \<Gamma>. bool_free e) \<and> bool_free e \<and> bool_free_stack S"
+
+lemma step_bool_free:
+  "c1 \<Rightarrow> c2 \<Longrightarrow> bool_free_conf c1 \<Longrightarrow> bool_free_conf c2"
+  by (cases rule: step.cases) (auto simp add: bool_free_stack_simps dest!: set_mp[OF set_delete_subset] map_of_is_SomeD)
+  
+lemma step_star_bool_free:
+  assumes  "c \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> c'"
+  assumes "bool_free_conf c"
+  shows "bool_free_conf c'"
+using assms by (induction) (auto dest: step_bool_free)
+
+lemma bal_star_bool_free:
+  assumes  "c \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> c'"
+  assumes "bool_free_conf c"
+  shows "bool_free_conf c'"
+using assms by (metis bal.simps step_star_bool_free)
+
+
 lemma lemma_3:
   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
+  assumes "bool_free_conf (\<Gamma>, e, S)"
   assumes "isLam z"
   shows "\<Gamma> : e \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z"
 using assms
@@ -101,7 +206,9 @@ proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[w
   next
   case (trace_cons conf' T')
     from `T = conf' # T'` and `\<forall> c'\<in>set T. S \<lesssim> stack c'` have "S \<lesssim> stack conf'" by auto
-  
+
+    note step_bool_free[OF `(\<Gamma>, e, S) \<Rightarrow> conf'`  `bool_free_conf (\<Gamma>, _, S)`]
+
     from `(\<Gamma>, e, S) \<Rightarrow> conf'`
     show ?thesis
     proof(cases)
@@ -112,6 +219,9 @@ proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[w
 
       from `T = _` `T' = _` have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T" by auto
 
+      note bal_star_bool_free[OF prem1 `bool_free_conf conf'`[unfolded app\<^sub>1]]
+      note step_bool_free[OF `c\<^sub>3 \<Rightarrow> c\<^sub>4` this]
+
       from prem1 have "stack c\<^sub>3 =  Arg x # S" by (auto dest:  bal_stackD)
       moreover
       from prem2 have "stack c\<^sub>4 = S" by (auto dest: bal_stackD)
@@ -120,11 +230,12 @@ proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[w
       ultimately
       obtain \<Delta>' y e' where "c\<^sub>3 = (\<Delta>', Lam [y]. e', Arg x # S)" and "c\<^sub>4 = (\<Delta>', e'[y ::= x], S)"
         by (auto elim!: step.cases simp del: exp_assn.eq_iff)
+
       
-      from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`] isLam_Lam]
+      from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`] `bool_free_conf conf'`[unfolded app\<^sub>1] isLam_Lam]
       have "\<Gamma> : e \<Down>\<^bsub>x # (flattn S)\<^esub> \<Delta>' : Lam [y]. e'" by simp
       moreover
-      from less(1)[OF `length T\<^sub>2 < length T` prem2[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`] `isLam z`]
+      from less(1)[OF `length T\<^sub>2 < length T` prem2[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`]  `bool_free_conf c\<^sub>4`[unfolded `c\<^sub>4 = _`] `isLam z`]
       have "\<Delta>' : e'[y::=x] \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z" by simp
       ultimately
       show ?thesis unfolding app\<^sub>1
@@ -157,7 +268,7 @@ proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[w
       with prem2 `c\<^sub>4 = _`
       have "z' = z" and "\<Delta> = (x,z)#\<Delta>'" by auto
           
-      from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`  `z' = _`] `isLam z`]
+      from less(1)[OF `length T\<^sub>1 < length T` prem1[unfolded `c\<^sub>3 = _` `c\<^sub>4 = _`  `z' = _`] `bool_free_conf conf'`[unfolded var\<^sub>1]  `isLam z`]
       have "delete x \<Gamma> : e \<Down>\<^bsub>x # flattn S\<^esub> \<Delta>' : z" by simp
       with `map_of _ _ = _`
       show ?thesis unfolding var\<^sub>1(1) `\<Delta> = _` by rule
@@ -173,6 +284,8 @@ proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[w
       have "(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)" 
         using trace_cons `conf' = _`  `\<forall> c'\<in>set T. S \<lesssim> stack c'` by fastforce
       moreover
+      note `bool_free_conf conf'`[unfolded let\<^sub>1]
+      moreover
       note `isLam z`
       ultimately
       have "as @ \<Gamma> : e \<Down>\<^bsub>flattn S\<^esub> \<Delta> : z" by (rule less)
@@ -181,6 +294,16 @@ proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[w
       have "atom ` domA as \<sharp>* (\<Gamma>, flattn S)" by (auto simp add: fresh_star_Pair)
       ultimately
       show ?thesis unfolding let\<^sub>1  by (rule reds.Let[rotated])
+    next
+    case (if\<^sub>1)
+      with `bool_free_conf (\<Gamma>, e, S)`
+      have False by simp
+      thus ?thesis..
+   next
+    case (if\<^sub>2)
+      with `bool_free_conf (\<Gamma>, e, S)`
+      have False by simp
+      thus ?thesis..
     qed
   qed
 qed
@@ -192,7 +315,7 @@ lemma dummy_stack_extended:
   apply auto
   done
 
-lemma[simp]: "Arg x \<notin> range Dummy"  "Upd x \<notin> range Dummy" by auto
+lemma[simp]: "Arg x \<notin> range Dummy"  "Upd x \<notin> range Dummy"   "Alts e\<^sub>1 e\<^sub>2 \<notin> range Dummy" by auto
 
 lemma dummy_stack_balanced:
   assumes "set S \<subseteq> Dummy ` UNIV"
@@ -203,7 +326,8 @@ proof-
   obtain T where "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"..
   moreover
   hence "\<forall> c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'"
-    by(rule conjunct1[OF traces_list_all]) (auto elim: step.cases simp add: dummy_stack_extended[OF `set S \<subseteq> Dummy \` UNIV`])
+    by (rule conjunct1[OF traces_list_all])
+       (auto elim: step.cases simp add: dummy_stack_extended[OF `set S \<subseteq> Dummy \` UNIV`])
   ultimately
   have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
     by (rule balI) simp
index c5f9d8c..31de3b0 100644 (file)
@@ -50,7 +50,7 @@ lemma delete_map_transform_env_delete:
   "delete x (map_transform t (env_delete x ae) \<Gamma>) = delete x (map_transform t ae \<Gamma>)"
   unfolding map_transform_def by (induction \<Gamma>) auto
 
-lemma map_transform_Nil:
+lemma map_transform_Nil[simp]:
   "map_transform t ae [] = []"
   unfolding map_transform_def by simp
 
index 2a41bf6..5a96b14 100644 (file)
@@ -47,6 +47,10 @@ next
   assume "x \<notin> S" and "y \<notin> S"
   thus "Trivial_Aexp e[x::=y]\<cdot>a f|` S = Trivial_Aexp e\<cdot>a f|` S"
     by (auto simp add: Trivial_Aexp_simp fv_subst_eq intro!: arg_cong[where f = "\<lambda> S. env_restr S e" for e])
+next
+  fix scrut e1 a e2
+  show "Trivial_Aexp scrut\<cdot>0 \<squnion> Trivial_Aexp e1\<cdot>a \<squnion> Trivial_Aexp e2\<cdot>a \<sqsubseteq> Trivial_Aexp (scrut ? e1 : e2)\<cdot>a"
+    by (auto intro: env_restr_mono2 simp add: Trivial_Aexp_simp join_below_iff )
 qed
 
 definition Trivial_Aheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> AEnv" where