More module splitting
authorJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 11:30:24 +0000 (11:30 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 11:30:24 +0000 (11:30 +0000)
25 files changed:
Launchbury/ArityAnalysisAbinds.thy
Launchbury/ArityAnalysisFix.thy
Launchbury/ArityAnalysisFixProps.thy
Launchbury/ArityAnalysisSig.thy
Launchbury/ArityAnalysisSpec.thy
Launchbury/ArityEtaExpand.thy [deleted file]
Launchbury/ArityEtaExpandCorrect.thy [new file with mode: 0644]
Launchbury/CallArityCorrectEnd2End.thy
Launchbury/CallArityEnd2End.thy [new file with mode: 0644]
Launchbury/CardinalityAnalysis.thy [deleted file]
Launchbury/CardinalityAnalysisSig.thy [new file with mode: 0644]
Launchbury/CardinalityAnalysisSpec.thy [new file with mode: 0644]
Launchbury/CardinalityEtaExpand.thy [deleted file]
Launchbury/CardinalityEtaExpandCorrect.thy [new file with mode: 0644]
Launchbury/CoCallAnalysisImpl.thy
Launchbury/CoCallAnalysisSpec.thy [new file with mode: 0644]
Launchbury/CoCallAritySig.thy [new file with mode: 0644]
Launchbury/CoCallImplCorrect.thy
Launchbury/CoCallImplFTree.thy [new file with mode: 0644]
Launchbury/CoCallImplFTreeCorrect.thy [new file with mode: 0644]
Launchbury/FTreeCardinality.thy [deleted file]
Launchbury/FTreeImplCardinality.thy [new file with mode: 0644]
Launchbury/FTreeImplCardinalityCorrect.thy [new file with mode: 0644]
Launchbury/NoCardinalityAnalysis.thy
ROOT

index e3bdabc..b86974b 100644 (file)
@@ -157,4 +157,14 @@ case (goal2  v e as heap2)
   show ?case by (auto simp add: ArityAnalysis.ABinds.simps ArityAnalysis.ABind_def)
 qed
 
+context EdomArityAnalysis
+begin
+  lemma fup_Aexp_lookup_fresh: "atom v \<sharp> e \<Longrightarrow> (fup\<cdot>(Aexp e)\<cdot>a) v = \<bottom>"
+    by (cases a) auto
+  
+  lemma edom_AnalBinds: "edom (ABinds \<Gamma>\<cdot>ae) \<subseteq> fv \<Gamma>"
+    by (induction \<Gamma> rule: ABinds.induct)
+       (auto simp del: fun_meet_simp dest: set_mp[OF fup_Aexp_edom] dest: set_mp[OF fv_delete_subset])
+end 
+
 end
index 0a4555a..b070c36 100644 (file)
@@ -173,5 +173,95 @@ lemma Afix_cong[fundef_cong]:
       \<Longrightarrow> ArityAnalysis.Afix aexp1 heap1 = ArityAnalysis.Afix aexp2 heap2"
    unfolding ArityAnalysis.Afix_def by (metis Abinds_cong)
 
+
+context EdomArityAnalysis
+begin
+
+lemma Afix_edom: "edom (Afix \<Gamma> \<cdot> ae) \<subseteq> fv \<Gamma> \<union> edom ae"
+  unfolding Afix_eq
+  by (rule fix_ind[where P = "\<lambda> ae' . edom ae' \<subseteq> fv \<Gamma> \<union> edom ae"] )
+     (auto dest: set_mp[OF edom_AnalBinds])
+
+lemma ABinds_lookup_fresh:
+  "atom v \<sharp> \<Gamma> \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae) v = \<bottom>"
+by (induct \<Gamma> rule: ABinds.induct) (auto simp add: fresh_Cons fresh_Pair fup_Aexp_lookup_fresh fresh_delete)
+
+lemma Afix_lookup_fresh:
+  assumes "atom v \<sharp> \<Gamma>"
+  shows "(Afix \<Gamma>\<cdot>ae) v = ae v"
+  apply (rule below_antisym)
+  apply (subst Afix_eq)
+  apply (rule fix_ind[where  P = "\<lambda> ae'. ae' v \<sqsubseteq> ae v"])
+  apply (auto simp add: ABinds_lookup_fresh[OF assms] fun_belowD[OF Afix_above_arg])
+  done
+
+lemma Afix_comp2join_fresh:
+  "atom ` (domA \<Delta>) \<sharp>* \<Gamma> \<Longrightarrow> ABinds \<Delta>\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds \<Delta>\<cdot>ae"
+proof (induct \<Delta> rule: ABinds.induct)
+  case 1 show ?case by (simp add: Afix_above_arg del: fun_meet_simp)
+next
+  case (2 v e \<Delta>)
+  from 2(2)
+  have "atom v \<sharp> \<Gamma>" and  "atom ` domA (delete v \<Delta>) \<sharp>* \<Gamma>"
+    by (auto simp add: fresh_star_def)
+  from 2(1)[OF this(2)]
+  show ?case by (simp del: fun_meet_simp add: Afix_lookup_fresh[OF `atom v \<sharp> \<Gamma>`])
+qed
+
+lemma Afix_append_fresh:
+  assumes "atom ` domA \<Delta> \<sharp>* \<Gamma>"
+  shows "Afix (\<Delta> @ \<Gamma>)\<cdot>ae = Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)"
+proof (rule below_antisym)
+  show *: "Afix (\<Delta> @ \<Gamma>)\<cdot>ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)"
+  apply (rule Afix_least_below)
+  apply (simp add: Abinds_append_disjoint[OF fresh_distinct[OF assms]] Afix_comp2join_fresh[OF assms])
+  apply (rule below_trans[OF join_mono[OF Abinds_Afix_below Abinds_Afix_below]])
+  apply (simp_all add: Afix_above_arg  below_trans[OF Afix_above_arg Afix_above_arg])
+  done
+next
+  show "Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
+  proof (rule Afix_least_below)
+    show "ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
+      apply (rule below_trans[OF _ Abinds_Afix_below])
+      apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
+      apply simp
+      done
+    have "ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
+      apply (rule below_trans[OF _ Abinds_Afix_below])
+      apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
+      apply simp
+      done
+    thus "Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
+      apply (rule Afix_least_below)
+      apply (rule Afix_above_arg)
+      done
+  qed
+qed
+
+
+lemma Afix_e_to_heap:
+   "Afix (delete x \<Gamma>)\<cdot>(fup\<cdot>(Aexp e)\<cdot>n \<squnion> ae) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>n \<squnion> ae)"
+    apply (simp add: Afix_eq)
+    apply (rule fix_least_below, simp)
+    apply (intro join_below)
+    apply (subst fix_eq, simp)
+    apply (subst fix_eq, simp)
+
+    apply (rule below_trans[OF _ join_above2])
+    apply (rule below_trans[OF _ join_above2])
+    apply (rule below_trans[OF _ join_above2])
+    apply (rule monofun_cfun_arg)
+    apply (subst fix_eq, simp)
+      
+    apply (subst fix_eq, simp) back apply (simp add: below_trans[OF _ join_above2])
+    done
+
+lemma Afix_e_to_heap':
+   "Afix (delete x \<Gamma>)\<cdot>(Aexp e\<cdot>n) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>(up\<cdot>n))"
+using Afix_e_to_heap[where ae = \<bottom> and n = "up\<cdot>n"] by simp
+
+end
+
+
 end
 
index e142c44..5bdc789 100644 (file)
@@ -2,94 +2,6 @@ theory ArityAnalysisFixProps
 imports ArityAnalysisFix ArityAnalysisSpec
 begin
 
-context EdomArityAnalysis
-begin
-
-lemma Afix_edom: "edom (Afix \<Gamma> \<cdot> ae) \<subseteq> fv \<Gamma> \<union> edom ae"
-  unfolding Afix_eq
-  by (rule fix_ind[where P = "\<lambda> ae' . edom ae' \<subseteq> fv \<Gamma> \<union> edom ae"] )
-     (auto dest: set_mp[OF edom_AnalBinds])
-
-lemma ABinds_lookup_fresh:
-  "atom v \<sharp> \<Gamma> \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae) v = \<bottom>"
-by (induct \<Gamma> rule: ABinds.induct) (auto simp add: fresh_Cons fresh_Pair fup_Aexp_lookup_fresh fresh_delete)
-
-lemma Afix_lookup_fresh:
-  assumes "atom v \<sharp> \<Gamma>"
-  shows "(Afix \<Gamma>\<cdot>ae) v = ae v"
-  apply (rule below_antisym)
-  apply (subst Afix_eq)
-  apply (rule fix_ind[where  P = "\<lambda> ae'. ae' v \<sqsubseteq> ae v"])
-  apply (auto simp add: ABinds_lookup_fresh[OF assms] fun_belowD[OF Afix_above_arg])
-  done
-
-lemma Afix_comp2join_fresh:
-  "atom ` (domA \<Delta>) \<sharp>* \<Gamma> \<Longrightarrow> ABinds \<Delta>\<cdot>(Afix \<Gamma>\<cdot>ae) = ABinds \<Delta>\<cdot>ae"
-proof (induct \<Delta> rule: ABinds.induct)
-  case 1 show ?case by (simp add: Afix_above_arg del: fun_meet_simp)
-next
-  case (2 v e \<Delta>)
-  from 2(2)
-  have "atom v \<sharp> \<Gamma>" and  "atom ` domA (delete v \<Delta>) \<sharp>* \<Gamma>"
-    by (auto simp add: fresh_star_def)
-  from 2(1)[OF this(2)]
-  show ?case by (simp del: fun_meet_simp add: Afix_lookup_fresh[OF `atom v \<sharp> \<Gamma>`])
-qed
-
-lemma Afix_append_fresh:
-  assumes "atom ` domA \<Delta> \<sharp>* \<Gamma>"
-  shows "Afix (\<Delta> @ \<Gamma>)\<cdot>ae = Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)"
-proof (rule below_antisym)
-  show *: "Afix (\<Delta> @ \<Gamma>)\<cdot>ae \<sqsubseteq> Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae)"
-  apply (rule Afix_least_below)
-  apply (simp add: Abinds_append_disjoint[OF fresh_distinct[OF assms]] Afix_comp2join_fresh[OF assms])
-  apply (rule below_trans[OF join_mono[OF Abinds_Afix_below Abinds_Afix_below]])
-  apply (simp_all add: Afix_above_arg  below_trans[OF Afix_above_arg Afix_above_arg])
-  done
-next
-  show "Afix \<Gamma>\<cdot>(Afix \<Delta>\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
-  proof (rule Afix_least_below)
-    show "ABinds \<Gamma>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
-      apply (rule below_trans[OF _ Abinds_Afix_below])
-      apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
-      apply simp
-      done
-    have "ABinds \<Delta>\<cdot>(Afix (\<Delta> @ \<Gamma>)\<cdot>ae) \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
-      apply (rule below_trans[OF _ Abinds_Afix_below])
-      apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
-      apply simp
-      done
-    thus "Afix \<Delta>\<cdot>ae \<sqsubseteq> Afix (\<Delta> @ \<Gamma>)\<cdot>ae"
-      apply (rule Afix_least_below)
-      apply (rule Afix_above_arg)
-      done
-  qed
-qed
-
-
-lemma Afix_e_to_heap:
-   "Afix (delete x \<Gamma>)\<cdot>(fup\<cdot>(Aexp e)\<cdot>n \<squnion> ae) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>n \<squnion> ae)"
-    apply (simp add: Afix_eq)
-    apply (rule fix_least_below, simp)
-    apply (intro join_below)
-    apply (subst fix_eq, simp)
-    apply (subst fix_eq, simp)
-
-    apply (rule below_trans[OF _ join_above2])
-    apply (rule below_trans[OF _ join_above2])
-    apply (rule below_trans[OF _ join_above2])
-    apply (rule monofun_cfun_arg)
-    apply (subst fix_eq, simp)
-      
-    apply (subst fix_eq, simp) back apply (simp add: below_trans[OF _ join_above2])
-    done
-
-lemma Afix_e_to_heap':
-   "Afix (delete x \<Gamma>)\<cdot>(Aexp e\<cdot>n) \<sqsubseteq> Afix ((x, e) # delete x \<Gamma>)\<cdot>(esing x\<cdot>(up\<cdot>n))"
-using Afix_e_to_heap[where ae = \<bottom> and n = "up\<cdot>n"] by simp
-
-end
-
 context SubstArityAnalysis
 begin
 
index bacb21f..94f10bb 100644 (file)
@@ -5,4 +5,25 @@ begin
 locale ArityAnalysis =
   fixes Aexp :: "exp \<Rightarrow> Arity \<rightarrow> AEnv"
 
+locale ArityAnalysisHeap =
+  fixes Aheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> AEnv"
+
+locale EdomArityAnalysis = ArityAnalysis + 
+  assumes Aexp_edom: "edom (Aexp e\<cdot>a) \<subseteq> fv e"
+begin
+
+  lemma fup_Aexp_edom: "edom (fup\<cdot>(Aexp e)\<cdot>a) \<subseteq> fv e"
+    by (cases a) (auto dest:set_mp[OF Aexp_edom])
+  
+  lemma Aexp_fresh_bot[simp]: assumes "atom v \<sharp> e" shows "(Aexp e\<cdot>a) v = \<bottom>"
+  proof-
+    from assms have "v \<notin> fv e" by (metis fv_not_fresh)
+    with Aexp_edom have "v \<notin> edom (Aexp e\<cdot>a)" by auto
+    thus ?thesis unfolding edom_def by simp
+  qed
+end
+
+locale ArityAnalysisHeapEqvt = ArityAnalysisHeap + 
+  assumes Aheap_eqvt[eqvt]: "\<pi> \<bullet> Aheap = Aheap"
+
 end
index 04c160f..d89de6c 100644 (file)
@@ -2,22 +2,6 @@ theory ArityAnalysisSpec
 imports ArityAnalysisAbinds
 begin
 
-locale EdomArityAnalysis = ArityAnalysis + 
-  assumes Aexp_edom: "edom (Aexp e\<cdot>a) \<subseteq> fv e"
-begin
-
-  lemma fup_Aexp_edom: "edom (fup\<cdot>(Aexp e)\<cdot>a) \<subseteq> fv e"
-    by (cases a) (auto dest:set_mp[OF Aexp_edom])
-  
-  lemma Aexp_fresh_bot[simp]: assumes "atom v \<sharp> e" shows "(Aexp e\<cdot>a) v = \<bottom>"
-  proof-
-    from assms have "v \<notin> fv e" by (metis fv_not_fresh)
-    with Aexp_edom have "v \<notin> edom (Aexp e\<cdot>a)" by auto
-    thus ?thesis unfolding edom_def by simp
-  qed
-
-end
-
 locale SubstArityAnalysis = EdomArityAnalysis + 
   assumes Aexp_subst_restr: "x \<notin> S \<Longrightarrow> y \<notin> S \<Longrightarrow> (Aexp e[x::=y] \<cdot> a) f|` S = (Aexp e\<cdot>a) f|` S"
 
@@ -26,28 +10,16 @@ locale CorrectArityAnalysis = SubstArityAnalysis +
   assumes Aexp_App: "Aexp e \<cdot>(inc\<cdot>n) \<squnion> esing x \<cdot> (up\<cdot>0) \<sqsubseteq>  Aexp (App e x) \<cdot> n"
   assumes Aexp_Lam: "env_delete y (Aexp e \<cdot>(pred\<cdot>n)) \<sqsubseteq> Aexp (Lam [y]. e) \<cdot> n"
 
-locale CorrectArityAnalysisAheap = CorrectArityAnalysis + 
-  fixes Aheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> AEnv"
-  assumes Aheap_eqvt[eqvt]: "\<pi> \<bullet> Aheap = Aheap"
+locale CorrectArityAnalysisHeap = CorrectArityAnalysis + ArityAnalysisHeapEqvt +
   assumes edom_Aheap: "edom (Aheap \<Gamma> e\<cdot> a) \<subseteq> domA \<Gamma>"
   assumes Aheap_subst: "x \<notin> domA \<Gamma> \<Longrightarrow> y \<notin> domA \<Gamma> \<Longrightarrow> Aheap \<Gamma>[x::h=y] e[x ::=y]  = Aheap \<Gamma> e"
 
-locale CorrectArityAnalysisLet = CorrectArityAnalysisAheap +
+locale CorrectArityAnalysisLet = CorrectArityAnalysisHeap +
   assumes Aexp_Let: "ABinds \<Gamma>\<cdot>(Aheap \<Gamma> e\<cdot>a) \<squnion> Aexp e\<cdot>a \<sqsubseteq> Aheap \<Gamma> e\<cdot>a \<squnion> Aexp (Let \<Gamma> e)\<cdot>a"
 
 locale CorrectArityAnalysisLetNoCard = CorrectArityAnalysisLet +
   assumes Aheap_heap3: "x \<in> thunks \<Gamma> \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
 
-context EdomArityAnalysis
-begin
-  lemma fup_Aexp_lookup_fresh: "atom v \<sharp> e \<Longrightarrow> (fup\<cdot>(Aexp e)\<cdot>a) v = \<bottom>"
-    by (cases a) auto
-  
-  lemma edom_AnalBinds: "edom (ABinds \<Gamma>\<cdot>ae) \<subseteq> fv \<Gamma>"
-    by (induction \<Gamma> rule: ABinds.induct)
-       (auto simp del: fun_meet_simp dest: set_mp[OF fup_Aexp_edom] dest: set_mp[OF fv_delete_subset])
-end 
-
 context SubstArityAnalysis
 begin
   lemma Aexp_subst_upd: "(Aexp e[y::=x]\<cdot>n) \<sqsubseteq> (Aexp e\<cdot>n)(y := \<bottom>, x := up\<cdot>0)"
diff --git a/Launchbury/ArityEtaExpand.thy b/Launchbury/ArityEtaExpand.thy
deleted file mode 100644 (file)
index bbb4e6a..0000000
+++ /dev/null
@@ -1,286 +0,0 @@
-theory ArityEtaExpand
-imports ArityAnalysisSpec ArityEtaExpansionSestoft AbstractTransform ConstOn
-begin
-
-locale CardinalityArityTransformation = CorrectArityAnalysisLetNoCard 
-begin
-
-  sublocale AbstractTransformBound
-    "\<lambda> a . inc\<cdot>a"
-    "\<lambda> a . pred\<cdot>a"
-    "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
-    "fst"
-    "snd"
-    "Aeta_expand"
-    "snd"
-  apply default
-  apply (((rule eq_reflection)?, perm_simp, rule)+)[7]
-  done
-
-  sublocale AbstractTransformBoundSubst
-    "\<lambda> a . inc\<cdot>a"
-    "\<lambda> a . pred\<cdot>a"
-    "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
-    "fst"
-    "snd"
-    "Aeta_expand"
-    "snd"
-  apply default
-  apply (simp add: Aheap_subst)
-  apply (rule subst_Aeta_expand)
-  done
-
-  abbreviation aTransform where "aTransform \<equiv> transform"
-
-  lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
-    by (induction rule: transform.induct)
-       (auto simp add: exp_assn.supp Let_supp dest!: set_mp[OF supp_map_transform] set_mp[OF supp_map_transform_step] )
-  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)"
-
-  inductive consistent :: "(AEnv \<times> Arity) \<Rightarrow> conf \<Rightarrow> bool" where
-    consistentI[intro!]: 
-    "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 \<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)"
-  
-  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'"
-  using assms
-  proof(induction c c' arbitrary: ae a 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)
-    moreover
-    have "conf_transform (ae, a) (\<Gamma>, App e x, S) \<Rightarrow> conf_transform (ae, inc\<cdot>a) (\<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
-
-  
-  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> isLam 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 `isLam e`
-  have "isLam (transform u e)" by simp
-  hence "isLam (Aeta_expand u (transform u e))" by (rule isLam_Aeta_expand)
-  moreover
-  from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u`  `isLam (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` `isLam (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 "Astack (Upd x # S) \<sqsubseteq> a" using var\<^sub>2 by auto
-  hence "a = 0" by auto
-
-  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)
-
-  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 "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])
-
-  have restr_stack_simp: "restr_stack (edom (?ae \<squnion> ae)) S = restr_stack (edom ae) S"
-    by (auto intro: restr_stack_cong dest!: *)
-
-  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])
-
-  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 \<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)
-    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)
-    ultimately
-
-    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
-
-end
-
-
-end
diff --git a/Launchbury/ArityEtaExpandCorrect.thy b/Launchbury/ArityEtaExpandCorrect.thy
new file mode 100644 (file)
index 0000000..d0c0176
--- /dev/null
@@ -0,0 +1,274 @@
+theory ArityEtaExpandCorrect
+imports ArityEtaExpand  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"
+    "Aeta_expand"
+    "snd"
+  apply default
+  apply (simp add: Aheap_subst)
+  apply (rule subst_Aeta_expand)
+  done
+
+  abbreviation aTransform where "aTransform \<equiv> transform"
+
+  lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
+    by (induction rule: transform.induct)
+       (auto simp add: exp_assn.supp Let_supp dest!: set_mp[OF supp_map_transform] set_mp[OF supp_map_transform_step] )
+  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)"
+
+  inductive consistent :: "(AEnv \<times> Arity) \<Rightarrow> conf \<Rightarrow> bool" where
+    consistentI[intro!]: 
+    "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 \<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)"
+  
+  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'"
+  using assms
+  proof(induction c c' arbitrary: ae a 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)
+    moreover
+    have "conf_transform (ae, a) (\<Gamma>, App e x, S) \<Rightarrow> conf_transform (ae, inc\<cdot>a) (\<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
+
+  
+  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> isLam 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 `isLam e`
+  have "isLam (transform u e)" by simp
+  hence "isLam (Aeta_expand u (transform u e))" by (rule isLam_Aeta_expand)
+  moreover
+  from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u`  `isLam (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` `isLam (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 "Astack (Upd x # S) \<sqsubseteq> a" using var\<^sub>2 by auto
+  hence "a = 0" by auto
+
+  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)
+
+  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 "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])
+
+  have restr_stack_simp: "restr_stack (edom (?ae \<squnion> ae)) S = restr_stack (edom ae) S"
+    by (auto intro: restr_stack_cong dest!: *)
+
+  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])
+
+  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 \<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)
+    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)
+    ultimately
+
+    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
+
+end
+
+
+end
index a9f0af0..4ac5bc8 100644 (file)
@@ -1,36 +1,24 @@
 theory CallArityCorrectEnd2End
-imports CardinalityEtaExpand CoCallImplCorrect CoCallImplFTreeCorrect FTreeCardinality "~~/src/Tools/Permanent_Interpretation" 
+imports CallArityEnd2End CardinalityEtaExpandCorrect CoCallImplCorrect CoCallImplFTreeCorrect FTreeImplCardinalityCorrect
 begin
 
-interpretation CoCallImplCorrect.
-
-thm CardinalityArityTransformation.foo
-
-print_locales
-print_interps FTreeAnalysisCarrier
-print_interps CardinalityPrognosisCorrectLet
-print_interps CardinalityArityTransformation
-
-
-permanent_interpretation CardinalityArityTransformation prognosis Aexp Aheap cHeap
-  defining final_consistent = consistent
-  and final_conf_transform = conf_transform
-  and final_transform = "AbstractTransform.transform (Rep_cfun inc) (Rep_cfun pred) (\<lambda>\<Delta> e a. (a, Aheap \<Delta> e\<cdot>a)) fst snd (\<lambda>a. Var) (\<lambda>a. Var1) (\<lambda>a. App) (\<lambda>a v e . Lam [v]. e)
-  (\<lambda>b \<Gamma>. Terms.Let (map_transform Aeta_expand (snd b) \<Gamma>))"
-   by default
+locale CallArityCorrectEnd2End
+begin
+sublocale CoCallImplCorrect.
+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> final_conf_transform  (ae, ce, a) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform  (ae', ce', a') c'"
+  \<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'"
   by (rule foo)
 
 lemma end2end_closed:
   assumes closed: "fv e = ({} :: var set)"
   assumes "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>,v,[])"
   assumes "isLam v"
-  shows "\<exists> \<Gamma>' v'. length \<Gamma>' \<le> length \<Gamma> \<and> isLam v' \<and> ([], final_transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (\<Gamma>',v',[])"
+  shows "\<exists> \<Gamma>' v'. length \<Gamma>' \<le> length \<Gamma> \<and> isLam v' \<and> ([], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (\<Gamma>',v',[])"
 proof-
   note assms(2)
   moreover
@@ -40,20 +28,20 @@ proof-
   ultimately
   obtain ae ce a where
     *: "consistent  (ae, ce, a) (\<Gamma>,v,[])" and
-    **: "final_conf_transform  (\<bottom>, \<bottom>, 0) ([],e,[]) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a) (\<Gamma>,v,[])"
+    **: "conf_transform  (\<bottom>, \<bottom>, 0) ([],e,[]) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a) (\<Gamma>,v,[])"
     by (metis end2end)
 
-  let ?\<Gamma> = "restrictA (edom ce) (map_transform Aeta_expand ae (map_transform final_transform ae \<Gamma>))"
-  let ?v = "final_transform a v"
+  let ?\<Gamma> = "restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))"
+  let ?v = "transform a v"
 
   show ?thesis
   proof(intro exI conjI)
-    show "length (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform final_transform ae \<Gamma>))) \<le> length \<Gamma>"
+    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
 
-    have "final_conf_transform  (\<bottom>, \<bottom>, 0) ([],e,[]) = ([],final_transform 0 e,[])" by simp
+    have "conf_transform  (\<bottom>, \<bottom>, 0) ([],e,[]) = ([],transform 0 e,[])" by simp
     with **
-    show "([], final_transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (?\<Gamma>, ?v, [])" by simp
+    show "([], transform 0 e, []) \<Rightarrow>\<^sub>G\<^sup>* (?\<Gamma>, ?v, [])" by simp
 
     show "isLam (transform a v)" using `isLam v` by simp
   qed
@@ -67,11 +55,11 @@ lemma example1:
   fixes f g x y z :: var
   assumes Aexp_e: "\<And>a. Aexp e\<cdot>a = esing x\<cdot>(up\<cdot>a) \<squnion> esing y\<cdot>(up\<cdot>a)"
   assumes ccExp_e: "\<And>a. CCexp e\<cdot>a = \<bottom>"
-  assumes [simp]: "final_transform 1 e = e"
+  assumes [simp]: "transform 1 e = e"
   assumes "isLam e"
   assumes disj: "y \<noteq> f" "y \<noteq> g" "x \<noteq> y" "z \<noteq> f" "z \<noteq> g" "y \<noteq> x"
   assumes fresh: "atom z \<sharp> e"
-  shows "final_transform 1 (let y be  App (Var f) g in (let x be e in (Var x))) = 
+  shows "transform 1 (let y be  App (Var f) g in (let x be e in (Var x))) = 
          let y be (Lam [z]. App (App (Var f) g) z) in (let x be (Lam [z]. App e z) in (Var x))"
 proof-
   from arg_cong[where f = edom, OF Aexp_e]
@@ -122,10 +110,10 @@ proof-
     apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj fresh intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
     done
 
-
   show ?thesis
     by (simp del: Let_eq_iff add: map_transform_Cons map_transform_Nil disj[symmetric])
 qed
 
 
 end
+end
diff --git a/Launchbury/CallArityEnd2End.thy b/Launchbury/CallArityEnd2End.thy
new file mode 100644 (file)
index 0000000..5762092
--- /dev/null
@@ -0,0 +1,77 @@
+theory CallArityEnd2End
+imports ArityEtaExpand CoCallAnalysisImpl  CoCallImplFTree FTreeImplCardinality 
+begin
+
+locale CallArityEnd2End
+begin
+sublocale CoCallAnalysisImpl.
+
+lemma fresh_var_eqE[elim_format]: "fresh_var e = x \<Longrightarrow> x \<notin>  fv e"
+  by (metis fresh_var_not_free)
+
+lemma example1:
+  fixes e :: exp
+  fixes f g x y z :: var
+  assumes Aexp_e: "\<And>a. Aexp e\<cdot>a = esing x\<cdot>(up\<cdot>a) \<squnion> esing y\<cdot>(up\<cdot>a)"
+  assumes ccExp_e: "\<And>a. CCexp e\<cdot>a = \<bottom>"
+  assumes [simp]: "transform 1 e = e"
+  assumes "isLam e"
+  assumes disj: "y \<noteq> f" "y \<noteq> g" "x \<noteq> y" "z \<noteq> f" "z \<noteq> g" "y \<noteq> x"
+  assumes fresh: "atom z \<sharp> e"
+  shows "transform 1 (let y be  App (Var f) g in (let x be e in (Var x))) = 
+         let y be (Lam [z]. App (App (Var f) g) z) in (let x be (Lam [z]. App e z) in (Var x))"
+proof-
+  from arg_cong[where f = edom, OF Aexp_e]
+  have "x \<in> fv e" by simp (metis Aexp_edom' insert_subset)
+  hence "\<not> atom x \<sharp> e" by (simp add:fresh_def fv_def)
+  hence [simp]: "\<not> nonrec [(x,e)]"
+    by (simp add: nonrec_def)
+  from `isLam e`
+  have [simp]: "thunks [(x, e)] = {}"
+    by (simp add: thunks_Cons)
+
+  have [simp]: "CCfix [(x, e)]\<cdot>(esing x\<cdot>(up\<cdot>1) \<squnion> esing y\<cdot>(up\<cdot>1), \<bottom>) = \<bottom>"
+    unfolding CCfix_def
+    apply (simp add: fix_bottom_iff ccBindsExtra_simp)
+    apply (simp add: ccBind_eq disj ccExp_e)
+    done
+
+  have [simp]: "Afix [(x, e)]\<cdot>(esing x\<cdot>(up\<cdot>1)) = esing x\<cdot>(up\<cdot>1) \<squnion> esing y\<cdot>(up\<cdot>1)"
+    unfolding Afix_def
+    apply simp
+    apply (rule fix_eqI)
+    apply (simp add: disj Aexp_e)
+    apply (case_tac "z x")
+    apply (auto simp add: disj Aexp_e)
+    done
+
+  have [simp]: "Aheap [(y, App (Var f) g)] (let x be e in Var x)\<cdot>1 = esing y\<cdot>((Aexp (let x be e in Var x )\<cdot>1) y)"
+    by (auto simp add:  Aheap_nonrec_simp ABind_nonrec_eq pure_fresh fresh_at_base disj)
+
+  have [simp]: "(Aexp (let x be e in Var x)\<cdot>1) = esing y\<cdot>(up\<cdot>1)"
+    by (simp add: env_restr_join disj)
+    
+  have [simp]: "Aheap [(x, e)] (Var x)\<cdot>1 = esing x\<cdot>(up\<cdot>1)"
+    by (simp add: env_restr_join disj)
+
+  have 1: "1 = inc\<cdot>0" apply (simp add: inc_def) apply transfer apply simp done
+  
+  have [simp]: "Aeta_expand 1 (App (Var f) g) = (Lam [z]. App (App (Var f) g) z)"
+    apply (simp add: 1 del: exp_assn.eq_iff)
+    apply (subst change_Lam_Variable[of z "fresh_var (App (Var f) g)"])
+    apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
+    done
+
+  have [simp]: "Aeta_expand 1 e = (Lam [z]. App e z)"
+    apply (simp add: 1 del: exp_assn.eq_iff)
+    apply (subst change_Lam_Variable[of z "fresh_var e"])
+    apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj fresh intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
+    done
+
+  show ?thesis
+    by (simp del: Let_eq_iff add: map_transform_Cons map_transform_Nil disj[symmetric])
+qed
+
+end
+end
diff --git a/Launchbury/CardinalityAnalysis.thy b/Launchbury/CardinalityAnalysis.thy
deleted file mode 100644 (file)
index cb2d628..0000000
+++ /dev/null
@@ -1,44 +0,0 @@
-theory CardinalityAnalysis
-imports ArityAnalysisSpec "Cardinality-Domain" SestoftConf ConstOn
-begin
-
-locale CardinalityHeap = CorrectArityAnalysisLet +
-  fixes cHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> (var \<Rightarrow> two)"
-
-(*   assumes cHeap: "\<pi> \<bullet> cHeap = cHeap" *)
-  assumes Aheap_heap3: "x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> (cHeap \<Gamma> e\<cdot>a) x \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
-  assumes edom_cHeap: "edom (cHeap \<Delta> e\<cdot>a) = edom (Aheap \<Delta> e\<cdot>a)"
-
-locale CardinalityPrognosis = 
-  fixes prognosis :: "AEnv \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> (var \<Rightarrow> two)"
-
-locale CardinalityPrognosisCorrect = CardinalityPrognosis +
-  assumes prognosis_env_cong: "ae f|` domA \<Gamma> = ae' f|` domA \<Gamma> \<Longrightarrow> prognosis ae u (\<Gamma>, e, S) = prognosis ae' u (\<Gamma>, e, S)"
-  assumes prognosis_reorder: "map_of \<Gamma> = map_of \<Delta>  \<Longrightarrow>  prognosis ae u (\<Gamma>, e, S) = prognosis ae u (\<Delta>, e, S)"
-  assumes prognosis_delete: "prognosis ae u (delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, S)"
-  assumes prognosis_ap: "const_on (prognosis ae a (\<Gamma>, e, S)) (ap S) many"
-  assumes prognosis_upd: "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, Upd x # S)"
-
-
-  assumes prognosis_App: "prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, App e x, S)"
-  assumes prognosis_subst_Lam: "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae a (\<Gamma>, Lam [y]. e, Arg x # S)"
-  assumes prognosis_Var_lam: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> isLam e \<Longrightarrow> prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-  assumes prognosis_Var_thunk: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> \<not> isLam e \<Longrightarrow> prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-  assumes prognosis_Var2: "isLam e \<Longrightarrow> x \<notin> domA \<Gamma> \<Longrightarrow> prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)"
-
-  assumes prognosis_not_called: "ae x = \<bottom> \<Longrightarrow> prognosis ae a (\<Gamma>, e, S) \<sqsubseteq> prognosis ae a (delete x \<Gamma>, e, S)"
-
-  assumes prognosis_called: "once \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S) x"
-
-
-
-locale CardinalityPrognosisCorrectLet = CardinalityPrognosisCorrect + CardinalityHeap +
-  assumes prognosis_Let:
-  "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> edom ae \<subseteq> domA \<Gamma> \<union> upds S \<Longrightarrow> prognosis (Aheap \<Delta> e\<cdot>a \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae a (\<Gamma>, Terms.Let \<Delta> e, S)"
-
-locale CardinalityPrognosisEdom = CardinalityPrognosis + CorrectArityAnalysisAheap +
-  assumes edom_prognosis:
-    "edom (prognosis ae a (\<Gamma>, e, S)) \<subseteq> fv \<Gamma> \<union> fv e \<union> fv S"
-
-
-end
diff --git a/Launchbury/CardinalityAnalysisSig.thy b/Launchbury/CardinalityAnalysisSig.thy
new file mode 100644 (file)
index 0000000..5731ea5
--- /dev/null
@@ -0,0 +1,10 @@
+theory CardinalityAnalysisSig
+imports Arity AEnv "Cardinality-Domain" SestoftConf
+begin
+
+locale CardinalityPrognosis = 
+  fixes prognosis :: "AEnv \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> (var \<Rightarrow> two)"
+
+locale CardinalityHeap = 
+  fixes cHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> (var \<Rightarrow> two)"
+end
diff --git a/Launchbury/CardinalityAnalysisSpec.thy b/Launchbury/CardinalityAnalysisSpec.thy
new file mode 100644 (file)
index 0000000..1d2ee44
--- /dev/null
@@ -0,0 +1,47 @@
+theory CardinalityAnalysisSpec
+imports ArityAnalysisSpec CardinalityAnalysisSig ConstOn
+begin
+
+locale CardinalityPrognosisEdom = CardinalityPrognosis +
+  assumes edom_prognosis:
+    "edom (prognosis ae a (\<Gamma>, e, S)) \<subseteq> fv \<Gamma> \<union> fv e \<union> fv S"
+
+locale CardinalityPrognosisShape = CardinalityPrognosis +
+  assumes prognosis_env_cong: "ae f|` domA \<Gamma> = ae' f|` domA \<Gamma> \<Longrightarrow> prognosis ae u (\<Gamma>, e, S) = prognosis ae' u (\<Gamma>, e, S)"
+  assumes prognosis_reorder: "map_of \<Gamma> = map_of \<Delta>  \<Longrightarrow>  prognosis ae u (\<Gamma>, e, S) = prognosis ae u (\<Delta>, e, S)"
+  assumes prognosis_delete: "prognosis ae u (delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, S)"
+  assumes prognosis_ap: "const_on (prognosis ae a (\<Gamma>, e, S)) (ap S) many"
+  assumes prognosis_upd: "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, Upd x # S)"
+  assumes prognosis_not_called: "ae x = \<bottom> \<Longrightarrow> prognosis ae a (\<Gamma>, e, S) \<sqsubseteq> prognosis ae a (delete x \<Gamma>, e, S)"
+  assumes prognosis_called: "once \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S) x"
+
+locale CardinalityPrognosisApp = CardinalityPrognosis +
+  assumes prognosis_App: "prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, App e x, S)"
+
+locale CardinalityPrognosisLam = CardinalityPrognosis +
+  assumes prognosis_subst_Lam: "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae a (\<Gamma>, Lam [y]. e, Arg x # S)"
+
+locale CardinalityPrognosisVar = CardinalityPrognosis +
+  assumes prognosis_Var_lam: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> isLam e \<Longrightarrow> prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+  assumes prognosis_Var_thunk: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> \<not> isLam e \<Longrightarrow> prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+  assumes prognosis_Var2: "isLam e \<Longrightarrow> x \<notin> domA \<Gamma> \<Longrightarrow> prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)"
+
+locale CardinalityPrognosisLet = CardinalityPrognosis + CardinalityHeap + ArityAnalysisHeap +
+  assumes prognosis_Let:
+  "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> edom ae \<subseteq> domA \<Gamma> \<union> upds S \<Longrightarrow> prognosis (Aheap \<Delta> e\<cdot>a \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae a (\<Gamma>, Terms.Let \<Delta> e, S)"
+
+locale CardinalityHeapCorrect = CardinalityHeap + ArityAnalysisHeap +
+  assumes Aheap_heap3: "x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> (cHeap \<Gamma> e\<cdot>a) x \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
+  assumes edom_cHeap: "edom (cHeap \<Delta> e\<cdot>a) = edom (Aheap \<Delta> e\<cdot>a)"
+
+locale CardinalityPrognosisCorrect =
+  CardinalityPrognosisEdom +
+  CardinalityPrognosisShape +
+  CardinalityPrognosisApp +
+  CardinalityPrognosisLam + 
+  CardinalityPrognosisVar +
+  CardinalityPrognosisLet +
+  CardinalityHeapCorrect +
+  CorrectArityAnalysisLet
+
+end
diff --git a/Launchbury/CardinalityEtaExpand.thy b/Launchbury/CardinalityEtaExpand.thy
deleted file mode 100644 (file)
index c994cce..0000000
+++ /dev/null
@@ -1,519 +0,0 @@
-theory CardinalityEtaExpand
-imports CardinalityAnalysis AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft
-begin
-
-locale CardinalityArityTransformation = CardinalityPrognosisCorrectLet + CardinalityPrognosisEdom
-begin
-
-  sublocale AbstractTransformBound
-    "\<lambda> a . inc\<cdot>a"
-    "\<lambda> a . pred\<cdot>a"
-    "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
-    "fst"
-    "snd"
-    "Aeta_expand"
-    "snd"
-  apply default
-  apply (((rule eq_reflection)?, perm_simp, rule)+)[7]
-  done
-
-  sublocale AbstractTransformBoundSubst
-    "\<lambda> a . inc\<cdot>a"
-    "\<lambda> a . pred\<cdot>a"
-    "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
-    "fst"
-    "snd"
-    "Aeta_expand"
-    "snd"
-  apply default
-  apply (simp add: Aheap_subst)
-  apply (rule subst_Aeta_expand)
-  done
-
-  abbreviation ccTransform where "ccTransform \<equiv> transform"
-
-  lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
-    by (induction rule: transform.induct)
-       (auto simp add: exp_assn.supp Let_supp dest!: set_mp[OF supp_map_transform] set_mp[OF supp_map_transform_step] )
-  interpretation supp_bounded_transform transform
-    by default (auto simp add: fresh_def supp_transform) 
-
-  type_synonym tstate = "(AEnv \<times> (var \<Rightarrow> two) \<times> Arity)"
-
-  fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
-  where "conf_transform (ae, ce,  a) (\<Gamma>, e, S) =
-    (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)), 
-     ccTransform a e,
-     restr_stack (edom ce) S)"
-
-  definition anal_env :: "(exp \<Rightarrow> 'a::cpo \<rightarrow> 'b::pcpo) \<Rightarrow> heap \<Rightarrow> (var \<Rightarrow> 'a\<^sub>\<bottom>) \<rightarrow> (var \<Rightarrow> 'b)"
-    where "anal_env f \<Gamma> = (\<Lambda> e. (\<lambda> x . fup\<cdot>(f (the (map_of \<Gamma> x)))\<cdot>(e x)))"
-
-
-  inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
-    consistentI[intro!]: 
-    "edom ce \<subseteq> domA \<Gamma> \<union> upds S
-    \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
-    \<Longrightarrow> edom ae = edom ce
-    \<Longrightarrow> Astack (restr_stack (edom ce) S) \<sqsubseteq> a
-    \<Longrightarrow> prognosis ae a (\<Gamma>, e, S) \<sqsubseteq> ce
-    \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a) f|` edom ce \<sqsubseteq> ae
-    \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
-    \<Longrightarrow> const_on ae (ap S \<inter> edom ce) (up\<cdot>0)
-    \<Longrightarrow> const_on ae (upds S \<inter> edom ce) (up\<cdot>0)
-    \<Longrightarrow> consistent (ae, ce, a) (\<Gamma>, e, S)"  
-  inductive_cases consistentE[elim!]: "consistent (ae, ce, a) (\<Gamma>, e, S)"
-
-  lemma closed_consistent:
-    assumes "fv e = ({}::var set)"
-    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)
-  qed
-
-  lemma foo:
-    fixes c c' R 
-    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a) c"
-    shows "\<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'"
-  using assms
-  proof(induction c c' arbitrary: ae ce a rule:step_induction)
-  case (app\<^sub>1 \<Gamma> e x S)
-    have "prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, App e x, S)" by (rule prognosis_App)
-    with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a) (\<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)
-    moreover
-    have "conf_transform (ae, ce, a) (\<Gamma>, App e x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, inc\<cdot>a) (\<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 "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae 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)
-    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
-    have "consistent (ae, ce, pred\<cdot>a) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
-      by (auto elim: below_trans edom_mono  simp add: join_below_iff env_restr_join)
-    moreover
-    have "conf_transform (ae, ce, a) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 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 "prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
-    from below_trans[OF prognosis_called fun_belowD[OF this] ]
-    have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
-  
-    from thunk
-    have "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> 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) f|` edom ce \<sqsubseteq> ae" by simp
-
-    show ?case
-    proof(cases "ce x" rule:two_cases)
-      case none
-      with `x \<in> edom ce` have False by (auto simp add: edom_def)
-      thus ?thesis..
-    next
-      case once
-
-      note `ae x = up\<cdot>u` 
-      moreover
-  
-      from `prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce`
-      have "prognosis ae a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
-        using once by (metis (mono_tags) fun_belowD)
-      hence "x \<notin> ap S" using prognosis_ap[of ae a \<Gamma> "(Var x)" S] by auto
-      
-  
-      from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isLam e`
-      have *: "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-        by (rule prognosis_Var_thunk)
-  
-      from `prognosis ae a (\<Gamma>, Var x, S) x \<sqsubseteq> once`
-      have "(record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))) x = none"
-        by (simp add: two_pred_none)
-      hence **: "prognosis ae u (delete x \<Gamma>, e, Upd x # S) x = none" using fun_belowD[OF *, where x = x] by auto
-
-      have eq: "prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S) = prognosis ae u (delete x \<Gamma>, e, Upd x # S)"
-        by (rule prognosis_env_cong) simp
-
-      have [simp]: "restr_stack (edom ce - {x}) S = restr_stack (edom ce) S" 
-        using `x \<notin> upds S` by (auto intro: restr_stack_cong)
-    
-      have "prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
-        unfolding eq
-        using ** below_trans[OF below_trans[OF * Cfun.monofun_cfun_arg[OF `prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce`]] record_call_below_arg]
-        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) f|\` edom ce \<sqsubseteq> ae`
-      have "(ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u) 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) f|` edom (env_delete x ce) \<sqsubseteq> env_delete x ae"
-        by (auto simp add: Diff_eq Int_commute env_delete_restr)
-
-      moreover
-  
-      have "const_on ae (ap S \<inter> edom ce) (up\<cdot>0)" using thunk by auto
-      hence "const_on (env_delete x ae) (ap S \<inter> edom ce) (up\<cdot>0)" using `x \<notin>  ap S`
-        by (fastforce simp add: env_delete_def)
-      moreover
-  
-      have "const_on ae (upds S \<inter> edom ce) (up\<cdot>0)" using thunk by auto
-      hence "const_on (env_delete x ae) (upds S \<inter> (edom (env_delete x ce))) (up\<cdot>0)" by fastforce
-      ultimately
-
-      have "consistent (env_delete x ae, env_delete x ce, u) (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])
-      moreover
-      
-      {
-      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))"
-        by (simp add: map_of_map_transform)
-      hence "conf_transform (ae, ce, a) (\<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 # 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), 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, restr_stack (edom ce) S)"
-        by (intro normal_trans Aeta_expand_correct `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`)
-      also(rtranclp_trans)
-      have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u) (delete x \<Gamma>, e, Upd x # S)" 
-        by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist)
-      finally(back_subst)
-      have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (env_delete x ae, env_delete x ce, u) (delete x \<Gamma>, e, Upd x # S)".
-      }
-      ultimately
-      show ?thesis by (blast del: consistentI consistentE)
-  
-    next
-      case many
-  
-      from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isLam e`
-      have "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-        by (rule prognosis_Var_thunk)
-      also note record_call_below_arg
-      finally
-      have *: "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)" by this simp_all
-  
-      have "ae x = up\<cdot>0" using thunk many `x \<in> thunks \<Gamma>` by (auto)
-      hence "u = 0" using `ae x = up\<cdot>u` by simp
-  
-      
-      have "prognosis ae 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) f|\` edom ce \<sqsubseteq> ae`
-      ultimately
-      have "consistent (ae, ce, 0) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`  by auto
-      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)"
-        by (simp add: map_of_map_transform)
-      with `\<not> isLam e`
-      have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 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 ?thesis by (blast del: consistentI consistentE)
-    qed
-  next
-  case (lamvar \<Gamma> x e S)
-    from lamvar have "prognosis ae 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)
-
-    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 u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae u (\<Gamma>, e, S)"
-      using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
-    also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-       using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isLam e`  by (rule prognosis_Var_lam)
-    also have "\<dots> \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
-    finally have *: "prognosis ae u ((x, e) # delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)" by this simp_all
-  
-    have "consistent (ae, ce, u) ((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 *])
-    moreover
-  
-    have "Astack (restr_stack (edom ce) S) \<sqsubseteq> u" using lamvar below_trans[OF _ `a \<sqsubseteq> u`] by auto
-  
-    {
-    from `isLam e`
-    have "isLam (transform u e)" by simp
-    hence "isLam (Aeta_expand u (transform u e))" by (rule isLam_Aeta_expand)
-    moreover
-    from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isLam (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))"
-      by (simp add: map_of_map_transform)
-    ultimately
-    have "conf_transform (ae, ce, a) (\<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), 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), restr_stack (edom ce) S)"
-      using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isLam (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) ((x, e) # delete x \<Gamma>, e, S)"
-      by simp (rule Aeta_expand_correct[OF `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`])
-    finally(rtranclp_trans)
-    have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* conf_transform (ae, ce, u) ((x, e) # delete x \<Gamma>, e, S)".
-    }
-    ultimately show ?case by (blast intro: normal_trans del: consistentI consistentE)
-  next
-  case (var\<^sub>2 \<Gamma> x e S)
-    show ?case
-    proof(cases "x \<in> edom ce")
-      case True[simp]
-      hence "ce x \<noteq> \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
-      hence "ae x = up\<cdot>a" 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 `isLam e` `x \<notin> domA \<Gamma>`
-      have *: "prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
-
-      have "consistent (ae, ce, 0) ((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 *])
-      moreover
-      have "conf_transform (ae, ce, a) (\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0) ((x, e) # \<Gamma>, e, S)"
-        using `ae x = up\<cdot>a` `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
-      case False[simp]
-      hence "ce x = \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
-
-      from False have "x \<notin> edom ae" using var\<^sub>2 by auto
-      hence [simp]: "ae x = \<bottom>" by (auto simp add: edom_def)
-
-      
-      have "prognosis ae a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae a ((x, e) # \<Gamma>, e, Upd x # S)" by (rule prognosis_upd)
-      also
-       
-      from `ae x = \<bottom>`
-      have "prognosis ae a ((x, e) # \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
-        by (rule prognosis_not_called)
-      also have  "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
-      finally
-      have *: "prognosis ae a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae a (\<Gamma>, e, Upd x # S)" by this simp
-
-      have "consistent (ae, ce, a) ((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 *])
-      moreover
-      have "conf_transform (ae, ce, a) (\<Gamma>, e, Upd x # S) = conf_transform (ae, ce, a) ((x, e) # \<Gamma>, e, S)"
-        by(simp add: map_transform_restrA[symmetric])
-      ultimately show ?thesis by (auto del: consistentI consistentE)
-    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"
-      by (auto intro: restr_stack_cong dest!: *)
-  
-    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 "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 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)
-
-  
-    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
-    { fix x e'
-      assume "x \<in> thunks \<Gamma>"
-      hence "x \<notin> edom ?ce" using fresh_distinct[OF let\<^sub>1(1)]
-        by (auto simp add: edom_cHeap dest: set_mp[OF edom_Aheap]  set_mp[OF thunks_domA])
-      hence [simp]: "?ce x = \<bottom>" unfolding edomIff by auto
-    
-      assume "many \<sqsubseteq> (?ce \<squnion> ce) x"
-      with let\<^sub>1 `x \<in> thunks \<Gamma>`
-      have "(?ae \<squnion> ae) x = up \<cdot>0" by auto
-    }
-    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 "x \<notin> edom ce" using let\<^sub>1 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 "const_on ae (ap S \<inter> edom ce) (up\<cdot>0)" using let\<^sub>1 by auto  
-    hence "const_on (?ae \<squnion> ae) (ap S \<inter> edom ce) (up\<cdot>0)" by fastforce
-    hence "const_on (?ae \<squnion> ae) (ap S \<inter> edom (?ce \<squnion> ce)) (up\<cdot>0)" by (simp add: Int_Un_distrib)
-    moreover
-    have "const_on ae (upds (restr_stack (edom ce) S)) (up\<cdot>0)" using let\<^sub>1 by auto
-    hence "const_on (?ae \<squnion> ae) (upds (restr_stack (edom ce) S)) (up\<cdot>0)"  by fastforce
-    hence "const_on (?ae \<squnion> ae) (upds (restr_stack (edom (?ce \<squnion> ce)) S)) (up\<cdot>0)" 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) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> prognosis ae a (\<Gamma>, Let \<Delta> e, S)" by (rule prognosis_Let)
-    also have "prognosis ae a (\<Gamma>, Let \<Delta> e, S) \<sqsubseteq> ce" using let\<^sub>1 by auto
-    finally have "prognosis (?ae \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
-    }
-    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)
-    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) 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])
-    ultimately
-    have "(ABinds (\<Delta> @ \<Gamma>) \<cdot> (Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a) 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)
-    }
-    ultimately
-    have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a) (\<Delta> @ \<Gamma>, e, S) "
-      by auto
-    }
-    moreover
-    {
-      have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
-        using fresh_distinct[OF let\<^sub>1(1)]
-        by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
-      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>))"
-         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
-      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 intro!: map_transform_cong restrictA_cong simp add: edomIff)
-      ultimately
-  
-      have "conf_transform (ae, ce, a) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (?ae \<squnion> ae, ?ce \<squnion> ce, a) (\<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])
-    }
-    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' ce' a' where "consistent (ae', ce', a') c'" and *: "conf_transform (ae, ce, a) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae', ce', a') c'" by blast
-      from trans(4)[OF this(1)]
-      obtain ae'' ce'' a'' where "consistent (ae'', ce'', a'') c''" and **: "conf_transform (ae', ce', a') c' \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae'', ce'', a'') c''" by blast
-      from this(1) rtranclp_trans[OF * **]
-      show ?case by blast
-  qed
-
-end
-
-end
diff --git a/Launchbury/CardinalityEtaExpandCorrect.thy b/Launchbury/CardinalityEtaExpandCorrect.thy
new file mode 100644 (file)
index 0000000..a68ccef
--- /dev/null
@@ -0,0 +1,506 @@
+theory CardinalityEtaExpandCorrect
+imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft
+begin
+
+context CardinalityPrognosisCorrect
+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"
+    "Aeta_expand"
+    "snd"
+  apply default
+  apply (simp add: Aheap_subst)
+  apply (rule subst_Aeta_expand)
+  done
+
+  abbreviation ccTransform where "ccTransform \<equiv> transform"
+
+  lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
+    by (induction rule: transform.induct)
+       (auto simp add: exp_assn.supp Let_supp dest!: set_mp[OF supp_map_transform] set_mp[OF supp_map_transform_step] )
+  interpretation supp_bounded_transform transform
+    by default (auto simp add: fresh_def supp_transform) 
+
+  type_synonym tstate = "(AEnv \<times> (var \<Rightarrow> two) \<times> Arity)"
+
+  fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
+  where "conf_transform (ae, ce,  a) (\<Gamma>, e, S) =
+    (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)), 
+     ccTransform a e,
+     restr_stack (edom ce) S)"
+
+  definition anal_env :: "(exp \<Rightarrow> 'a::cpo \<rightarrow> 'b::pcpo) \<Rightarrow> heap \<Rightarrow> (var \<Rightarrow> 'a\<^sub>\<bottom>) \<rightarrow> (var \<Rightarrow> 'b)"
+    where "anal_env f \<Gamma> = (\<Lambda> e. (\<lambda> x . fup\<cdot>(f (the (map_of \<Gamma> x)))\<cdot>(e x)))"
+
+
+  inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
+    consistentI[intro!]: 
+    "edom ce \<subseteq> domA \<Gamma> \<union> upds S
+    \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
+    \<Longrightarrow> edom ae = edom ce
+    \<Longrightarrow> Astack (restr_stack (edom ce) S) \<sqsubseteq> a
+    \<Longrightarrow> prognosis ae a (\<Gamma>, e, S) \<sqsubseteq> ce
+    \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a) f|` edom ce \<sqsubseteq> ae
+    \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
+    \<Longrightarrow> const_on ae (ap S \<inter> edom ce) (up\<cdot>0)
+    \<Longrightarrow> const_on ae (upds S \<inter> edom ce) (up\<cdot>0)
+    \<Longrightarrow> consistent (ae, ce, a) (\<Gamma>, e, S)"  
+  inductive_cases consistentE[elim!]: "consistent (ae, ce, a) (\<Gamma>, e, S)"
+
+  lemma closed_consistent:
+    assumes "fv e = ({}::var set)"
+    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)
+  qed
+
+  lemma foo:
+    fixes c c' R 
+    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a) c"
+    shows "\<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'"
+  using assms
+  proof(induction c c' arbitrary: ae ce a rule:step_induction)
+  case (app\<^sub>1 \<Gamma> e x S)
+    have "prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, App e x, S)" by (rule prognosis_App)
+    with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a) (\<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)
+    moreover
+    have "conf_transform (ae, ce, a) (\<Gamma>, App e x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, inc\<cdot>a) (\<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 "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae 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)
+    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
+    have "consistent (ae, ce, pred\<cdot>a) (\<Gamma>, e[y::=x], S)" using app\<^sub>2
+      by (auto elim: below_trans edom_mono  simp add: join_below_iff env_restr_join)
+    moreover
+    have "conf_transform (ae, ce, a) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 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 "prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
+    from below_trans[OF prognosis_called fun_belowD[OF this] ]
+    have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
+  
+    from thunk
+    have "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> 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) f|` edom ce \<sqsubseteq> ae" by simp
+
+    show ?case
+    proof(cases "ce x" rule:two_cases)
+      case none
+      with `x \<in> edom ce` have False by (auto simp add: edom_def)
+      thus ?thesis..
+    next
+      case once
+
+      note `ae x = up\<cdot>u` 
+      moreover
+  
+      from `prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce`
+      have "prognosis ae a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
+        using once by (metis (mono_tags) fun_belowD)
+      hence "x \<notin> ap S" using prognosis_ap[of ae a \<Gamma> "(Var x)" S] by auto
+      
+  
+      from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isLam e`
+      have *: "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+        by (rule prognosis_Var_thunk)
+  
+      from `prognosis ae a (\<Gamma>, Var x, S) x \<sqsubseteq> once`
+      have "(record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))) x = none"
+        by (simp add: two_pred_none)
+      hence **: "prognosis ae u (delete x \<Gamma>, e, Upd x # S) x = none" using fun_belowD[OF *, where x = x] by auto
+
+      have eq: "prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S) = prognosis ae u (delete x \<Gamma>, e, Upd x # S)"
+        by (rule prognosis_env_cong) simp
+
+      have [simp]: "restr_stack (edom ce - {x}) S = restr_stack (edom ce) S" 
+        using `x \<notin> upds S` by (auto intro: restr_stack_cong)
+    
+      have "prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
+        unfolding eq
+        using ** below_trans[OF below_trans[OF * Cfun.monofun_cfun_arg[OF `prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce`]] record_call_below_arg]
+        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) f|\` edom ce \<sqsubseteq> ae`
+      have "(ABinds (delete x \<Gamma>)\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u) 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) f|` edom (env_delete x ce) \<sqsubseteq> env_delete x ae"
+        by (auto simp add: Diff_eq Int_commute env_delete_restr)
+
+      moreover
+  
+      have "const_on ae (ap S \<inter> edom ce) (up\<cdot>0)" using thunk by auto
+      hence "const_on (env_delete x ae) (ap S \<inter> edom ce) (up\<cdot>0)" using `x \<notin>  ap S`
+        by (fastforce simp add: env_delete_def)
+      moreover
+  
+      have "const_on ae (upds S \<inter> edom ce) (up\<cdot>0)" using thunk by auto
+      hence "const_on (env_delete x ae) (upds S \<inter> (edom (env_delete x ce))) (up\<cdot>0)" by fastforce
+      ultimately
+
+      have "consistent (env_delete x ae, env_delete x ce, u) (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])
+      moreover
+      
+      {
+      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))"
+        by (simp add: map_of_map_transform)
+      hence "conf_transform (ae, ce, a) (\<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 # 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), 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, restr_stack (edom ce) S)"
+        by (intro normal_trans Aeta_expand_correct `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`)
+      also(rtranclp_trans)
+      have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u) (delete x \<Gamma>, e, Upd x # S)" 
+        by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist)
+      finally(back_subst)
+      have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (env_delete x ae, env_delete x ce, u) (delete x \<Gamma>, e, Upd x # S)".
+      }
+      ultimately
+      show ?thesis by (blast del: consistentI consistentE)
+  
+    next
+      case many
+  
+      from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isLam e`
+      have "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+        by (rule prognosis_Var_thunk)
+      also note record_call_below_arg
+      finally
+      have *: "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)" by this simp_all
+  
+      have "ae x = up\<cdot>0" using thunk many `x \<in> thunks \<Gamma>` by (auto)
+      hence "u = 0" using `ae x = up\<cdot>u` by simp
+  
+      
+      have "prognosis ae 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) f|\` edom ce \<sqsubseteq> ae`
+      ultimately
+      have "consistent (ae, ce, 0) (delete x \<Gamma>, e, Upd x # S)" using thunk `ae x = up\<cdot>u` `u = 0`  by auto
+      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)"
+        by (simp add: map_of_map_transform)
+      with `\<not> isLam e`
+      have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 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 ?thesis by (blast del: consistentI consistentE)
+    qed
+  next
+  case (lamvar \<Gamma> x e S)
+    from lamvar have "prognosis ae 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)
+
+    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 u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae u (\<Gamma>, e, S)"
+      using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
+    also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+       using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isLam e`  by (rule prognosis_Var_lam)
+    also have "\<dots> \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
+    finally have *: "prognosis ae u ((x, e) # delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)" by this simp_all
+  
+    have "consistent (ae, ce, u) ((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 *])
+    moreover
+  
+    have "Astack (restr_stack (edom ce) S) \<sqsubseteq> u" using lamvar below_trans[OF _ `a \<sqsubseteq> u`] by auto
+  
+    {
+    from `isLam e`
+    have "isLam (transform u e)" by simp
+    hence "isLam (Aeta_expand u (transform u e))" by (rule isLam_Aeta_expand)
+    moreover
+    from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isLam (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))"
+      by (simp add: map_of_map_transform)
+    ultimately
+    have "conf_transform (ae, ce, a) (\<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), 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), restr_stack (edom ce) S)"
+      using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isLam (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) ((x, e) # delete x \<Gamma>, e, S)"
+      by simp (rule Aeta_expand_correct[OF `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`])
+    finally(rtranclp_trans)
+    have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* conf_transform (ae, ce, u) ((x, e) # delete x \<Gamma>, e, S)".
+    }
+    ultimately show ?case by (blast intro: normal_trans del: consistentI consistentE)
+  next
+  case (var\<^sub>2 \<Gamma> x e S)
+    show ?case
+    proof(cases "x \<in> edom ce")
+      case True[simp]
+      hence "ce x \<noteq> \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
+      hence "ae x = up\<cdot>a" 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 `isLam e` `x \<notin> domA \<Gamma>`
+      have *: "prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
+
+      have "consistent (ae, ce, 0) ((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 *])
+      moreover
+      have "conf_transform (ae, ce, a) (\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0) ((x, e) # \<Gamma>, e, S)"
+        using `ae x = up\<cdot>a` `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
+      case False[simp]
+      hence "ce x = \<bottom>" using var\<^sub>2 by (auto simp add: edom_def)
+
+      from False have "x \<notin> edom ae" using var\<^sub>2 by auto
+      hence [simp]: "ae x = \<bottom>" by (auto simp add: edom_def)
+
+      
+      have "prognosis ae a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae a ((x, e) # \<Gamma>, e, Upd x # S)" by (rule prognosis_upd)
+      also
+       
+      from `ae x = \<bottom>`
+      have "prognosis ae a ((x, e) # \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
+        by (rule prognosis_not_called)
+      also have  "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
+      finally
+      have *: "prognosis ae a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae a (\<Gamma>, e, Upd x # S)" by this simp
+
+      have "consistent (ae, ce, a) ((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 *])
+      moreover
+      have "conf_transform (ae, ce, a) (\<Gamma>, e, Upd x # S) = conf_transform (ae, ce, a) ((x, e) # \<Gamma>, e, S)"
+        by(simp add: map_transform_restrA[symmetric])
+      ultimately show ?thesis by (auto del: consistentI consistentE)
+    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"
+      by (auto intro: restr_stack_cong dest!: *)
+  
+    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 "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 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)
+
+  
+    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
+    { fix x e'
+      assume "x \<in> thunks \<Gamma>"
+      hence "x \<notin> edom ?ce" using fresh_distinct[OF let\<^sub>1(1)]
+        by (auto simp add: edom_cHeap dest: set_mp[OF edom_Aheap]  set_mp[OF thunks_domA])
+      hence [simp]: "?ce x = \<bottom>" unfolding edomIff by auto
+    
+      assume "many \<sqsubseteq> (?ce \<squnion> ce) x"
+      with let\<^sub>1 `x \<in> thunks \<Gamma>`
+      have "(?ae \<squnion> ae) x = up \<cdot>0" by auto
+    }
+    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 "x \<notin> edom ce" using let\<^sub>1 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 "const_on ae (ap S \<inter> edom ce) (up\<cdot>0)" using let\<^sub>1 by auto  
+    hence "const_on (?ae \<squnion> ae) (ap S \<inter> edom ce) (up\<cdot>0)" by fastforce
+    hence "const_on (?ae \<squnion> ae) (ap S \<inter> edom (?ce \<squnion> ce)) (up\<cdot>0)" by (simp add: Int_Un_distrib)
+    moreover
+    have "const_on ae (upds (restr_stack (edom ce) S)) (up\<cdot>0)" using let\<^sub>1 by auto
+    hence "const_on (?ae \<squnion> ae) (upds (restr_stack (edom ce) S)) (up\<cdot>0)"  by fastforce
+    hence "const_on (?ae \<squnion> ae) (upds (restr_stack (edom (?ce \<squnion> ce)) S)) (up\<cdot>0)" 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) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> prognosis ae a (\<Gamma>, Let \<Delta> e, S)" by (rule prognosis_Let)
+    also have "prognosis ae a (\<Gamma>, Let \<Delta> e, S) \<sqsubseteq> ce" using let\<^sub>1 by auto
+    finally have "prognosis (?ae \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> ce" by this simp
+    }
+    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)
+    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) 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])
+    ultimately
+    have "(ABinds (\<Delta> @ \<Gamma>) \<cdot> (Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a) 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)
+    }
+    ultimately
+    have "consistent (?ae \<squnion> ae, ?ce \<squnion> ce, a) (\<Delta> @ \<Gamma>, e, S) "
+      by auto
+    }
+    moreover
+    {
+      have "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ae" "\<And> x. x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> edom ?ce"
+        using fresh_distinct[OF let\<^sub>1(1)]
+        by (auto simp add: edom_cHeap dest!: set_mp[OF edom_Aheap])
+      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>))"
+         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
+      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 intro!: map_transform_cong restrictA_cong simp add: edomIff)
+      ultimately
+  
+      have "conf_transform (ae, ce, a) (\<Gamma>, Let \<Delta> e, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (?ae \<squnion> ae, ?ce \<squnion> ce, a) (\<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])
+    }
+    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' ce' a' where "consistent (ae', ce', a') c'" and *: "conf_transform (ae, ce, a) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae', ce', a') c'" by blast
+      from trans(4)[OF this(1)]
+      obtain ae'' ce'' a'' where "consistent (ae'', ce'', a'') c''" and **: "conf_transform (ae', ce', a') c' \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae'', ce'', a'') c''" by blast
+      from this(1) rtranclp_trans[OF * **]
+      show ?case by blast
+  qed
+
+end
+
+end
index aecaa72..a825548 100644 (file)
@@ -133,8 +133,10 @@ qed auto
 
 nominal_termination (eqvt) by lexicographic_order
 
-
-interpretation CoCallArityAnalysis cCCexp.
+locale CoCallAnalysisImpl
+begin
+sublocale CoCallArityAnalysis cCCexp.
+sublocale ArityAnalysis Aexp.
 
 lemma cCCexp_eq[simp]:
   "cCCexp (GVar b x)\<cdot>n =   (esing x \<cdot> (up \<cdot> n),                                   \<bottom>)"
@@ -172,6 +174,77 @@ lemma cc_restr_CCexp[simp]:
   "cc_restr (fv e) (CCexp e\<cdot>a) = CCexp e\<cdot>a"
 by (rule cc_restr_noop[OF ccField_CCexp])
 
+lemma ccField_fup_CCexp:
+  "ccField (fup\<cdot>(CCexp e)\<cdot>n) \<subseteq> fv e"
+by (cases n) (auto dest: set_mp[OF ccField_CCexp])
+
+lemma cc_restr_fup_ccExp_useless[simp]: "cc_restr (fv e) (fup\<cdot>(CCexp e)\<cdot>n) = fup\<cdot>(CCexp e)\<cdot>n"
+  by (rule cc_restr_noop[OF ccField_fup_CCexp])
+
+
+
+lemma Aexp_edom': "edom (Aexp e\<cdot>a) \<subseteq> fv e"
+  by (induction e arbitrary: a rule: exp_induct_rec)(auto)
+
+sublocale EdomArityAnalysis Aexp by default (rule Aexp_edom')
+
+
+
+definition Aheap where
+  "Aheap \<Gamma> e = (\<Lambda> a. if nonrec \<Gamma> then (split Aheap_nonrec (hd \<Gamma>))\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a) else  (Afix \<Gamma> \<cdot> (Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` domA \<Gamma>)"
+
+lemma Aheap_simp1[simp]:
+  "\<not> nonrec \<Gamma> \<Longrightarrow> Aheap \<Gamma> e \<cdot>a = (Afix \<Gamma> \<cdot> (Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` domA \<Gamma>"
+  unfolding Aheap_def by simp
+
+lemma Aheap_simp2[simp]:
+  "atom x \<sharp> e' \<Longrightarrow> Aheap [(x,e')] e \<cdot>a = Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a)"
+  unfolding Aheap_def by (simp add: nonrec_def)
+
+lemma Aheap_eqvt'[eqvt]:
+  "\<pi> \<bullet> (Aheap \<Gamma> e) = Aheap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
+  apply (rule cfun_eqvtI)
+  apply (cases nonrec \<pi> rule: eqvt_cases[where x = \<Gamma>])
+  apply simp
+  apply (erule nonrecE)
+  apply simp
+  apply (perm_simp, rule)
+  apply simp
+  apply (perm_simp, rule)
+  done
+
+sublocale ArityAnalysisHeap Aheap.
+
+sublocale ArityAnalysisHeapEqvt Aheap
+proof
+  fix \<pi> show "\<pi> \<bullet> Aheap = Aheap"
+    by perm_simp rule
+qed
+
+lemma Aexp_lam_simp[simp]: "Aexp (Lam [x]. e) \<cdot> n = env_delete x (Aexp e \<cdot> (pred \<cdot> n))"
+proof-
+  have "Aexp (Lam [x]. e) \<cdot> n = Aexp e\<cdot>(pred\<cdot>n) f|` (fv e - {x})" by simp
+  also have "... = env_delete x (Aexp e\<cdot>(pred\<cdot>n)) f|` (fv e - {x})" by simp
+  also have "\<dots> = env_delete x (Aexp e\<cdot>(pred\<cdot>n))"
+     by (rule env_restr_useless) (auto dest: set_mp[OF Aexp_edom])
+  finally show ?thesis.
+qed
+declare Aexp_simps(2)[simp del]
+
+lemma Aexp_Let_simp1[simp]:
+  "\<not> nonrec \<Gamma> \<Longrightarrow> Aexp (Let \<Gamma> e)\<cdot>n = (Afix \<Gamma>\<cdot>(Aexp e\<cdot>n \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` (- domA \<Gamma>)"
+  unfolding Aexp_simps
+  by (rule env_restr_cong) (auto dest!: set_mp[OF Afix_edom] set_mp[OF Aexp_edom] set_mp[OF thunks_domA])
+
+lemma Aexp_Let_simp2[simp]:
+  "atom x \<sharp> e \<Longrightarrow> Aexp (let x be e in exp)\<cdot>n = env_delete x (fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> (Aexp exp\<cdot>n, CCexp exp\<cdot>n)) \<squnion> Aexp exp\<cdot>n)"
+  unfolding Aexp_simps env_delete_restr
+  by (rule env_restr_cong) (auto dest!: set_mp[OF fup_Aexp_edom]  set_mp[OF Aexp_edom])
+
+declare Aexp_simps(4)[simp del]
+declare Aexp_simps(5)[simp del]
+
+end
 
 
 end
diff --git a/Launchbury/CoCallAnalysisSpec.thy b/Launchbury/CoCallAnalysisSpec.thy
new file mode 100644 (file)
index 0000000..675dcb6
--- /dev/null
@@ -0,0 +1,25 @@
+theory CoCallAnalysisSpec
+imports CoCallAritySig ArityAnalysisSpec
+begin
+
+hide_const Multiset.single
+
+locale CoCallArityEdom = CoCallArity + EdomArityAnalysis
+
+locale CoCallArityCorrect = CoCallArity + CoCallAnalyisHeap + CorrectArityAnalysisLet +
+  assumes ccExp_App: "ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (insert x (fv e)) \<sqsubseteq> ccExp (App e x)\<cdot>a"
+  assumes ccExp_Lam: "cc_restr (fv (Lam [y]. e)) (ccExp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> ccExp (Lam [y]. e)\<cdot>n"
+  assumes ccExp_subst: "x \<notin>  S \<Longrightarrow> y \<notin> S \<Longrightarrow> cc_restr S (ccExp e[y::=x]\<cdot>a) \<sqsubseteq> cc_restr S (ccExp e\<cdot>a)"
+  assumes ccExp_pap: "isLam e \<Longrightarrow> ccExp e\<cdot>0 = ccSquare (fv e)"
+  assumes ccExp_Let: "cc_restr (-domA \<Gamma>) (ccHeap \<Gamma> e\<cdot>a) \<sqsubseteq> ccExp (Let \<Gamma> e)\<cdot>a"
+
+  assumes ccHeap_Exp: "ccExp e\<cdot>a \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
+  assumes ccHeap_Heap: "map_of \<Delta> x = Some e' \<Longrightarrow> (Aheap \<Delta> e\<cdot>a) x= up\<cdot>a' \<Longrightarrow> ccExp e'\<cdot>a' \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
+  assumes ccHeap_Extra_Edges:
+    "map_of \<Delta> x = Some e' \<Longrightarrow> (Aheap \<Delta> e\<cdot>a) x = up\<cdot>a' \<Longrightarrow> ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
+
+  assumes aHeap_thunks_rec: " \<not> nonrec \<Gamma> \<Longrightarrow> x \<in> thunks \<Gamma> \<Longrightarrow> x \<in> edom (Aheap \<Gamma> e\<cdot>a) \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
+  assumes aHeap_thunks_nonrec: "nonrec \<Gamma> \<Longrightarrow> x \<in> thunks \<Gamma> \<Longrightarrow> x \<in> ccManyCalls (ccExp e\<cdot>a) \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
+
+
+end
diff --git a/Launchbury/CoCallAritySig.thy b/Launchbury/CoCallAritySig.thy
new file mode 100644 (file)
index 0000000..21dcaef
--- /dev/null
@@ -0,0 +1,7 @@
+theory CoCallAritySig
+imports ArityAnalysisSig CoCallAnalysisSig
+begin
+
+locale CoCallArity = CoCallAnalysis + ArityAnalysis
+
+end
index 5d680e7..9bd8587 100644 (file)
@@ -2,22 +2,10 @@ theory CoCallImplCorrect
 imports CoCallAnalysisImpl CoCallAnalysisSpec ArityAnalysisFixProps
 begin
 
-lemma ccField_fup_CCexp:
-  "ccField (fup\<cdot>(CCexp e)\<cdot>n) \<subseteq> fv e"
-by (cases n) (auto dest: set_mp[OF ccField_CCexp])
-
-lemma cc_restr_fup_ccExp_useless[simp]: "cc_restr (fv e) (fup\<cdot>(CCexp e)\<cdot>n) = fup\<cdot>(CCexp e)\<cdot>n"
-  by (rule cc_restr_noop[OF ccField_fup_CCexp])
-
-interpretation ArityAnalysis Aexp.
-
-lemma Aexp_edom': "edom (Aexp e\<cdot>a) \<subseteq> fv e"
-  by (induction e arbitrary: a rule: exp_induct_rec)(auto)
-
 locale CoCallImplCorrect
 begin
-sublocale EdomArityAnalysis Aexp by default (rule Aexp_edom')
+sublocale CoCallAnalysisImpl.
+
 lemma ccField_CCfix: "ccField (CCfix \<Gamma>\<cdot>(ae, CCexp  e\<cdot>a)) \<subseteq> fv \<Gamma> \<union> fv e"
   unfolding CCfix_def
   apply simp
@@ -31,30 +19,6 @@ lemma ccField_CCfix: "ccField (CCfix \<Gamma>\<cdot>(ae, CCexp  e\<cdot>a)) \<su
              split: if_splits)
   done
 
-lemma Aexp_lam_simp[simp]: "Aexp (Lam [x]. e) \<cdot> n = env_delete x (Aexp e \<cdot> (pred \<cdot> n))"
-proof-
-  have "Aexp (Lam [x]. e) \<cdot> n = Aexp e\<cdot>(pred\<cdot>n) f|` (fv e - {x})" by simp
-  also have "... = env_delete x (Aexp e\<cdot>(pred\<cdot>n)) f|` (fv e - {x})" by simp
-  also have "\<dots> = env_delete x (Aexp e\<cdot>(pred\<cdot>n))"
-     by (rule env_restr_useless) (auto dest: set_mp[OF Aexp_edom])
-  finally show ?thesis.
-qed
-declare Aexp_simps(2)[simp del]
-
-lemma Aexp_Let_simp1[simp]:
-  "\<not> nonrec \<Gamma> \<Longrightarrow> Aexp (Let \<Gamma> e)\<cdot>n = (Afix \<Gamma>\<cdot>(Aexp e\<cdot>n \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` (- domA \<Gamma>)"
-  unfolding Aexp_simps
-  by (rule env_restr_cong) (auto dest!: set_mp[OF Afix_edom] set_mp[OF Aexp_edom] set_mp[OF thunks_domA])
-
-lemma Aexp_Let_simp2[simp]:
-  "atom x \<sharp> e \<Longrightarrow> Aexp (let x be e in exp)\<cdot>n = env_delete x (fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> (Aexp exp\<cdot>n, CCexp exp\<cdot>n)) \<squnion> Aexp exp\<cdot>n)"
-  unfolding Aexp_simps env_delete_restr
-  by (rule env_restr_cong) (auto dest!: set_mp[OF fup_Aexp_edom]  set_mp[OF Aexp_edom])
-
-declare Aexp_simps(4)[simp del]
-declare Aexp_simps(5)[simp del]
-
-
 lemma CCexp_Let_simp1[simp]:
   "\<not> nonrec \<Gamma> \<Longrightarrow> CCexp (Let \<Gamma> e)\<cdot>n = cc_restr (- domA \<Gamma>) (CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>n \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>n))"
   unfolding CCexp_simps
@@ -224,34 +188,9 @@ qed
 sublocale CorrectArityAnalysis Aexp
   by default (simp_all add:Aexp_restr_subst)
 
-definition Aheap where
-  "Aheap \<Gamma> e = (\<Lambda> a. if nonrec \<Gamma> then (split Aheap_nonrec (hd \<Gamma>))\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a) else  (Afix \<Gamma> \<cdot> (Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` domA \<Gamma>)"
-
-lemma Aheap_simp1[simp]:
-  "\<not> nonrec \<Gamma> \<Longrightarrow> Aheap \<Gamma> e \<cdot>a = (Afix \<Gamma> \<cdot> (Aexp e\<cdot>a \<squnion> (\<lambda>_.up\<cdot>0) f|` thunks \<Gamma>)) f|` domA \<Gamma>"
-  unfolding Aheap_def by simp
-
-lemma Aheap_simp2[simp]:
-  "atom x \<sharp> e' \<Longrightarrow> Aheap [(x,e')] e \<cdot>a = Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a)"
-  unfolding Aheap_def by (simp add: nonrec_def)
-
-lemma Aheap_eqvt'[eqvt]:
-  "\<pi> \<bullet> (Aheap \<Gamma> e) = Aheap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
-  apply (rule cfun_eqvtI)
-  apply (cases nonrec \<pi> rule: eqvt_cases[where x = \<Gamma>])
-  apply simp
-  apply (erule nonrecE)
-  apply simp
-  apply (perm_simp, rule)
-  apply simp
-  apply (perm_simp, rule)
-  done
 
 sublocale CorrectArityAnalysisLet Aexp Aheap
 proof default
-  fix \<pi> show "\<pi> \<bullet> Aheap = Aheap"
-    by perm_simp rule
-next
   fix \<Gamma> e a
   show "edom (Aheap \<Gamma> e\<cdot>a) \<subseteq> domA \<Gamma>"
     by (cases "nonrec \<Gamma>")
diff --git a/Launchbury/CoCallImplFTree.thy b/Launchbury/CoCallImplFTree.thy
new file mode 100644 (file)
index 0000000..b4e5d61
--- /dev/null
@@ -0,0 +1,19 @@
+theory CoCallImplFTree
+imports FTreeAnalysisSpec CoCallAritySig "CoCallGraph-FTree"
+begin
+
+context CoCallArity
+begin
+  definition Fexp :: "exp \<Rightarrow> Arity \<rightarrow> var ftree"
+    where "Fexp e = (\<Lambda> a. ccFTree (edom (Aexp e \<cdot>a)) (ccExp e\<cdot>a))"
+  
+  lemma Fexp_simp: "Fexp e\<cdot>a = ccFTree (edom (Aexp e \<cdot>a)) (ccExp e\<cdot>a)"
+    unfolding Fexp_def by simp
+
+  sublocale FTreeAnalysis Fexp.
+end
+
+
+
+end
+
diff --git a/Launchbury/CoCallImplFTreeCorrect.thy b/Launchbury/CoCallImplFTreeCorrect.thy
new file mode 100644 (file)
index 0000000..79132d0
--- /dev/null
@@ -0,0 +1,552 @@
+theory CoCallImplFTreeCorrect
+imports CoCallImplFTree CoCallAnalysisSpec
+begin
+
+hide_const Multiset.single
+
+lemma valid_lists_many_calls:
+  assumes "\<not> one_call_in_path x p"
+  assumes "p \<in> valid_lists S G"
+  shows "x \<in> ccManyCalls G"
+using assms(2,1)
+proof(induction rule:valid_lists.induct[case_names Nil Cons])
+  case Nil thus ?case by simp
+next
+  case (Cons xs x')
+  show ?case
+  proof(cases "one_call_in_path x xs")
+    case False
+    from Cons.IH[OF this]
+    show ?thesis.
+  next
+    case True
+    with `\<not> one_call_in_path x (x' # xs)`
+    have [simp]: "x' = x" by (auto split: if_splits)
+
+    have "x \<in> set xs"
+    proof(rule ccontr)
+      assume "x \<notin> set xs"
+      hence "no_call_in_path x xs" by (metis no_call_in_path_set_conv)
+      hence "one_call_in_path x (x # xs)" by simp
+      with Cons show False by simp
+    qed
+    with `set xs \<subseteq> ccNeighbors x' G`
+    have "x \<in> ccNeighbors x G" by auto
+    thus ?thesis by simp
+  qed
+qed
+
+context CoCallArityEdom
+begin
+ lemma carrier_Fexp': "carrier (Fexp e\<cdot>a) \<subseteq> fv e"
+    unfolding Fexp_simp carrier_ccFTree
+    by (rule Aexp_edom)
+
+end
+
+
+context CoCallArityCorrect
+begin
+
+
+lemma carrier_AnalBinds_below:
+  "carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom ((ABinds \<Delta>)\<cdot>(Aheap \<Delta> e\<cdot>a))"
+by (auto simp add: Fexp.AnalBinds_lookup Fexp_def split: option.splits 
+         elim!: set_mp[OF edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]]])
+
+sublocale FTreeAnalysisCarrier Fexp
+  apply default unfolding Fexp_simp carrier_ccFTree..
+
+sublocale FTreeAnalysisCorrect Fexp
+proof default
+  fix x e a
+
+  from edom_mono[OF Aexp_App]
+  have *: "{x} \<union> edom (Aexp e\<cdot>(inc\<cdot>a)) \<subseteq> edom (Aexp (App e x)\<cdot>a)" by auto
+
+  have **: "{x} \<union> edom (Aexp e\<cdot>(inc\<cdot>a)) \<subseteq> insert x (fv e)"
+    by (intro subset_trans[OF *] subset_trans[OF Aexp_edom]) auto
+
+  have "many_calls x \<otimes>\<otimes> Fexp e\<cdot>(inc\<cdot>a) = many_calls x \<otimes>\<otimes> ccFTree (edom (Aexp e\<cdot>(inc\<cdot>a))) (ccExp e\<cdot>(inc\<cdot>a))"
+    unfolding Fexp_simp..
+  also have "\<dots> = ccFTree {x} (ccProd {x} {x}) \<otimes>\<otimes> ccFTree (edom (Aexp e\<cdot>(inc\<cdot>a))) (ccExp e\<cdot>(inc\<cdot>a))"
+    unfolding many_calls_ccFTree..
+  also have "\<dots> \<sqsubseteq> ccFTree ({x} \<union> edom (Aexp e\<cdot>(inc\<cdot>a))) (ccProd {x} {x} \<squnion> ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (edom (Aexp e\<cdot>(inc\<cdot>a))))"
+    by (rule interleave_ccFTree)
+  also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp (App e x)\<cdot>a)) (ccProd {x} {x} \<squnion> ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (edom (Aexp e\<cdot>(inc\<cdot>a))))"
+    by (rule ccFTree_mono1[OF *])
+  also have "ccProd {x} {x} \<squnion> ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (edom (Aexp e\<cdot>(inc\<cdot>a))) = ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} ({x} \<union> (edom (Aexp e\<cdot>(inc\<cdot>a))))"
+    by (simp add: ccProd_union2[symmetric] del: ccProd_union2)
+  also have "ccProd {x} ({x} \<union> (edom (Aexp e\<cdot>(inc\<cdot>a)))) \<sqsubseteq> ccProd {x} (insert x (fv e))"
+    by (rule ccProd_mono2[OF **])
+  also have "ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (insert x (fv e)) \<sqsubseteq> ccExp (App e x)\<cdot>a"
+    by (rule ccExp_App)
+  also have "ccFTree (edom (Aexp (App e x)\<cdot>a)) (ccExp (App e x)\<cdot>a) =  Fexp (App e x)\<cdot>a"
+    unfolding Fexp_simp..
+  finally
+  show "many_calls x \<otimes>\<otimes> Fexp e\<cdot>(inc\<cdot>a) \<sqsubseteq> Fexp (App e x)\<cdot>a"
+    by this simp_all
+next
+  fix y e n
+  from edom_mono[OF Aexp_Lam]
+  have *: "edom (Aexp e\<cdot>(pred\<cdot>n)) - {y} \<subseteq> edom (Aexp (Lam [y]. e)\<cdot>n)" by auto
+
+  have "without y (Fexp e\<cdot>(pred\<cdot>n)) = without y (ccFTree (edom (Aexp e\<cdot>(pred\<cdot>n))) (ccExp e\<cdot>(pred\<cdot>n)))"
+    unfolding Fexp_simp..
+  also have "\<dots> = ccFTree (edom (Aexp e\<cdot>(pred\<cdot>n)) - {y}) (ccExp e\<cdot>(pred\<cdot>n))"
+    by (rule  without_ccFTree)
+  also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp (Lam [y]. e)\<cdot>n)) (ccExp e\<cdot>(pred\<cdot>n))"
+    by (rule ccFTree_mono1[OF *])
+  also have "\<dots> = ccFTree (edom (Aexp (Lam [y]. e)\<cdot>n)) (cc_restr ((edom (Aexp (Lam [y]. e)\<cdot>n))) (ccExp e\<cdot>(pred\<cdot>n)))"
+    by (rule ccFTree_cc_restr)
+  also have "(cc_restr ((edom (Aexp (Lam [y]. e)\<cdot>n))) (ccExp e\<cdot>(pred\<cdot>n))) \<sqsubseteq> (cc_restr (fv (Lam [y]. e)) (ccExp e\<cdot>(pred\<cdot>n)))"
+    by (rule cc_restr_mono1[OF Aexp_edom])
+  also have "\<dots> \<sqsubseteq> ccExp (Lam [y]. e)\<cdot>n"
+    by (rule ccExp_Lam)
+  also have "ccFTree (edom (Aexp (Lam [y]. e)\<cdot>n)) (ccExp (Lam [y]. e)\<cdot>n) = Fexp (Lam [y]. e)\<cdot>n"
+    unfolding Fexp_simp..
+  finally
+  show "without y (Fexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> Fexp (Lam [y]. e)\<cdot>n" by this simp_all
+next
+  fix e y x a
+
+  from edom_mono[OF Aexp_subst]
+  have *: "edom (Aexp e[y::=x]\<cdot>a) \<subseteq> insert x (edom (Aexp e\<cdot>a) - {y})" by simp
+
+
+  have "Fexp e[y::=x]\<cdot>a = ccFTree (edom (Aexp e[y::=x]\<cdot>a)) (ccExp e[y::=x]\<cdot>a)"
+    unfolding Fexp_simp..
+  also have "\<dots> \<sqsubseteq> ccFTree (insert x (edom (Aexp e\<cdot>a) - {y})) (ccExp e[y::=x]\<cdot>a)"
+    by (rule ccFTree_mono1[OF *])
+  also have "\<dots> \<sqsubseteq> many_calls x \<otimes>\<otimes> without x (\<dots>)"
+    by (rule paths_many_calls_subset)
+  also have "without x (ccFTree (insert x (edom (Aexp e\<cdot>a) - {y})) (ccExp e[y::=x]\<cdot>a))
+    = ccFTree (edom (Aexp e\<cdot>a) - {y} - {x}) (ccExp e[y::=x]\<cdot>a)"
+    by simp
+  also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp e\<cdot>a) - {y} - {x}) (ccExp e\<cdot>a)"
+    by (rule ccFTree_cong_below[OF ccExp_subst]) auto
+  also have "\<dots> = without y (ccFTree (edom (Aexp e\<cdot>a) - {x}) (ccExp e\<cdot>a))"
+    by simp (metis Diff_insert Diff_insert2)
+  also have "ccFTree (edom (Aexp e\<cdot>a) - {x}) (ccExp e\<cdot>a) \<sqsubseteq> ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)"
+    by (rule ccFTree_mono1) auto
+  also have "\<dots> = Fexp e\<cdot>a"
+    unfolding Fexp_simp..
+  finally
+  show "Fexp e[y::=x]\<cdot>a \<sqsubseteq> many_calls x \<otimes>\<otimes> without y (Fexp e\<cdot>a)"
+    by this simp_all
+next
+  fix v a
+  have "up\<cdot>a \<sqsubseteq> (Aexp (Var v)\<cdot>a) v" by (rule Aexp_Var)
+  hence "v \<in> edom (Aexp (Var v)\<cdot>a)" by (auto simp add: edom_def)
+  hence "[v] \<in> valid_lists (edom (Aexp (Var v)\<cdot>a)) (ccExp (Var v)\<cdot>a)"
+    by auto
+  thus "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
+    unfolding Fexp_simp by (auto intro: single_below)
+next
+  fix e
+  assume "isLam e"
+  hence [simp]: "ccExp e\<cdot>0 = ccSquare (fv e)" by (rule ccExp_pap)
+  thus "repeatable (Fexp e\<cdot>0)"
+    unfolding Fexp_simp by (auto intro: repeatable_ccFTree_ccSquare[OF Aexp_edom])
+qed
+
+definition Fheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> var ftree"
+  where "Fheap \<Gamma> e = (\<Lambda> a. if nonrec \<Gamma> then ccFTree (edom (Aheap \<Gamma> e\<cdot>a)) (ccExp e\<cdot>a) else ftree_restr (edom (Aheap \<Gamma> e\<cdot>a)) anything)"
+
+lemma Fheap_simp: "Fheap \<Gamma> e\<cdot>a = (if nonrec \<Gamma> then ccFTree (edom (Aheap \<Gamma> e\<cdot>a)) (ccExp e\<cdot>a) else ftree_restr (edom (Aheap \<Gamma> e\<cdot>a)) anything)"
+  unfolding Fheap_def by simp
+
+lemma carrier_Fheap':"carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
+    unfolding Fheap_simp carrier_ccFTree by simp
+
+sublocale FTreeAnalysisCardinalityHeap Fexp Aexp Aheap Fheap
+proof default
+  fix \<Gamma> e a
+  show "carrier (Fheap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
+    by (rule carrier_Fheap')
+next
+  fix x \<Gamma> p e a
+  assume "x \<in> thunks \<Gamma>"
+  
+  assume "\<not> one_call_in_path x p"
+  hence "x \<in> set p" by (rule more_than_one_setD)
+  
+  assume "p \<in> paths (Fheap \<Gamma> e\<cdot>a)" with `x \<in> set p`
+  have "x \<in> carrier (Fheap \<Gamma> e\<cdot>a)" by (auto simp add: Union_paths_carrier[symmetric])
+  hence "x \<in> edom (Aheap \<Gamma> e\<cdot>a)"
+    unfolding Fheap_simp by (auto split: if_splits)
+  
+  show "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
+  proof(cases "nonrec \<Gamma>")
+    case False
+    from False `x \<in> thunks \<Gamma>`  `x \<in> edom (Aheap \<Gamma> e\<cdot>a)`
+    show ?thesis  by (rule aHeap_thunks_rec)
+  next
+    case True
+    with `p \<in> paths (Fheap \<Gamma> e\<cdot>a)`
+    have "p \<in> valid_lists (edom (Aheap \<Gamma> e\<cdot>a)) (ccExp e\<cdot>a)" by (simp add: Fheap_simp)
+
+    with `\<not> one_call_in_path x p`
+    have "x \<in> ccManyCalls (ccExp e\<cdot>a)" by (rule valid_lists_many_calls)
+  
+    from True `x \<in> thunks \<Gamma>` this
+    show ?thesis by (rule aHeap_thunks_nonrec)
+  qed
+next
+  fix \<Delta> e a
+
+  show "ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>)  (Fexp e\<cdot>a)) \<sqsubseteq> Fexp (Let \<Delta> e)\<cdot>a"
+  unfolding Fexp_simp
+  proof (rule below_ccFTreeI)
+    have "carrier (ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))
+       = carrier (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))) - domA \<Delta>"
+        by auto
+    also
+    have "carrier (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)))
+         \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
+    proof (rule carrier_substitute_below)
+    show "carrier (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)) \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)" by simp
+    next
+      fix x
+      assume "x \<in> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
+      show "carrier ((ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
+      proof(cases "map_of \<Delta> x")
+        case None thus ?thesis by (simp add: Fexp.AnalBinds_lookup)
+      next
+        case (Some e')
+        hence "carrier ((ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) = carrier (fup\<cdot>(Fexp e')\<cdot>((Aheap \<Delta> e\<cdot>a) x))"
+            by (simp add: Fexp.AnalBinds_lookup)
+        also have "\<dots> \<subseteq> edom (fup\<cdot>(Aexp e')\<cdot>((Aheap \<Delta> e\<cdot>a) x))"
+          by (auto simp add: Fexp_simp)
+        also have "\<dots> = edom (ABind x e'\<cdot>(Aheap \<Delta> e\<cdot>a))" by (simp add: ABind_def)
+        also have "\<dots> \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))" using Some
+          by (rule edom_mono[OF monofun_cfun_fun[OF ABind_below_ABinds]])
+        also have "\<dots> \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)" by simp
+        finally show ?thesis.
+      qed
+    qed
+    also have "\<dots> \<subseteq> edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a)"
+      by (rule edom_mono[OF Aexp_Let])
+    also have "edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a) - domA \<Delta> = edom (Aexp (Let \<Delta> e)\<cdot>a)"
+      by (auto dest: set_mp[OF edom_Aheap] set_mp[OF Aexp_edom])
+    finally
+    show "carrier (ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))
+          \<subseteq> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a)"  by this auto
+  next
+    let ?x = "ccApprox (ftree_restr (- domA \<Delta>) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))"
+  
+    have "?x = cc_restr (- domA \<Delta>) ?x"  by simp
+    also have "\<dots> \<sqsubseteq> cc_restr (- domA \<Delta>) (ccHeap \<Delta> e\<cdot>a)"
+    proof(rule cc_restr_mono2[OF wild_recursion_thunked])
+    (*
+      have "ccLinear (domA \<Delta>) (ccExp e\<cdot>a)" using linear by (rule linear_Exp)
+      thus "ccLinear (domA \<Delta>) (ccApprox (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)))"
+        by auto
+    next
+    *)
+      have "ccExp e\<cdot>a \<sqsubseteq> ccHeap \<Delta> e\<cdot>a" by (rule ccHeap_Exp)
+      thus "ccApprox (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a)) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
+        by (auto intro: below_trans[OF cc_restr_below_arg])
+    next
+      fix x
+      assume "x \<notin> domA \<Delta>"
+      thus "(Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x = empty"
+        by (metis Fexp.AnalBinds_not_there empty_is_bottom)
+    next
+      fix x
+      assume "x \<in> domA \<Delta>"
+      then obtain e' where e': "map_of \<Delta> x = Some e'" by (metis domA_map_of_Some_the)
+      
+      (*
+      thus "ccLinear (domA \<Delta>) (ccApprox ((Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x))"
+      proof(cases "(Aheap \<Delta> e\<cdot>a) x")
+        case bottom thus ?thesis using e' by (simp add: Fexp.AnalBinds_lookup)
+      next
+        case (up a')
+        with linear e'
+        have "ccLinear (domA \<Delta>) (ccExp e'\<cdot>a')" by (rule linear_Heap)
+        thus ?thesis using up e' by (auto simp add: Fexp.AnalBinds_lookup Fexp_simp)
+      qed
+      *)
+      
+      show "ccApprox ((Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
+      proof(cases "(Aheap \<Delta> e\<cdot>a) x")
+        case bottom thus ?thesis using e' by (simp add: Fexp.AnalBinds_lookup)
+      next
+        case (up a')
+        with e'
+        have "ccExp e'\<cdot>a' \<sqsubseteq> ccHeap \<Delta> e\<cdot>a" by (rule ccHeap_Heap)
+        thus ?thesis using up e'
+          by (auto simp add: Fexp.AnalBinds_lookup Fexp_simp  intro: below_trans[OF cc_restr_below_arg])
+      qed
+
+      show "ccProd (ccNeighbors x (ccHeap \<Delta> e\<cdot>a)- {x} \<inter> thunks \<Delta>) (carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x)) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
+      proof(cases "(Aheap \<Delta> e\<cdot>a) x")
+        case bottom thus ?thesis using e' by (simp add: Fexp.AnalBinds_lookup)
+      next
+        case (up a')
+        have subset: "(carrier (fup\<cdot>(Fexp e')\<cdot>((Aheap \<Delta> e\<cdot>a) x))) \<subseteq> fv e'"
+          using up e' by (auto simp add: Fexp.AnalBinds_lookup carrier_Fexp dest!: set_mp[OF Aexp_edom])
+        
+        from e' up
+        have "ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
+          by (rule ccHeap_Extra_Edges)
+        then
+        show ?thesis using e'
+          by (simp add: Fexp.AnalBinds_lookup  Fexp_simp ccProd_comm  below_trans[OF ccProd_mono1[OF subset]])
+      qed
+    qed
+    also have "\<dots> \<sqsubseteq> ccExp (Let \<Delta> e)\<cdot>a"
+      by (rule ccExp_Let)
+    finally
+    show "ccApprox (ftree_restr (- domA \<Delta>) (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (ccFTree (edom (Aexp e\<cdot>a)) (ccExp e\<cdot>a))))
+        \<sqsubseteq> ccExp (Terms.Let \<Delta> e)\<cdot>a" by this simp_all
+
+  qed
+
+  have "carrier (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
+  proof(rule carrier_substitute_below)
+    from edom_mono[OF Aexp_Let[of \<Delta> e a]]
+    show "carrier (Fexp e\<cdot>a) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"  by (simp add: Fexp_def)
+  next
+    fix x
+    assume "x \<in> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
+    hence "x \<in> edom (Aheap \<Delta> e\<cdot>a) \<or> x : (edom (Aexp (Let \<Delta> e)\<cdot>a))" by simp
+    thus "carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
+    proof
+      assume "x \<in> edom (Aheap \<Delta> e\<cdot>a)"
+      
+      have "carrier ((Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<subseteq> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))"
+        by (rule carrier_AnalBinds_below)
+      also have "\<dots> \<subseteq> edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Terms.Let \<Delta> e)\<cdot>a)"
+        using edom_mono[OF Aexp_Let[of \<Delta> e a]] by simp
+      finally show ?thesis by simp
+    next
+      assume "x \<in> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a)"
+      hence "x \<notin> domA \<Delta>" by (auto  dest: set_mp[OF Aexp_edom])
+      hence "(Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x = \<bottom>"
+        by (rule Fexp.AnalBinds_not_there)
+      thus ?thesis by simp
+    qed
+  qed
+  hence "carrier (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> - domA \<Delta>"
+    by (rule order_trans) (auto dest: set_mp[OF Aexp_edom])
+  hence "ftree_restr (domA \<Delta>)            (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
+      = ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (ftree_restr (domA \<Delta>) (substitute (Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)))"
+    by -(rule ftree_restr_noop[symmetric], auto)
+  also
+  have "\<dots> = ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds  \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))"
+    by (simp add: inf.absorb2[OF edom_Aheap ])
+  also
+  (*
+  have "substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<sqsubseteq> singles (calledOnce \<Delta> e a)"
+  proof(rule substitute_below_singlesI)
+    show "Fexp e\<cdot>a \<sqsubseteq> singles (calledOnce \<Delta> e a)"
+      unfolding Fexp_simp
+      using calledOnce_exp
+      by (auto intro!: ccFTree_below_singleI)
+  next
+    fix x
+    show "carrier ((Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x) \<inter> calledOnce \<Delta> e a = {}"
+      using calledOnce_heap[unfolded disjoint_iff_not_equal]
+      by (force simp add: Fexp.AnalBinds_lookup Fexp_simp split: option.split)
+  qed
+  hence "ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
+      \<sqsubseteq> ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (singles (calledOnce \<Delta> e a))"
+    by (rule ftree_restr_mono)
+  *)
+  have "\<dots> \<sqsubseteq> Fheap \<Delta> e \<cdot>a"
+  proof(cases "nonrec \<Delta>")
+    case False
+    have "ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
+      \<sqsubseteq> ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) anything"
+    by (rule ftree_restr_mono) simp
+    also have "\<dots> = Fheap \<Delta> e\<cdot>a"
+      by (simp add:  Fheap_simp False)
+    finally show ?thesis.
+  next
+    case True[simp]
+
+    from True
+    have "ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (substitute (Fexp.AnalBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))
+       = ftree_restr (edom (Aheap \<Delta> e\<cdot>a)) (Fexp e\<cdot>a)"
+      by (rule nonrecE) (rule ftree_rest_substitute, auto simp add: carrier_Fexp fv_def fresh_def dest!: set_mp[OF edom_Aheap] set_mp[OF Aexp_edom])
+    also have "\<dots> = ccFTree (edom (Aexp e\<cdot>a) \<inter> edom (Aheap \<Delta> e\<cdot>a)) (ccExp e\<cdot>a)"
+      by (simp add: Fexp_simp)
+    also have "\<dots> \<sqsubseteq> ccFTree (edom (Aexp e\<cdot>a) \<inter> domA \<Delta>) (ccExp e\<cdot>a)"
+      by (rule ccFTree_mono1[OF Int_mono[OF order_refl edom_Aheap]])
+    also have "\<dots> \<sqsubseteq> ccFTree (edom (Aheap \<Delta> e\<cdot>a)) (ccExp e\<cdot>a)"
+      by (rule ccFTree_mono1[OF edom_mono[OF Aheap_nonrec[OF True], simplified]])
+    also have "\<dots> \<sqsubseteq> Fheap \<Delta> e\<cdot>a"
+      by (simp add: Fheap_simp)
+    finally
+    show ?thesis by this simp_all
+  qed
+  finally
+  show "ftree_restr (domA \<Delta>) (substitute (ExpAnalysis.AnalBinds Fexp \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fheap \<Delta> e\<cdot>a".
+
+qed
+end
+
+(* TODO: Unused stuff from here, mostly about singles. Might be useful later. *)
+
+
+lemma paths_singles: "xs \<in> paths (singles S) \<longleftrightarrow> (\<forall>x \<in> S. one_call_in_path x xs)"
+  by transfer (auto simp add: one_call_in_path_filter_conv)
+
+lemma paths_singles': "xs \<in> paths (singles S) \<longleftrightarrow> (\<forall>x \<in> (set xs \<inter> S). one_call_in_path x xs)"
+  apply transfer
+  apply (auto simp add: one_call_in_path_filter_conv)
+  apply (erule_tac x = x in ballE)
+  apply auto
+  by (metis (poly_guards_query) filter_empty_conv le0 length_0_conv)
+
+lemma both_below_singles1:
+  assumes "t \<sqsubseteq> singles S"
+  assumes "carrier t' \<inter> S = {}"
+  shows "t \<otimes>\<otimes> t' \<sqsubseteq> singles S"
+proof (rule ftree_belowI)
+  fix xs
+  assume "xs \<in> paths (t \<otimes>\<otimes> t')"
+  then obtain ys zs where "ys \<in> paths t" and "zs \<in> paths t'" and "xs \<in> ys \<otimes> zs" by (auto simp add: paths_both)
+  with assms 
+  have "ys \<in> paths (singles S)" and "set zs \<inter> S = {}"
+    by (metis below_ftree.rep_eq contra_subsetD paths.rep_eq, auto simp add: Union_paths_carrier[symmetric])
+  with `xs \<in> ys \<otimes> zs`
+  show "xs \<in> paths (singles S)"
+    by (induction) (auto simp add: paths_singles no_call_in_path_set_conv interleave_set dest: more_than_one_setD split: if_splits)
+qed
+
+
+lemma paths_ftree_restr_singles: "xs \<in> paths (ftree_restr S' (singles S)) \<longleftrightarrow> set xs \<subseteq> S' \<and> (\<forall>x \<in> S. one_call_in_path x xs)"
+proof
+  show "xs \<in> paths (ftree_restr S' (singles S)) \<Longrightarrow>  set xs \<subseteq> S' \<and> (\<forall>x \<in> S. one_call_in_path x xs)"
+    by (auto simp add: filter_paths_conv_free_restr[symmetric] paths_singles)
+next
+  assume *: "set xs \<subseteq> S' \<and> (\<forall>x\<in>S. one_call_in_path x xs)"
+  hence "set xs \<subseteq> S'" by auto
+  hence [simp]: "filter (\<lambda> x'. x' \<in> S') xs = xs" by (auto simp add: filter_id_conv)
+  
+  from *
+  have "xs \<in> paths (singles S)"
+     by (auto simp add: paths_singles')
+  hence "filter (\<lambda> x'. x' \<in> S') xs \<in> filter (\<lambda>x'. x' \<in> S') ` paths (singles S)"
+    by (rule imageI)
+  thus "xs \<in> paths (ftree_restr S' (singles S))"
+    by (auto simp add: filter_paths_conv_free_restr[symmetric] )
+qed
+
+
+
+(* TODO: unused *)
+lemma substitute_not_carrier:
+  assumes "x \<notin> carrier t"
+  assumes "\<And> x'. x \<notin> carrier (f x')"
+  shows "x \<notin>  carrier (substitute f T t)"
+proof-
+  have "ftree_restr ({x}) (substitute f T t) = ftree_restr ({x}) t"
+  proof(rule ftree_rest_substitute)
+    fix x'
+    from `x \<notin> carrier (f x')`
+    show "carrier (f x') \<inter> {x} = {}" by auto
+  qed
+  hence "x \<notin> carrier (ftree_restr ({x}) (substitute f T t)) \<longleftrightarrow> x \<notin> carrier (ftree_restr ({x}) t)" by metis
+  with assms(1)
+  show ?thesis by simp
+qed
+
+(* TODO: unused *)
+lemma substitute_below_singlesI:
+  assumes "t \<sqsubseteq> singles S"
+  assumes "\<And> x. carrier (f x) \<inter> S = {}"
+  shows "substitute f T t \<sqsubseteq> singles S"
+proof(rule ftree_belowI)
+  fix xs
+  assume "xs \<in> paths (substitute f T t)"
+  thus "xs \<in> paths (singles S)"
+  using assms
+  proof(induction f T t xs arbitrary: S rule: substitute_induct)
+    case Nil
+    thus ?case by simp
+  next
+    case (Cons f T t x xs)
+
+    from `x#xs \<in> _`
+    have xs: "xs \<in> paths (substitute (f_nxt f T x) T (nxt t x \<otimes>\<otimes> f x))" by auto
+    moreover
+
+    from `t \<sqsubseteq> singles S`
+    have "nxt t x \<sqsubseteq> singles S" 
+      by (metis "FTree-HOLCF.nxt_mono" below_trans nxt_singles_below_singles)
+    from this `carrier (f x) \<inter> S = {}`
+    have "nxt t x \<otimes>\<otimes> f x \<sqsubseteq> singles S"
+      by (rule both_below_singles1)
+    moreover
+    { fix x'
+      from  `carrier (f x') \<inter> S = {}`
+      have "carrier (f_nxt f T x x') \<inter> S = {}"
+        by (auto simp add: f_nxt_def)
+    }
+    ultimately
+    have IH: "xs \<in> paths (singles S)"
+      by (rule Cons.IH) 
+  
+  show ?case
+    proof(cases "x \<in> S")
+      case True
+      with `carrier (f x) \<inter> S = {}`
+      have "x \<notin> carrier (f x)" by auto
+      moreover
+      from `t \<sqsubseteq> singles S`
+      have "nxt t x \<sqsubseteq> nxt (singles S) x" by (rule nxt_mono)
+      hence "carrier (nxt t x) \<subseteq> carrier (nxt (singles S) x)" by (rule carrier_mono)
+      from set_mp[OF this] True
+      have "x \<notin> carrier (nxt t x)" by auto
+      ultimately
+      have "x \<notin> carrier (nxt t x \<otimes>\<otimes> f x)" by simp
+      hence "x \<notin> carrier (substitute (f_nxt f T x) T (nxt t x \<otimes>\<otimes> f x))"
+      proof(rule substitute_not_carrier)
+        fix x'  
+        from `carrier (f x') \<inter> S = {}` `x \<in> S`
+        show "x \<notin> carrier (f_nxt f T x x')" by (auto simp add: f_nxt_def)
+      qed
+      with xs
+      have "x \<notin> set xs" by (auto simp add: Union_paths_carrier[symmetric])
+      with IH
+      have "xs \<in> paths (without x (singles S))" by (rule paths_withoutI)
+      thus ?thesis using True by (simp add: Cons_path)
+    next
+      case False
+      with IH
+      show ?thesis by (simp add: Cons_path)
+    qed
+  qed
+qed
+
+(* TODO: Unused. Remove? *)
+lemma multi_calls_ccFTree:
+  assumes "xs \<in> paths (ccFTree S G)"
+  assumes "\<not> one_call_in_path x xs"
+  shows "x \<in> S" and "x \<in> ccManyCalls G"
+proof-
+  from assms(1) have "xs \<in> valid_lists S G" by simp 
+
+  have "x \<in> set xs" by (metis assms(2) filter_True one_call_in_path_filter)
+  with `xs \<in> valid_lists S G`
+  show "x \<in> S" by (metis  subsetCE valid_lists_subset)
+
+  show "x \<in> ccManyCalls G"
+  proof(rule ccontr)
+    assume "x \<notin> ccManyCalls G"
+    with `xs \<in> valid_lists S G` 
+    have "one_call_in_path x xs"
+    by (induction rule: valid_lists.induct) (auto simp add: no_call_in_path_set_conv)
+    with assms(2)
+    show False..
+  qed
+qed
+
+
+
+end
+
diff --git a/Launchbury/FTreeCardinality.thy b/Launchbury/FTreeCardinality.thy
deleted file mode 100644 (file)
index 9b113db..0000000
+++ /dev/null
@@ -1,375 +0,0 @@
-theory FTreeCardinality
-imports FTreeAnalysisSpec CardinalityAnalysis CallFutureCardinality
-begin
-
-hide_const Multiset.single
-
-context FTreeAnalysis
-begin
-
-fun unstack :: "stack \<Rightarrow> exp \<Rightarrow> exp" where
-  "unstack [] e = e"
-| "unstack (Upd x # S) e = unstack S e"
-| "unstack (Arg x # S) e = unstack S (App e x)"
-| "unstack (Dummy x # S) e = unstack S e"
-
-fun Fstack :: "stack \<Rightarrow> var ftree"
-  where "Fstack [] = \<bottom>"
-  | "Fstack (Upd x # S) = Fstack S"
-  | "Fstack (Arg x # S) = many_calls x \<otimes>\<otimes> Fstack S"
-  | "Fstack (Dummy x # S) = Fstack S"
-
-lemma carrier_Fstack[simp]: "carrier (Fstack S) = ap S"
-  by (induction S rule: Fstack.induct) (auto simp add: empty_is_bottom[symmetric])
-
-fun prognosis :: "AEnv \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> var \<Rightarrow> two"
-   where "prognosis ae a (\<Gamma>, e, S) = pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)))"
-end
-
-
-lemma pathsCard_paths_nxt:  "pathsCard (paths (nxt f x)) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths f))"
-  apply transfer
-  apply (rule pathsCard_below)
-  apply auto
-  apply (erule below_trans[OF _ monofun_cfun_arg[OF paths_Card_above], rotated]) back
-  apply (auto intro: fun_belowI simp add: record_call_simp two_pred_two_add_once)
-  done
-
-lemma pathsCards_none: "pathsCard (paths t) x = none \<Longrightarrow> x \<notin> carrier t"
-  by transfer (auto dest: pathCards_noneD)
-
-lemma const_on_edom_disj: "const_on f S empty \<longleftrightarrow> edom f \<inter> S = {}"
-  by (auto simp add: empty_is_bottom edom_def)
-
-context FTreeAnalysisCarrier
-begin
-  lemma carrier_FBinds: "carrier ((FBinds \<Gamma>\<cdot>ae) x) \<subseteq> fv \<Gamma>"
-  apply (simp add: Fexp.AnalBinds_lookup)
-  apply (auto split: option.split simp add: empty_is_bottom[symmetric] )
-  apply (case_tac "ae x")
-  apply (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: set_mp[OF Aexp_edom])
-  by (metis (poly_guards_query) contra_subsetD domA_from_set map_of_fv_subset map_of_is_SomeD option.sel)
-end
-
-
-
-
-context FTreeAnalysisCorrect
-begin
-
-  sublocale CardinalityPrognosisCorrect prognosis
-  proof
-    fix \<Gamma> :: heap and ae ae' :: AEnv and u e S
-    assume "ae f|` domA \<Gamma> = ae' f|` domA \<Gamma>"
-    from Fexp.AnalBinds_cong[OF this]
-    show "prognosis ae u (\<Gamma>, e, S) = prognosis ae' u (\<Gamma>, e, S)" by simp
-  next
-    fix ae a \<Gamma> e S
-    show "const_on (prognosis ae a (\<Gamma>, e, S)) (ap S) many"
-    proof
-      fix x
-      assume "x \<in> ap S"
-      hence "[x,x] \<in> paths (Fstack S)"
-        by (induction S rule: Fstack.induct)
-           (auto 4 4 intro: set_mp[OF both_contains_arg1] set_mp[OF both_contains_arg2] paths_Cons_nxt)
-      hence "[x,x] \<in> paths (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)"
-        by (rule set_mp[OF both_contains_arg2])
-      hence "[x,x] \<in> paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))" 
-        by (rule set_mp[OF substitute_contains_arg])
-      hence "pathCard [x,x] x \<sqsubseteq> pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))) x"
-        by (metis fun_belowD paths_Card_above)
-      also have "pathCard [x,x] x = many"  by (auto simp add: pathCard_def)
-      finally
-      show "prognosis ae a (\<Gamma>, e, S) x = many"
-        by (auto intro: below_antisym)
-    qed
-  next
-    fix ae a \<Gamma> e x S
-    have "Fexp e\<cdot>(inc\<cdot>a)  \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack S = many_calls x  \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<otimes>\<otimes> Fstack S"
-      by (metis both_assoc both_comm)
-    thus "prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, App e x, S)"
-      by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1' Fexp_App)
-  next
-    fix ae a \<Gamma> e y x S
-    have "Fexp e[y::=x]\<cdot>(pred\<cdot>a) \<sqsubseteq> many_calls x  \<otimes>\<otimes> Fexp (Lam [y]. e)\<cdot>a"
-      by (rule below_trans[OF Fexp_subst both_mono2'[OF Fexp_Lam]])
-    moreover have "Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack S = many_calls x  \<otimes>\<otimes> Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> Fstack S"
-      by (metis both_assoc both_comm)
-    ultimately  
-    show "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae a (\<Gamma>, Lam [y]. e, Arg x # S)"
-      by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1')
-  next
-    fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
-    assume "map_of \<Gamma> x = Some e"
-    assume "ae x = up\<cdot>u"
-
-    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S))) = pathsCard (paths (nxt (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) x))"
-      by simp
-    also
-    have "\<dots> \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))))"
-      by (rule pathsCard_paths_nxt)
-    also
-    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
-      by (metis both_comm)
-    also
-    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
-      using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` by (simp add: Fexp.AnalBinds_lookup)
-    also
-    assume "isLam e"
-    hence "x \<notin> thunks \<Gamma>" using `map_of \<Gamma> x = Some e` by (metis thunksE)
-    hence "FBinds \<Gamma>\<cdot>ae = f_nxt (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) x" by (auto simp add: f_nxt_def)
-    hence "and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack S))"
-      by (simp add: substitute_and_then)
-    also
-    have "and_then x (Fstack S) \<sqsubseteq> FTree.single x \<otimes>\<otimes> Fstack S" by (rule and_then_both_single')
-    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF this]]]
-    also
-    have "FTree.single x \<sqsubseteq> Fexp (Var x)\<cdot>a" by (rule Fexp_Var)
-    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF both_mono1'[OF this]]]]
-    finally
-    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a  \<otimes>\<otimes> Fstack S))))" 
-      by this simp_all
-    thus "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> record_call x\<cdot>(prognosis ae a (\<Gamma>, Var x, S))" by simp
-  next
-    fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
-    assume "map_of \<Gamma> x = Some e"
-    assume "ae x = up\<cdot>u"
-    assume "\<not> isLam e"
-    hence "x \<in> thunks \<Gamma>" using `map_of \<Gamma> x = Some e` by (metis thunksI)
-    hence [simp]: "f_nxt (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) x = FBinds (delete x \<Gamma>)\<cdot>ae" 
-      by (auto simp add: f_nxt_def Fexp.AnalBinds_delete_to_fun_upd empty_is_bottom)
-
-    have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S)))
-       =  pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S)))"
-       by (rule arg_cong[OF substitute_cong_T]) (auto simp add: empty_is_bottom)
-    also have "\<dots>  = pathsCard (paths (nxt (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) x))"
-      by simp
-    also
-    have "\<dots> \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))))"
-      by (rule pathsCard_paths_nxt)
-    also
-    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
-      by (metis both_comm)
-    also
-    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
-      using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` by (simp add: Fexp.AnalBinds_lookup)
-    also
-    have "and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack S))"
-      by (simp add: substitute_and_then)
-    also
-    have "and_then x (Fstack S) \<sqsubseteq> FTree.single x \<otimes>\<otimes> Fstack S" by (rule and_then_both_single')
-    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF this]]]
-    also
-    have "FTree.single x \<sqsubseteq> Fexp (Var x)\<cdot>a" by (rule Fexp_Var)
-    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF both_mono1'[OF this]]]]
-    finally
-    have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))
-       \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a  \<otimes>\<otimes> Fstack S))))" 
-      by this simp_all
-    thus "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x\<cdot>(prognosis ae a (\<Gamma>, Var x, S))" by simp
-  next
-    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and  x :: var and  S
-    assume "isLam e"
-    hence "repeatable (Fexp e\<cdot>0)" by (rule Fun_repeatable)
-
-    assume [simp]: "x \<notin> domA \<Gamma>"
-
-    have [simp]: "thunks ((x, e) # \<Gamma>) = thunks \<Gamma>" 
-      using `isLam e`
-      by (auto simp add: thunks_Cons dest: set_mp[OF thunks_domA])
-
-    have "fup\<cdot>(Fexp e)\<cdot>(ae x) \<sqsubseteq> Fexp e\<cdot>0" by (metis fup2 monofun_cfun_arg up_zero_top)
-    hence "substitute ((FBinds \<Gamma>\<cdot>ae)(x := fup\<cdot>(Fexp e)\<cdot>(ae x))) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S) \<sqsubseteq> substitute ((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S)"
-      by (intro substitute_mono1' fun_upd_mono below_refl)
-    also have "\<dots> = substitute (((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0))(x := empty)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S)"
-      using `repeatable (Fexp e\<cdot>0)` by (rule substitute_remove_anyways, simp)
-    also have "((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0))(x := empty) = FBinds \<Gamma>\<cdot>ae"
-      by (simp add: fun_upd_idem Fexp.AnalBinds_not_there empty_is_bottom)
-    finally
-    show "prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)"
-      by (simp, intro pathsCard_mono' paths_mono)
-  next
-    fix \<Gamma> \<Delta> :: heap and e :: exp and ae :: AEnv and u S
-    assume "map_of \<Gamma> = map_of \<Delta>"
-    hence "FBinds \<Gamma> = FBinds \<Delta>" and "thunks \<Gamma> = thunks \<Delta>" by (auto intro!: cfun_eqI  thunks_cong simp add: Fexp.AnalBinds_lookup)
-    thus "prognosis ae u (\<Gamma>, e, S) = prognosis ae u (\<Delta>, e, S)"  by simp
-  next
-    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and u S x
-
-    show "prognosis ae u (delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, S)"
-      by (simp add: substitute_T_delete empty_is_bottom)
-         (intro pathsCard_mono' paths_mono substitute_mono1' Fexp.AnalBinds_delete_below)
-  next
-    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and u S x
-    show "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, Upd x # S)" by simp
-  next
-  fix \<Gamma> :: heap and e :: exp and ae :: AEnv and a S x
-  assume "ae x = \<bottom>"
-
-  hence "FBinds (delete x \<Gamma>)\<cdot>ae = FBinds \<Gamma>\<cdot>ae" by (rule Fexp.AnalBinds_delete_bot)
-  moreover
-  hence "((FBinds \<Gamma>\<cdot>ae) x) = \<bottom>" by (metis Fexp.AnalBinds_delete_lookup)
-  ultimately
-  show "prognosis ae a (\<Gamma>, e, S) \<sqsubseteq> prognosis ae a (delete x \<Gamma>, e, S)"
-    by (simp add: substitute_T_delete empty_is_bottom)
-  next
-    fix ae a \<Gamma> x S
-    have "once \<sqsubseteq> (pathCard [x]) x" by (simp add: two_add_simp)
-    also have "pathCard [x] \<sqsubseteq> pathsCard ({[],[x]})"
-      by (rule paths_Card_above) simp
-    also have "\<dots> = pathsCard (paths (single x))" by simp
-    also have "single x \<sqsubseteq> (Fexp (Var x)\<cdot>a)" by (rule Fexp_Var)
-    also have "\<dots> \<sqsubseteq> Fexp (Var x)\<cdot>a \<otimes>\<otimes> Fstack S" by (rule both_above_arg1)
-    also have "\<dots> \<sqsubseteq> substitute  (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a \<otimes>\<otimes> Fstack S)" by (rule substitute_above_arg)
-    also have "pathsCard (paths \<dots>) x =  prognosis ae a (\<Gamma>, Var x, S) x" by simp
-    finally
-    show "once \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S) x"
-      by this (rule cont2cont_fun, intro cont2cont)+
-  qed
-end
-
-context FTreeAnalysisCardinalityHeap
-begin
-
-  definition cHeap where
-    "cHeap \<Gamma> e = (\<Lambda> a. pathsCard (paths (Fheap \<Gamma> e\<cdot>a)))"
-
-  lemma cHeap_simp: "(cHeap \<Gamma> e)\<cdot>a = pathsCard (paths (Fheap \<Gamma> e\<cdot>a))"
-    unfolding cHeap_def  by (rule beta_cfun) (intro cont2cont)
-  
-  (*
-  lemma cHeap_eqvt: "\<pi> \<bullet> (cHeap \<Gamma> e) = cHeap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
-    unfolding cHeap_def
-    apply perm_simp
-    apply (simp add: Fheap_eqvt)
-    apply (rule Abs_cfun_eqvt)
-    apply (intro cont2cont)
-    done
-  *)
-
-  sublocale CardinalityHeap Aexp Aheap cHeap
-  proof
-  (*
-    note cHeap_eqvt[eqvt]
-    fix \<pi> show "\<pi> \<bullet> cHeap = cHeap" by perm_simp rule
-  next
-  *)
-    fix x \<Gamma> e a
-    assume "x \<in> thunks \<Gamma>"
-    moreover
-    assume "many \<sqsubseteq> (cHeap \<Gamma> e\<cdot>a) x"
-    hence "many \<sqsubseteq> pathsCard (paths (Fheap \<Gamma> e \<cdot>a)) x" unfolding cHeap_def by simp
-    hence "\<exists>p\<in> (paths (Fheap \<Gamma> e\<cdot>a)). \<not> (one_call_in_path x p)" unfolding pathsCard_def
-      by (auto split: if_splits)
-    ultimately
-    show "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
-      by (metis Fheap_thunk)
-  next
-    fix \<Gamma> e a
-    show "edom (cHeap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
-    by (simp add: cHeap_def Union_paths_carrier carrier_Fheap)
-  qed
-
-  sublocale CardinalityPrognosisEdom prognosis Aexp Aheap
-  proof
-    fix ae a \<Gamma> e S
-    show "edom (prognosis ae a (\<Gamma>, e, S)) \<subseteq> fv \<Gamma> \<union> fv e \<union> fv S"
-      apply (simp add: Union_paths_carrier)
-      apply (rule carrier_substitute_below)
-      apply (auto simp add: carrier_Fexp dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF carrier_FBinds])
-      done
-  qed
-  
-  sublocale CardinalityPrognosisCorrectLet prognosis Aexp Aheap cHeap
-  proof
-    fix \<Delta> \<Gamma> :: heap and e :: exp and S :: stack and  ae :: AEnv and a :: Arity
-    assume "atom ` domA \<Delta> \<sharp>* \<Gamma>"
-    assume "atom ` domA \<Delta> \<sharp>* S"
-    assume "edom ae \<subseteq> domA \<Gamma> \<union> upds S"
-
-    have "domA \<Delta> \<inter> edom ae = {}"
-      using fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`] fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`] 
-            `edom ae \<subseteq> domA \<Gamma> \<union> upds S` ups_fv_subset[of S]
-      by auto
-
-    have const_on1:  "\<And> x. const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (carrier ((FBinds \<Gamma>\<cdot>ae) x)) empty"
-      unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
-      by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF Fexp.edom_AnalBinds])
-    have const_on2:  "const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (carrier (Fstack S)) empty"
-      unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`]
-      by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF Fexp.edom_AnalBinds] set_mp[OF ap_fv_subset ])
-    have  const_on3: "const_on (FBinds \<Gamma>\<cdot>ae) (- (- domA \<Delta>)) FTree.empty"
-      and const_on4: "const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (domA \<Gamma>) FTree.empty"
-      unfolding const_on_edom_disj using fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
-      by (auto dest!:  set_mp[OF Fexp.edom_AnalBinds])
-
-    have disj1: "\<And> x. carrier ((FBinds \<Gamma>\<cdot>ae) x) \<inter> domA \<Delta> = {}"
-      using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
-      by (auto dest: set_mp[OF carrier_FBinds])
-    hence disj1': "\<And> x. carrier ((FBinds \<Gamma>\<cdot>ae) x) \<subseteq> - domA \<Delta>" by auto
-    have disj2: "\<And> x. carrier (Fstack S) \<inter> domA \<Delta> = {}"
-      using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`] ap_fv_subset[of S] by auto
-    hence disj2': "carrier (Fstack S) \<subseteq> - domA \<Delta>" by auto
-    
-
-    {
-    fix x
-    have "(FBinds (\<Delta> @ \<Gamma>)\<cdot>(ae \<squnion> Aheap \<Delta> e\<cdot>a)) x = (FBinds \<Gamma>\<cdot>ae) x \<otimes>\<otimes> (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x"
-    proof (cases "x \<in> domA \<Delta>")
-      case True
-      have "map_of \<Gamma> x = None" using True fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`] by (metis disjoint_iff_not_equal domA_def map_of_eq_None_iff)
-      moreover
-      have "ae x = \<bottom>" using True `domA \<Delta> \<inter> edom ae = {}` by auto
-      ultimately
-      show ?thesis using True 
-          by (auto simp add: Fexp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
-    next
-      case False
-      have "map_of \<Delta> x = None" using False by (metis domA_def map_of_eq_None_iff)
-      moreover
-      have "(Aheap \<Delta> e\<cdot>a) x = \<bottom>" using False using edom_Aheap by (metis contra_subsetD edomIff)
-      ultimately
-      show ?thesis using False
-         by (auto simp add: Fexp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
-    qed
-    }
-    note FBinds = ext[OF this]
-
-    {
-    have "pathsCard (paths (substitute (FBinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) (thunks (\<Delta> @ \<Gamma>)) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)))
-      = pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks (\<Delta> @ \<Gamma>)) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks (\<Delta> @ \<Gamma>))  (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))))"
-       by (simp add: substitute_substitute[OF const_on1] FBinds)
-    also have "substitute (FBinds \<Gamma>\<cdot>ae) (thunks (\<Delta> @ \<Gamma>)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>)"
-      apply (rule substitute_cong_T)
-      using const_on3
-      by (auto dest: set_mp[OF thunks_domA])
-    also have "substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks (\<Delta> @ \<Gamma>)) = substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>)"
-      apply (rule substitute_cong_T)
-      using const_on4
-      by (auto dest: set_mp[OF thunks_domA])
-    also have "substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S) = substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S" 
-      by (rule substitute_only_empty_both[OF const_on2])
-    also note calculation
-    }
-    note eq_imp_below[OF this]
-    also
-    note env_restr_split[where S = "domA \<Delta>"]
-    also
-    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S))) f|` domA \<Delta> 
-        = pathsCard (paths (ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))))"
-          by (simp add: filter_paths_conv_free_restr ftree_restr_both ftree_rest_substitute[OF disj1]  ftree_restr_is_empty[OF disj2])
-    also
-    have "ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fheap \<Delta> e\<cdot>a"  by (rule Fheap_substitute)
-    also
-    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S))) f|` (- domA \<Delta>) =
-          pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<otimes>\<otimes> Fstack S)))"
-          by (simp add: filter_paths_conv_free_restr2 ftree_rest_substitute2[OF disj1' const_on3] ftree_restr_both  ftree_restr_noop[OF disj2'])
-    also have "ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks \<Delta>)  (Fexp e\<cdot>a)) \<sqsubseteq> Fexp (Terms.Let \<Delta> e)\<cdot>a" by (rule Fexp_Let)
-    finally
-    show "prognosis (Aheap \<Delta> e\<cdot>a \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae a (\<Gamma>, Terms.Let \<Delta> e, S)"
-      by (simp add: cHeap_def del: fun_meet_simp) 
-  qed
-end
-
-
-end
diff --git a/Launchbury/FTreeImplCardinality.thy b/Launchbury/FTreeImplCardinality.thy
new file mode 100644 (file)
index 0000000..03b4234
--- /dev/null
@@ -0,0 +1,29 @@
+theory FTreeImplCardinality
+imports FTreeAnalysisSpec CardinalityAnalysisSpec CallFutureCardinality
+begin
+
+hide_const Multiset.single
+
+context FTreeAnalysis
+begin
+
+fun unstack :: "stack \<Rightarrow> exp \<Rightarrow> exp" where
+  "unstack [] e = e"
+| "unstack (Upd x # S) e = unstack S e"
+| "unstack (Arg x # S) e = unstack S (App e x)"
+| "unstack (Dummy x # S) e = unstack S e"
+
+fun Fstack :: "stack \<Rightarrow> var ftree"
+  where "Fstack [] = \<bottom>"
+  | "Fstack (Upd x # S) = Fstack S"
+  | "Fstack (Arg x # S) = many_calls x \<otimes>\<otimes> Fstack S"
+  | "Fstack (Dummy x # S) = Fstack S"
+
+lemma carrier_Fstack[simp]: "carrier (Fstack S) = ap S"
+  by (induction S rule: Fstack.induct) (auto simp add: empty_is_bottom[symmetric])
+
+fun prognosis :: "AEnv \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> var \<Rightarrow> two"
+   where "prognosis ae a (\<Gamma>, e, S) = pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)))"
+end
+
+end
diff --git a/Launchbury/FTreeImplCardinalityCorrect.thy b/Launchbury/FTreeImplCardinalityCorrect.thy
new file mode 100644 (file)
index 0000000..4ba18a3
--- /dev/null
@@ -0,0 +1,345 @@
+theory FTreeImplCardinalityCorrect
+imports FTreeImplCardinality FTreeAnalysisSpec CardinalityAnalysisSpec CallFutureCardinality
+begin
+
+lemma pathsCard_paths_nxt:  "pathsCard (paths (nxt f x)) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths f))"
+  apply transfer
+  apply (rule pathsCard_below)
+  apply auto
+  apply (erule below_trans[OF _ monofun_cfun_arg[OF paths_Card_above], rotated]) back
+  apply (auto intro: fun_belowI simp add: record_call_simp two_pred_two_add_once)
+  done
+
+lemma pathsCards_none: "pathsCard (paths t) x = none \<Longrightarrow> x \<notin> carrier t"
+  by transfer (auto dest: pathCards_noneD)
+
+lemma const_on_edom_disj: "const_on f S empty \<longleftrightarrow> edom f \<inter> S = {}"
+  by (auto simp add: empty_is_bottom edom_def)
+
+context FTreeAnalysisCarrier
+begin
+  lemma carrier_FBinds: "carrier ((FBinds \<Gamma>\<cdot>ae) x) \<subseteq> fv \<Gamma>"
+  apply (simp add: Fexp.AnalBinds_lookup)
+  apply (auto split: option.split simp add: empty_is_bottom[symmetric] )
+  apply (case_tac "ae x")
+  apply (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: set_mp[OF Aexp_edom])
+  by (metis (poly_guards_query) contra_subsetD domA_from_set map_of_fv_subset map_of_is_SomeD option.sel)
+end
+
+context FTreeAnalysisCorrect
+begin
+
+  sublocale CardinalityPrognosisShape prognosis
+  proof
+    fix \<Gamma> :: heap and ae ae' :: AEnv and u e S
+    assume "ae f|` domA \<Gamma> = ae' f|` domA \<Gamma>"
+    from Fexp.AnalBinds_cong[OF this]
+    show "prognosis ae u (\<Gamma>, e, S) = prognosis ae' u (\<Gamma>, e, S)" by simp
+  next
+    fix ae a \<Gamma> e S
+    show "const_on (prognosis ae a (\<Gamma>, e, S)) (ap S) many"
+    proof
+      fix x
+      assume "x \<in> ap S"
+      hence "[x,x] \<in> paths (Fstack S)"
+        by (induction S rule: Fstack.induct)
+           (auto 4 4 intro: set_mp[OF both_contains_arg1] set_mp[OF both_contains_arg2] paths_Cons_nxt)
+      hence "[x,x] \<in> paths (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)"
+        by (rule set_mp[OF both_contains_arg2])
+      hence "[x,x] \<in> paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))" 
+        by (rule set_mp[OF substitute_contains_arg])
+      hence "pathCard [x,x] x \<sqsubseteq> pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))) x"
+        by (metis fun_belowD paths_Card_above)
+      also have "pathCard [x,x] x = many"  by (auto simp add: pathCard_def)
+      finally
+      show "prognosis ae a (\<Gamma>, e, S) x = many"
+        by (auto intro: below_antisym)
+    qed
+  next
+    fix \<Gamma> \<Delta> :: heap and e :: exp and ae :: AEnv and u S
+    assume "map_of \<Gamma> = map_of \<Delta>"
+    hence "FBinds \<Gamma> = FBinds \<Delta>" and "thunks \<Gamma> = thunks \<Delta>" by (auto intro!: cfun_eqI  thunks_cong simp add: Fexp.AnalBinds_lookup)
+    thus "prognosis ae u (\<Gamma>, e, S) = prognosis ae u (\<Delta>, e, S)"  by simp
+  next
+    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and u S x
+
+    show "prognosis ae u (delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, S)"
+      by (simp add: substitute_T_delete empty_is_bottom)
+         (intro pathsCard_mono' paths_mono substitute_mono1' Fexp.AnalBinds_delete_below)
+  next
+    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and u S x
+    show "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> prognosis ae u (\<Gamma>, e, Upd x # S)" by simp
+  next
+  fix \<Gamma> :: heap and e :: exp and ae :: AEnv and a S x
+  assume "ae x = \<bottom>"
+
+  hence "FBinds (delete x \<Gamma>)\<cdot>ae = FBinds \<Gamma>\<cdot>ae" by (rule Fexp.AnalBinds_delete_bot)
+  moreover
+  hence "((FBinds \<Gamma>\<cdot>ae) x) = \<bottom>" by (metis Fexp.AnalBinds_delete_lookup)
+  ultimately
+  show "prognosis ae a (\<Gamma>, e, S) \<sqsubseteq> prognosis ae a (delete x \<Gamma>, e, S)"
+    by (simp add: substitute_T_delete empty_is_bottom)
+  next
+    fix ae a \<Gamma> x S
+    have "once \<sqsubseteq> (pathCard [x]) x" by (simp add: two_add_simp)
+    also have "pathCard [x] \<sqsubseteq> pathsCard ({[],[x]})"
+      by (rule paths_Card_above) simp
+    also have "\<dots> = pathsCard (paths (single x))" by simp
+    also have "single x \<sqsubseteq> (Fexp (Var x)\<cdot>a)" by (rule Fexp_Var)
+    also have "\<dots> \<sqsubseteq> Fexp (Var x)\<cdot>a \<otimes>\<otimes> Fstack S" by (rule both_above_arg1)
+    also have "\<dots> \<sqsubseteq> substitute  (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a \<otimes>\<otimes> Fstack S)" by (rule substitute_above_arg)
+    also have "pathsCard (paths \<dots>) x =  prognosis ae a (\<Gamma>, Var x, S) x" by simp
+    finally
+    show "once \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S) x"
+      by this (rule cont2cont_fun, intro cont2cont)+
+  qed
+
+  sublocale CardinalityPrognosisApp prognosis
+  proof default
+    fix ae a \<Gamma> e x S
+    have "Fexp e\<cdot>(inc\<cdot>a)  \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack S = many_calls x  \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<otimes>\<otimes> Fstack S"
+      by (metis both_assoc both_comm)
+    thus "prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, App e x, S)"
+      by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1' Fexp_App)
+  qed
+
+  sublocale CardinalityPrognosisLam prognosis
+  proof default
+    fix ae a \<Gamma> e y x S
+    have "Fexp e[y::=x]\<cdot>(pred\<cdot>a) \<sqsubseteq> many_calls x  \<otimes>\<otimes> Fexp (Lam [y]. e)\<cdot>a"
+      by (rule below_trans[OF Fexp_subst both_mono2'[OF Fexp_Lam]])
+    moreover have "Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack S = many_calls x  \<otimes>\<otimes> Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> Fstack S"
+      by (metis both_assoc both_comm)
+    ultimately  
+    show "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae a (\<Gamma>, Lam [y]. e, Arg x # S)"
+      by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1')
+  qed
+
+  sublocale CardinalityPrognosisVar prognosis
+  proof default
+    fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
+    assume "map_of \<Gamma> x = Some e"
+    assume "ae x = up\<cdot>u"
+
+    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S))) = pathsCard (paths (nxt (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) x))"
+      by simp
+    also
+    have "\<dots> \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))))"
+      by (rule pathsCard_paths_nxt)
+    also
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
+      by (metis both_comm)
+    also
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
+      using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` by (simp add: Fexp.AnalBinds_lookup)
+    also
+    assume "isLam e"
+    hence "x \<notin> thunks \<Gamma>" using `map_of \<Gamma> x = Some e` by (metis thunksE)
+    hence "FBinds \<Gamma>\<cdot>ae = f_nxt (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) x" by (auto simp add: f_nxt_def)
+    hence "and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack S))"
+      by (simp add: substitute_and_then)
+    also
+    have "and_then x (Fstack S) \<sqsubseteq> FTree.single x \<otimes>\<otimes> Fstack S" by (rule and_then_both_single')
+    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF this]]]
+    also
+    have "FTree.single x \<sqsubseteq> Fexp (Var x)\<cdot>a" by (rule Fexp_Var)
+    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF both_mono1'[OF this]]]]
+    finally
+    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a  \<otimes>\<otimes> Fstack S))))" 
+      by this simp_all
+    thus "prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> record_call x\<cdot>(prognosis ae a (\<Gamma>, Var x, S))" by simp
+  next
+    fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
+    assume "map_of \<Gamma> x = Some e"
+    assume "ae x = up\<cdot>u"
+    assume "\<not> isLam e"
+    hence "x \<in> thunks \<Gamma>" using `map_of \<Gamma> x = Some e` by (metis thunksI)
+    hence [simp]: "f_nxt (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) x = FBinds (delete x \<Gamma>)\<cdot>ae" 
+      by (auto simp add: f_nxt_def Fexp.AnalBinds_delete_to_fun_upd empty_is_bottom)
+
+    have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S)))
+       =  pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack S)))"
+       by (rule arg_cong[OF substitute_cong_T]) (auto simp add: empty_is_bottom)
+    also have "\<dots>  = pathsCard (paths (nxt (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S))) x))"
+      by simp
+    also
+    have "\<dots> \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))))"
+      by (rule pathsCard_paths_nxt)
+    also
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
+      by (metis both_comm)
+    also
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
+      using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` by (simp add: Fexp.AnalBinds_lookup)
+    also
+    have "and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack S \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack S))"
+      by (simp add: substitute_and_then)
+    also
+    have "and_then x (Fstack S) \<sqsubseteq> FTree.single x \<otimes>\<otimes> Fstack S" by (rule and_then_both_single')
+    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF this]]]
+    also
+    have "FTree.single x \<sqsubseteq> Fexp (Var x)\<cdot>a" by (rule Fexp_Var)
+    note pathsCard_mono'[OF paths_mono[OF substitute_mono2'[OF both_mono1'[OF this]]]]
+    finally
+    have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack S)))
+       \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a  \<otimes>\<otimes> Fstack S))))" 
+      by this simp_all
+    thus "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x\<cdot>(prognosis ae a (\<Gamma>, Var x, S))" by simp
+  next
+    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and  x :: var and  S
+    assume "isLam e"
+    hence "repeatable (Fexp e\<cdot>0)" by (rule Fun_repeatable)
+
+    assume [simp]: "x \<notin> domA \<Gamma>"
+
+    have [simp]: "thunks ((x, e) # \<Gamma>) = thunks \<Gamma>" 
+      using `isLam e`
+      by (auto simp add: thunks_Cons dest: set_mp[OF thunks_domA])
+
+    have "fup\<cdot>(Fexp e)\<cdot>(ae x) \<sqsubseteq> Fexp e\<cdot>0" by (metis fup2 monofun_cfun_arg up_zero_top)
+    hence "substitute ((FBinds \<Gamma>\<cdot>ae)(x := fup\<cdot>(Fexp e)\<cdot>(ae x))) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S) \<sqsubseteq> substitute ((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S)"
+      by (intro substitute_mono1' fun_upd_mono below_refl)
+    also have "\<dots> = substitute (((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0))(x := empty)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack S)"
+      using `repeatable (Fexp e\<cdot>0)` by (rule substitute_remove_anyways, simp)
+    also have "((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0))(x := empty) = FBinds \<Gamma>\<cdot>ae"
+      by (simp add: fun_upd_idem Fexp.AnalBinds_not_there empty_is_bottom)
+    finally
+    show "prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)"
+      by (simp, intro pathsCard_mono' paths_mono)
+  qed
+end
+
+context FTreeAnalysisCardinalityHeap
+begin
+
+  definition cHeap where
+    "cHeap \<Gamma> e = (\<Lambda> a. pathsCard (paths (Fheap \<Gamma> e\<cdot>a)))"
+
+  lemma cHeap_simp: "(cHeap \<Gamma> e)\<cdot>a = pathsCard (paths (Fheap \<Gamma> e\<cdot>a))"
+    unfolding cHeap_def  by (rule beta_cfun) (intro cont2cont)
+  
+  sublocale CardinalityHeap cHeap.
+  sublocale CardinalityHeapCorrect cHeap Aheap
+  proof
+    fix x \<Gamma> e a
+    assume "x \<in> thunks \<Gamma>"
+    moreover
+    assume "many \<sqsubseteq> (cHeap \<Gamma> e\<cdot>a) x"
+    hence "many \<sqsubseteq> pathsCard (paths (Fheap \<Gamma> e \<cdot>a)) x" unfolding cHeap_def by simp
+    hence "\<exists>p\<in> (paths (Fheap \<Gamma> e\<cdot>a)). \<not> (one_call_in_path x p)" unfolding pathsCard_def
+      by (auto split: if_splits)
+    ultimately
+    show "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
+      by (metis Fheap_thunk)
+  next
+    fix \<Gamma> e a
+    show "edom (cHeap \<Gamma> e\<cdot>a) = edom (Aheap \<Gamma> e\<cdot>a)"
+    by (simp add: cHeap_def Union_paths_carrier carrier_Fheap)
+  qed
+
+  sublocale CardinalityPrognosisEdom prognosis 
+  proof
+    fix ae a \<Gamma> e S
+    show "edom (prognosis ae a (\<Gamma>, e, S)) \<subseteq> fv \<Gamma> \<union> fv e \<union> fv S"
+      apply (simp add: Union_paths_carrier)
+      apply (rule carrier_substitute_below)
+      apply (auto simp add: carrier_Fexp dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF carrier_FBinds])
+      done
+  qed
+  
+  sublocale CardinalityPrognosisLet prognosis cHeap
+  proof
+    fix \<Delta> \<Gamma> :: heap and e :: exp and S :: stack and  ae :: AEnv and a :: Arity
+    assume "atom ` domA \<Delta> \<sharp>* \<Gamma>"
+    assume "atom ` domA \<Delta> \<sharp>* S"
+    assume "edom ae \<subseteq> domA \<Gamma> \<union> upds S"
+
+    have "domA \<Delta> \<inter> edom ae = {}"
+      using fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`] fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`] 
+            `edom ae \<subseteq> domA \<Gamma> \<union> upds S` ups_fv_subset[of S]
+      by auto
+
+    have const_on1:  "\<And> x. const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (carrier ((FBinds \<Gamma>\<cdot>ae) x)) empty"
+      unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
+      by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF Fexp.edom_AnalBinds])
+    have const_on2:  "const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (carrier (Fstack S)) empty"
+      unfolding const_on_edom_disj using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`]
+      by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF Fexp.edom_AnalBinds] set_mp[OF ap_fv_subset ])
+    have  const_on3: "const_on (FBinds \<Gamma>\<cdot>ae) (- (- domA \<Delta>)) FTree.empty"
+      and const_on4: "const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (domA \<Gamma>) FTree.empty"
+      unfolding const_on_edom_disj using fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
+      by (auto dest!:  set_mp[OF Fexp.edom_AnalBinds])
+
+    have disj1: "\<And> x. carrier ((FBinds \<Gamma>\<cdot>ae) x) \<inter> domA \<Delta> = {}"
+      using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`]
+      by (auto dest: set_mp[OF carrier_FBinds])
+    hence disj1': "\<And> x. carrier ((FBinds \<Gamma>\<cdot>ae) x) \<subseteq> - domA \<Delta>" by auto
+    have disj2: "\<And> x. carrier (Fstack S) \<inter> domA \<Delta> = {}"
+      using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`] ap_fv_subset[of S] by auto
+    hence disj2': "carrier (Fstack S) \<subseteq> - domA \<Delta>" by auto
+    
+
+    {
+    fix x
+    have "(FBinds (\<Delta> @ \<Gamma>)\<cdot>(ae \<squnion> Aheap \<Delta> e\<cdot>a)) x = (FBinds \<Gamma>\<cdot>ae) x \<otimes>\<otimes> (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) x"
+    proof (cases "x \<in> domA \<Delta>")
+      case True
+      have "map_of \<Gamma> x = None" using True fresh_distinct[OF `atom \` domA \<Delta> \<sharp>* \<Gamma>`] by (metis disjoint_iff_not_equal domA_def map_of_eq_None_iff)
+      moreover
+      have "ae x = \<bottom>" using True `domA \<Delta> \<inter> edom ae = {}` by auto
+      ultimately
+      show ?thesis using True 
+          by (auto simp add: Fexp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
+    next
+      case False
+      have "map_of \<Delta> x = None" using False by (metis domA_def map_of_eq_None_iff)
+      moreover
+      have "(Aheap \<Delta> e\<cdot>a) x = \<bottom>" using False using edom_Aheap by (metis contra_subsetD edomIff)
+      ultimately
+      show ?thesis using False
+         by (auto simp add: Fexp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
+    qed
+    }
+    note FBinds = ext[OF this]
+
+    {
+    have "pathsCard (paths (substitute (FBinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) (thunks (\<Delta> @ \<Gamma>)) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S)))
+      = pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks (\<Delta> @ \<Gamma>)) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks (\<Delta> @ \<Gamma>))  (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S))))"
+       by (simp add: substitute_substitute[OF const_on1] FBinds)
+    also have "substitute (FBinds \<Gamma>\<cdot>ae) (thunks (\<Delta> @ \<Gamma>)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>)"
+      apply (rule substitute_cong_T)
+      using const_on3
+      by (auto dest: set_mp[OF thunks_domA])
+    also have "substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks (\<Delta> @ \<Gamma>)) = substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>)"
+      apply (rule substitute_cong_T)
+      using const_on4
+      by (auto dest: set_mp[OF thunks_domA])
+    also have "substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack S) = substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S" 
+      by (rule substitute_only_empty_both[OF const_on2])
+    also note calculation
+    }
+    note eq_imp_below[OF this]
+    also
+    note env_restr_split[where S = "domA \<Delta>"]
+    also
+    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S))) f|` domA \<Delta> 
+        = pathsCard (paths (ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a))))"
+          by (simp add: filter_paths_conv_free_restr ftree_restr_both ftree_rest_substitute[OF disj1]  ftree_restr_is_empty[OF disj2])
+    also
+    have "ftree_restr (domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<sqsubseteq> Fheap \<Delta> e\<cdot>a"  by (rule Fheap_substitute)
+    also
+    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack S))) f|` (- domA \<Delta>) =
+          pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a)) \<otimes>\<otimes> Fstack S)))"
+          by (simp add: filter_paths_conv_free_restr2 ftree_rest_substitute2[OF disj1' const_on3] ftree_restr_both  ftree_restr_noop[OF disj2'])
+    also have "ftree_restr (- domA \<Delta>) (substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a))  (thunks \<Delta>)  (Fexp e\<cdot>a)) \<sqsubseteq> Fexp (Terms.Let \<Delta> e)\<cdot>a" by (rule Fexp_Let)
+    finally
+    show "prognosis (Aheap \<Delta> e\<cdot>a \<squnion> ae) a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae a (\<Gamma>, Terms.Let \<Delta> e, S)"
+      by (simp add: cHeap_def del: fun_meet_simp) 
+  qed
+
+  sublocale CardinalityPrognosisCorrect prognosis cHeap Aheap Aexp by default
+end
+
+
+end
index c56d89f..6de5667 100644 (file)
@@ -1,5 +1,5 @@
 theory NoCardinalityAnalysis
-imports CardinalityAnalysis
+imports CardinalityAnalysisSpec
 begin
 
 locale NoCardinalityAnalysis = CorrectArityAnalysisLet +
@@ -41,26 +41,13 @@ definition cHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> (v
 lemma cHeap_simp[simp]: "cHeap \<Gamma> e\<cdot>a = ae2ce (Aheap \<Gamma> e\<cdot>a)"
   unfolding cHeap_def by simp
 
-(*
-lemma cHeap_eqvt[eqvt]: "\<pi> \<bullet> cHeap \<Gamma> e = cHeap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
-  unfolding cHeap_def
-  apply perm_simp
-  apply (rule Abs_cfun_eqvt)
-  apply simp
-  done
-*)
+sublocale CardinalityHeap cHeap.
 
-sublocale CardinalityHeap Aexp Aheap cHeap
+sublocale CardinalityHeapCorrect cHeap Aheap
   apply default
-(*  apply (perm_simp, rule) *)
   apply (erule Aheap_thunk)
   apply simp
   done
-  
-(*
-fun prognosis where 
-  "prognosis ae a (\<Gamma>, e, S) = ae2ce (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a) \<squnion> ((\<lambda>_. many) f|` ap S)"
-*)
 
 fun prognosis where 
   "prognosis ae a (\<Gamma>, e, S) = ((\<lambda>_. many) f|` (edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp e\<cdot>a) \<union> ap S))"
@@ -71,7 +58,7 @@ lemma record_all_noop[simp]:
 
 sublocale CardinalityPrognosis prognosis.
 
-sublocale CardinalityPrognosisCorrect prognosis
+sublocale CardinalityPrognosisShape prognosis
 proof
   case goal1 thus ?case by (simp cong: Abinds_env_restr_cong)
 next
@@ -81,45 +68,52 @@ next
 next
   case goal4 thus ?case by auto
 next
-  case goal5 thus ?case
-    using edom_mono[OF Aexp_App] by (auto intro!: env_restr_mono2)
+  case goal5
+  show ?case by (auto intro: env_restr_mono2 )
 next
   case goal6
-  from edom_mono[OF Aexp_App]
-  have "insert x (edom (Aexp e\<cdot>(inc\<cdot>a))) \<subseteq> edom (Aexp (App e x)\<cdot>a)" by auto
-  thus ?case by (auto intro: env_restr_mono2 )
+  from `ae x = \<bottom>`
+  have "ABinds (delete x \<Gamma>)\<cdot>ae = ABinds \<Gamma>\<cdot>ae" by (rule ABinds_delete_bot)
+  thus ?case by simp
 next
   case goal7
+  from Aexp_Var[where n = a and x = x]
+  have "(Aexp (Var x)\<cdot>a) x \<noteq> \<bottom>" by auto
+  hence "x \<in> edom (Aexp (Var x)\<cdot>a)" by (simp add: edomIff)
+  thus ?case by simp
+qed
+
+sublocale CardinalityPrognosisApp prognosis
+proof
+  case goal1 thus ?case
+    using edom_mono[OF Aexp_App] by (auto intro!: env_restr_mono2)
+qed
+
+sublocale CardinalityPrognosisLam prognosis
+proof
+  case goal1
   have "edom (Aexp e[y::=x]\<cdot>(pred\<cdot>a)) \<subseteq> insert x (edom (env_delete y (Aexp e\<cdot>(pred\<cdot>a))))"
     by (auto dest: set_mp[OF edom_mono[OF Aexp_subst]] )
   also have "\<dots> \<subseteq> insert x (edom (Aexp (Lam [y]. e)\<cdot>a))"
     using edom_mono[OF Aexp_Lam] by auto
   finally show ?case by (auto intro!: env_restr_mono2)
+qed
+
+sublocale CardinalityPrognosisVar prognosis
+proof
+  case goal1
+  thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal1(1)])
 next
-  case goal8
-  thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal8(1)])
-next
-  case goal9
-  thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal9(1)])
+  case goal2
+  thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal2(1)])
 next
-  case goal10
+  case goal3
   have "fup\<cdot>(Aexp e)\<cdot>(ae x) \<sqsubseteq> Aexp e\<cdot>0" by (cases "ae x") (auto intro: monofun_cfun_arg)
   from edom_mono[OF this]
   show ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]])
-next
-  case goal11
-  from `ae x = \<bottom>`
-  have "ABinds (delete x \<Gamma>)\<cdot>ae = ABinds \<Gamma>\<cdot>ae" by (rule ABinds_delete_bot)
-  thus ?case by simp
-next
-  case goal12
-  from Aexp_Var[where n = a and x = x]
-  have "(Aexp (Var x)\<cdot>a) x \<noteq> \<bottom>" by auto
-  hence "x \<in> edom (Aexp (Var x)\<cdot>a)" by (simp add: edomIff)
-  thus ?case by simp
 qed
   
-sublocale CardinalityPrognosisCorrectLet prognosis Aexp Aheap cHeap
+sublocale CardinalityPrognosisLet prognosis  cHeap Aheap
 proof
   case goal1
 
@@ -146,9 +140,11 @@ proof
   thus ?case by (simp add: ae2ce_to_env_restr env_restr_join2 Un_assoc[symmetric] env_restr_mono2)
 qed
 
-sublocale CardinalityPrognosisEdom prognosis Aexp Aheap
+sublocale CardinalityPrognosisEdom prognosis
   by default (auto dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF edom_AnalBinds])
 
+
+sublocale CardinalityPrognosisCorrect prognosis cHeap Aheap Aexp..
 end
 
 end
diff --git a/ROOT b/ROOT
index 967d363..68d136d 100644 (file)
--- a/ROOT
+++ b/ROOT
@@ -35,16 +35,14 @@ session Arity (AFP) in "Launchbury" = "HOLCF-Nominal2" +
   theories
     "ArityAnalysisImpl"
     "TrivialArityAnal"
-    "ArityEtaExpand"
-    "CardinalityEtaExpand"
+    "ArityEtaExpandCorrect"
+    "CardinalityEtaExpandCorrect"
     "EtaExpansionSestoft"
     "DeadCodeRemovalCorrect"
     "DeadCodeRemoval2Correct"
     "DeadCodeRemoval2CorrectSestoft"
     "RedsImprovesArityAnalysis"
     "NoCardinalityAnalysis"
-    "FTreeCardinality"
-    "CoCallImplCorrect"
     "CallArityCorrectEnd2End"
 
 session Nominal2013_1 in "Nominal2-Isabelle2013-1/Nominal" = HOL +