Finish CardinalityetaExpandCorrect with IfThenElse
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 16 Jan 2015 15:50:26 +0000 (15:50 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 16 Jan 2015 15:50:26 +0000 (15:50 +0000)
26 files changed:
Launchbury/AbstractTransform.thy
Launchbury/ArityAnalysisImpl.thy
Launchbury/ArityAnalysisImplCorrect.thy
Launchbury/ArityAnalysisPreImpl.thy
Launchbury/ArityEtaExpand.thy
Launchbury/CardinalityAnalysisSig.thy
Launchbury/CardinalityAnalysisSpec.thy
Launchbury/CardinalityEtaExpandCorrect.thy
Launchbury/CoCallAnalysisImpl.thy
Launchbury/CoCallAnalysisSpec.thy
Launchbury/CoCallGraph-FTree.thy
Launchbury/CoCallGraph.thy
Launchbury/CoCallImplCorrect.thy
Launchbury/CoCallImplFTreeCorrect.thy
Launchbury/DeadCodeRemoval2.thy
Launchbury/DeadCodeRemoval2CorrectSestoft.thy
Launchbury/Env.thy
Launchbury/FTree-HOLCF.thy
Launchbury/FTree.thy
Launchbury/FTreeAnalysisSpec.thy
Launchbury/FTreeImplCardinality.thy
Launchbury/FTreeImplCardinalityCorrect.thy
Launchbury/NoCardinalityAnalysis.thy
Launchbury/SestoftConf.thy
Launchbury/Set-Cpo.thy
Launchbury/TransformTools.thy

index a2f8518..b99432c 100644 (file)
@@ -8,11 +8,13 @@ locale AbstractAnalProp =
   fixes AnalLet :: "heap \<Rightarrow> exp \<Rightarrow> 'a \<Rightarrow> 'b::cont_pt"
   fixes PropLetBody :: "'b \<Rightarrow> 'a"
   fixes PropLetHeap :: "'b\<Rightarrow> var \<Rightarrow> 'a\<^sub>\<bottom>"
+  fixes PropIfScrut :: "'a \<Rightarrow> 'a"
   assumes PropApp_eqvt: "\<pi> \<bullet> PropApp \<equiv> PropApp"
   assumes PropLam_eqvt: "\<pi> \<bullet> PropLam \<equiv> PropLam"
   assumes AnalLet_eqvt: "\<pi> \<bullet> AnalLet \<equiv> AnalLet"
   assumes PropLetBody_eqvt: "\<pi> \<bullet> PropLetBody \<equiv> PropLetBody"
   assumes PropLetHeap_eqvt: "\<pi> \<bullet> PropLetHeap \<equiv> PropLetHeap"
+  assumes PropIfScrut_eqvt: "\<pi> \<bullet> PropIfScrut \<equiv> PropIfScrut"
 
 locale AbstractAnalPropSubst = AbstractAnalProp +
   assumes AnalLet_subst:  "x \<notin> domA \<Gamma> \<Longrightarrow> y \<notin> domA \<Gamma> \<Longrightarrow> AnalLet (\<Gamma>[x::h=y]) (e[x::=y]) a = AnalLet \<Gamma> e a"
@@ -38,7 +40,7 @@ begin
         (map_transform transform (PropLetHeap (AnalLet \<Gamma> e a)) \<Gamma>)
         (transform (PropLetBody (AnalLet \<Gamma> e a)) e)"
   | "transform a (Bool b) = (Bool b)"
-  | "transform a (scrut ? e1 : e2)  = (transform a scrut ? transform a e1 : transform a e2)"
+  | "transform a (scrut ? e1 : e2)  = (transform (PropIfScrut a) scrut ? transform a e1 : transform a e2)"
 proof-
 case goal1
   note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] TransVar_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
@@ -171,13 +173,14 @@ locale AbstractTransformBound = AbstractAnalProp + supp_bounded_transform  +
   assumes PropLetHeapTrans_eqvt: "\<pi> \<bullet> PropLetHeapTrans = PropLetHeapTrans"
   assumes TransBound_eqvt: "\<pi> \<bullet> trans = trans"
 begin
-  sublocale AbstractTransform PropApp PropLam AnalLet PropLetBody PropLetHeap
+  sublocale AbstractTransform PropApp PropLam AnalLet PropLetBody PropLetHeap PropIfScrut
       "(\<lambda> a. Var)"
       "(\<lambda> a. App)"
       "(\<lambda> a. Terms.Lam)"
       "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeapTrans b) \<Gamma>) e)"
   proof-
-  note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] AnalLet_eqvt[eqvt_raw] PropLetHeapTrans_eqvt[eqvt] TransBound_eqvt[eqvt]
+  note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] PropIfScrut_eqvt[eqvt_raw]
+      AnalLet_eqvt[eqvt_raw] PropLetHeapTrans_eqvt[eqvt] TransBound_eqvt[eqvt]
   case goal1
   show ?case
   apply default
@@ -199,13 +202,14 @@ end
 locale AbstractTransformBoundSubst = AbstractAnalPropSubst + AbstractTransformBound + 
   assumes TransBound_subst: "(trans a e)[x::=y] = trans a e[x::=y]"
 begin
-  sublocale AbstractTransformSubst PropApp PropLam AnalLet PropLetBody PropLetHeap
+  sublocale AbstractTransformSubst PropApp PropLam AnalLet PropLetBody PropLetHeap PropIfScrut
       "(\<lambda> a. Var)"
       "(\<lambda> a. App)"
       "(\<lambda> a. Terms.Lam)"
       "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeapTrans b) \<Gamma>) e)"
   proof-
-  note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransBound_eqvt[eqvt]
+  note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] PropIfScrut_eqvt[eqvt_raw]
+       TransBound_eqvt[eqvt]
   case goal1
   show ?case
   apply default
index 6484ca0..3398ce1 100644 (file)
@@ -20,6 +20,6 @@ interpretation ArityAnalysisPreImpl ArityAnalysis.Afix where "Aexp = ArityAnalys
 interpretation ArityAnalysis Aexp.
 
 lemma Aexp_edom': "edom (Aexp e\<cdot>a) \<subseteq> fv e"
-  by (nominal_induct arbitrary: a rule: exp_strong_induct) auto
+  by (nominal_induct arbitrary: a rule: exp_strong_induct) fastforce+
 
 end
index 0efcc2f..151b51a 100644 (file)
@@ -58,6 +58,9 @@ next
     apply (simp add: env_restr_join)
     done
   thus ?case using Let(1,2) by (auto simp add: fresh_star_Pair elim:env_restr_eq_subset[rotated])
+next
+  case (IfThenElse \<Gamma> e)
+  then show ?case by (auto simp add: env_restr_join simp del: fun_meet_simp)
 qed auto
 
 interpretation CorrectArityAnalysis Aexp
index 92c6f5f..75d8540 100644 (file)
@@ -37,7 +37,7 @@ where
 | "Aexp (App e x) = (\<Lambda> n . Aexp e  \<cdot> (inc \<cdot> n) \<squnion> (esing x \<cdot> (up \<cdot> 0)))"
 | "Aexp (Terms.Let as e) = (\<Lambda> n . (Afix Aexp as \<cdot> (Aexp e \<cdot> n \<squnion> thunks_AE as)) f|` (fv (Terms.Let as e)))"
 | "Aexp (Bool b) = \<bottom>"
-| "Aexp (scrut ? e1 : e2) = \<bottom>"
+| "Aexp (scrut ? e1 : e2) = (\<Lambda> n. Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>n \<squnion> Aexp e2\<cdot>n)"
 proof-
 case goal1
     note Afix_eqvt[eqvt]
index 1464b91..b4c92a1 100644 (file)
@@ -1,5 +1,5 @@
 theory ArityEtaExpand
-imports ArityAnalysisSig AbstractTransform  ArityEtaExpansionSestoft
+imports ArityAnalysisSig AbstractTransform ArityEtaExpansionSestoft
 begin
 
 context ArityAnalysisHeapEqvt
@@ -10,10 +10,11 @@ begin
     "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
     "fst"
     "snd"
+    "\<lambda> _. 0"
     "Aeta_expand"
     "snd"
   apply default
-  apply (((rule eq_reflection)?, perm_simp, rule)+)[7]
+  apply (((rule eq_reflection)?, perm_simp, rule)+)
   done
 end
 
index 5731ea5..d131b16 100644 (file)
@@ -3,7 +3,7 @@ imports Arity AEnv "Cardinality-Domain" SestoftConf
 begin
 
 locale CardinalityPrognosis = 
-  fixes prognosis :: "AEnv \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> (var \<Rightarrow> two)"
+  fixes prognosis :: "AEnv \<Rightarrow> Arity list \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> (var \<Rightarrow> two)"
 
 locale CardinalityHeap = 
   fixes cHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> (var \<Rightarrow> two)"
index 943ade7..279f978 100644 (file)
@@ -4,35 +4,34 @@ begin
 
 locale CardinalityPrognosisEdom = CardinalityPrognosis +
   assumes edom_prognosis:
-    "edom (prognosis ae a (\<Gamma>, e, S)) \<subseteq> fv \<Gamma> \<union> fv e \<union> fv S"
+    "edom (prognosis ae as 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"
+  assumes prognosis_env_cong: "ae f|` domA \<Gamma> = ae' f|` domA \<Gamma> \<Longrightarrow> prognosis ae as u (\<Gamma>, e, S) = prognosis ae' as u (\<Gamma>, e, S)"
+  assumes prognosis_reorder: "map_of \<Gamma> = map_of \<Delta>  \<Longrightarrow>  prognosis ae as u (\<Gamma>, e, S) = prognosis ae as u (\<Delta>, e, S)"
+  assumes prognosis_ap: "const_on (prognosis ae as a (\<Gamma>, e, S)) (ap S) many"
+  assumes prognosis_upd: "prognosis ae as u (\<Gamma>, e, S) \<sqsubseteq> prognosis ae as u (\<Gamma>, e, Upd x # S)"
+  assumes prognosis_not_called: "ae x = \<bottom> \<Longrightarrow> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (delete x \<Gamma>, e, S)"
+  assumes prognosis_called: "once \<sqsubseteq> prognosis ae as 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)"
+  assumes prognosis_App: "prognosis ae as (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae as 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)"
+  assumes prognosis_subst_Lam: "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as 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> isVal 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> isVal 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: "isVal 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_Var_lam: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> isVal e \<Longrightarrow> prognosis ae as u (\<Gamma>, e, S) \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
+  assumes prognosis_Var_thunk: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> \<not> isVal e \<Longrightarrow> prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
+  assumes prognosis_Var2: "isVal e \<Longrightarrow> x \<notin> domA \<Gamma> \<Longrightarrow> prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)"
 
 locale CardinalityPrognosisIfThenElse = CardinalityPrognosis +
-  assumes prognosis_IfThenElse: "prognosis ae 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> prognosis ae a (\<Gamma>, scrut ? e1 : e2, S)"
-  assumes prognosis_Alts: "prognosis ae a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, Bool b, Alts e1 e2 # S)"
+  assumes prognosis_IfThenElse: "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S)"
+  assumes prognosis_Alts: "prognosis ae as a (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> prognosis ae (a#as) 0 (\<Gamma>, Bool b, Alts e1 e2 # 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)"
+  "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) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae as 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"
index fc5d51d..3b1cb7b 100644 (file)
@@ -1,5 +1,5 @@
 theory CardinalityEtaExpandCorrect
-imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft
+imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft ArityAnalysisStack 
 begin
 
 context CardinalityPrognosisCorrect
@@ -10,6 +10,7 @@ begin
     "\<lambda> \<Delta> e a . (a, Aheap \<Delta> e\<cdot>a)"
     "fst"
     "snd"
+    "\<lambda> _. 0"
     "Aeta_expand"
     "snd"
   apply default
@@ -27,11 +28,27 @@ begin
 
   type_synonym tstate = "(AEnv \<times> (var \<Rightarrow> two) \<times> Arity \<times> Arity list)"
 
+  fun transform_alts :: "Arity list \<Rightarrow> stack \<Rightarrow> stack"
+    where 
+      "transform_alts _ [] = []"
+    | "transform_alts (a#as) (Alts e1 e2 # S) = (Alts (ccTransform a e1) (ccTransform a e2)) # transform_alts as S"
+    | "transform_alts as (x # S) = x # transform_alts as S"
+
+  lemma transform_alts_Nil[simp]: "transform_alts [] S = S"
+    by (induction  S) auto
+
+  lemma Astack_transform_alts[simp]:
+    "Astack (transform_alts as S) = Astack S"
+   by (induction rule: transform_alts.induct) auto
+
+  lemma fresh_star_transform_alts[intro]: "a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S"
+   by (induction as S  rule: transform_alts.induct) (auto simp add: fresh_star_Cons)
+
   fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
   where "conf_transform (ae, ce, a, as) (\<Gamma>, e, S) =
     (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)), 
      ccTransform a e,
-     restr_stack (edom ce) S)"
+     transform_alts as (restr_stack (edom ce) S))"
 
   inductive stack_consistent :: "Arity list \<Rightarrow> stack \<Rightarrow> bool"
     where 
@@ -43,25 +60,13 @@ begin
     "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)"
   inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"
 
-  fun AEstack :: "Arity list \<Rightarrow> stack \<Rightarrow> AEnv"
-    where 
-      "AEstack _ [] = \<bottom>"
-    | "AEstack (a#as) (Alts e1 e2 # S) = Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a \<squnion> AEstack as S"
-    | "AEstack as (Upd x # S) = esing x\<cdot>(up\<cdot>0) \<squnion> AEstack as S"
-    | "AEstack as (Arg x # S) = esing x\<cdot>(up\<cdot>0) \<squnion> AEstack as S"
-    | "AEstack as (_ # S) = AEstack as S"
-
-  lemma edom_AEstack: "edom (AEstack as S) \<subseteq> fv S"
-    by (induction as S rule: AEstack.induct) (auto simp del: fun_meet_simp dest!: set_mp[OF Aexp_edom])
-    
-
   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> prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> ce
     \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` edom ce \<sqsubseteq> ae
     \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow> many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
     \<Longrightarrow> stack_consistent as (restr_stack (edom ce) S)
@@ -77,7 +82,7 @@ begin
       by (auto dest!: set_mp[OF Aexp_edom])
     moreover
     from assms
-    have "edom (prognosis \<bottom> 0 ([], e, [])) = {}"
+    have "edom (prognosis \<bottom> [] 0 ([], e, [])) = {}"
      by (auto dest!: set_mp[OF edom_prognosis])
     ultimately
     show ?thesis
@@ -91,7 +96,7 @@ begin
   using assms
   proof(induction c c' arbitrary: ae ce a as 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)
+    have "prognosis ae as (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae as a (\<Gamma>, App e x, S)" by (rule prognosis_App)
     with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
       by (cases "x \<in> edom ce") (auto simp add: join_below_iff env_restr_join dest!: below_trans[OF env_restr_mono[OF Aexp_App]] elim: below_trans)
     moreover
@@ -101,7 +106,7 @@ begin
     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)"
+    have "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as a (\<Gamma>, (Lam [y]. e), Arg x # S)"
        by (rule prognosis_subst_Lam)
     moreover
     {
@@ -127,7 +132,7 @@ begin
     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 thunk have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
     from below_trans[OF prognosis_called fun_belowD[OF this] ]
     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
   
@@ -158,30 +163,30 @@ begin
       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"
+      from `prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce`
+      have "prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
         using once by (metis (mono_tags) fun_belowD)
-      hence "x \<notin> ap S" using prognosis_ap[of ae a \<Gamma> "(Var x)" S] by auto
+      hence "x \<notin> ap S" using prognosis_ap[of ae as a \<Gamma> "(Var x)" S] by auto
       
   
       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
-      have *: "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+      have *: "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae as 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"
+      from `prognosis ae as a (\<Gamma>, Var x, S) x \<sqsubseteq> once`
+      have "(record_call x \<cdot> (prognosis ae as 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
+      hence **: "prognosis ae as 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)"
+      have eq: "prognosis (env_delete x ae) as u (delete x \<Gamma>, e, Upd x # S) = prognosis ae as u (delete x \<Gamma>, e, Upd x # S)"
         by (rule prognosis_env_cong) simp
 
       have [simp]: "restr_stack (edom ce - {x}) S = restr_stack (edom ce) S" 
         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"
+      have "prognosis (env_delete x ae) as 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]
+        using ** below_trans[OF below_trans[OF * Cfun.monofun_cfun_arg[OF `prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce`]] record_call_below_arg]
         by (rule below_env_deleteI)
       moreover
 
@@ -199,20 +204,23 @@ begin
         
         
       moreover
+
+      from `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`
+      have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" by simp
       
       {
       from  `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, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G
-             (restrictA (edom ce) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # restr_stack (edom ce) S)"
+             (restrictA (edom ce) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (edom ce) S))"
           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)"
+      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (restrictA (edom ce) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (edom ce) S))"
         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`)
+      have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (restrictA (edom ce)  (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>))), ccTransform u e, transform_alts as (restr_stack (edom ce) S))"
+        by (intro normal_trans Aeta_expand_correct `Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u`)
       also(rtranclp_trans)
       have "\<dots> = conf_transform (env_delete x ae, env_delete x ce, u, as) (delete x \<Gamma>, e, Upd x # S)" 
         by (auto simp add:  map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist)
@@ -226,17 +234,17 @@ begin
       case many
   
       from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isVal e`
-      have "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+      have "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae as 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 *: "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae as 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)
+      have "prognosis ae as 0 (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> ce" using *[unfolded `u=0`] thunk by (auto elim: below_trans)
       moreover
       note `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u  \<squnion> AEstack as S) f|\` edom ce \<sqsubseteq> ae`
       ultimately
@@ -255,7 +263,7 @@ begin
     qed
   next
   case (lamvar \<Gamma> x e S)
-    from lamvar have "prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
+    from lamvar have "prognosis ae as a (\<Gamma>, Var x, S) \<sqsubseteq> ce" by auto
     from below_trans[OF prognosis_called fun_belowD[OF this] ]
     have [simp]: "x \<in> edom ce" by (auto simp add: edom_def)
     then obtain c where "ce x = up\<cdot>c" by (cases "ce x") (auto simp add: edom_def)
@@ -274,19 +282,19 @@ begin
     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)"
+    have "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae as u (\<Gamma>, e, S)"
       using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
-    also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
+    also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae as a (\<Gamma>, Var x, S))"
        using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isVal e`  by (rule prognosis_Var_lam)
-    also have "\<dots> \<sqsubseteq> prognosis ae 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
+    also have "\<dots> \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by (rule record_call_below_arg)
+    finally have *: "prognosis ae as u ((x, e) # delete x \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, Var x, S)" by this simp_all
   
     have "consistent (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
       using lamvar `(ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u) f|\` edom ce \<sqsubseteq> ae`   `ae x = up\<cdot>u` edom_mono[OF *]
       by (auto simp add: join_below_iff env_restr_join thunks_Cons restr_delete_twist split:if_splits intro: below_trans[OF _ `a \<sqsubseteq> u`] below_trans[OF *])
     moreover
   
-    have "Astack (restr_stack (edom ce) S) \<sqsubseteq> u" using lamvar below_trans[OF _ `a \<sqsubseteq> u`] by auto
+    have "Astack (transform_alts as (restr_stack (edom ce) S)) \<sqsubseteq> u" using lamvar below_trans[OF _ `a \<sqsubseteq> u`] by auto
   
     {
     from `isVal e`
@@ -298,13 +306,13 @@ begin
       by (simp add: map_of_map_transform)
     ultimately
     have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>*
-          ((x, Aeta_expand u (transform u e)) # delete x (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))), Aeta_expand u  (transform u e), restr_stack (edom ce) S)"
+          ((x, Aeta_expand u (transform u e)) # delete x (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
        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)"
+    also have "\<dots> = (restrictA (edom ce) ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x \<Gamma>)))), Aeta_expand u  (transform u e), transform_alts as (restr_stack (edom ce) S))"
       using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
       by (simp add: map_transform_Cons map_transform_delete restr_delete_twist del: restr_delete)
     also(subst[rotated]) have "\<dots> \<Rightarrow>\<^sup>* conf_transform (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)"
-      by simp (rule Aeta_expand_correct[OF `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`])
+      by simp (rule Aeta_expand_correct[OF `Astack _ \<sqsubseteq> u`])
     finally(rtranclp_trans)
     have "conf_transform (ae, ce, a, as) (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* conf_transform (ae, ce, u, as) ((x, e) # delete x \<Gamma>, e, S)".
     }
@@ -323,7 +331,7 @@ begin
       hence "a = 0" by auto
   
       from `isVal 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 *: "prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)" by (rule prognosis_Var2)
 
       have "consistent (ae, ce, 0, as) ((x, e) # \<Gamma>, e, S)"
         using var\<^sub>2
@@ -341,15 +349,15 @@ begin
       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)
+      have "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a ((x, e) # \<Gamma>, e, Upd x # S)" by (rule prognosis_upd)
       also
        
       from `ae x = \<bottom>`
-      have "prognosis ae a ((x, e) # \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
+      have "prognosis ae as a ((x, e) # \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae as a (delete x ((x,e) # \<Gamma>), e, Upd x # S)"
         by (rule prognosis_not_called)
       also have  "delete x ((x,e)#\<Gamma>) = \<Gamma>" using `x \<notin> domA \<Gamma>` by simp
       finally
-      have *: "prognosis ae a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae a (\<Gamma>, e, Upd x # S)" by this simp
+      have *: "prognosis ae as a ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (\<Gamma>, e, Upd x # S)" by this simp
 
       have "consistent (ae, ce, a, as) ((x, e) # \<Gamma>, e, S)" using var\<^sub>2
         by (auto simp add: join_below_iff env_restr_join `ce x = \<bottom>` thunks_Cons split:if_splits elim:below_trans[OF *])
@@ -436,9 +444,9 @@ begin
     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
+    have "prognosis (?ae \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> ?ce \<squnion> prognosis ae as a (\<Gamma>, Let \<Delta> e, S)" by (rule prognosis_Let)
+    also have "prognosis ae as a (\<Gamma>, Let \<Delta> e, S) \<sqsubseteq> ce" using let\<^sub>1 by auto
+    finally have "prognosis (?ae \<squnion> ae) as 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
@@ -508,16 +516,16 @@ begin
     hence "(Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a) f|` edom ce \<sqsubseteq> ae"
       by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]])
     moreover
-    have "prognosis ae a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
-    hence "prognosis ae 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
+    have "prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S) \<sqsubseteq> ce" using if\<^sub>1 by auto
+    hence "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> ce"
       by (rule below_trans[OF prognosis_IfThenElse])
     ultimately
     have "consistent (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
       using if\<^sub>1  by (auto simp add: env_restr_join join_below_iff)
     }
     moreover
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
-      sorry
+    have "conf_transform (ae, ce, a, as) (\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
+      by (auto intro: normal step.intros)
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
@@ -526,14 +534,15 @@ begin
     from if\<^sub>2 have [simp]: "a = 0" by auto
 
     {
-    have "prognosis ae 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
-    hence "prognosis ae a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
+    have "prognosis ae (a'#as') 0 (\<Gamma>, Bool b, Alts e1 e2 # S) \<sqsubseteq> ce" using if\<^sub>2 by auto
+    hence "prognosis ae as' a' (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> ce" by (rule below_trans[OF prognosis_Alts])
     then
     have "consistent (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" 
       using if\<^sub>2 by (auto simp add: env_restr_join join_below_iff)
     }
     moreover
-    have "conf_transform (ae, ce, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)" sorry
+    have "conf_transform (ae, ce, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, a', as') (\<Gamma>, if b then e1 else e2, S)"
+      by (auto intro:normal  step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
     ultimately
     show ?case by (blast del: consistentI consistentE)
   next
index 8811138..373c2f0 100644 (file)
@@ -1,5 +1,5 @@
 theory CoCallAnalysisImpl
-imports "Arity-Nominal" "Nominal-HOLCF" "Env-Nominal" "Env-HOLCF" CoCallFix
+imports "Arity-Nominal" "Nominal-HOLCF" "Env-Nominal"  "Env-Set-Cpo" "Env-HOLCF" CoCallFix "/home/jojo/uni/info/isa-where-to-move/Where_To_Move"
 begin
 
 fun combined_restrict :: "var set \<Rightarrow> (AEnv \<times> CoCalls) \<Rightarrow> (AEnv \<times> CoCalls)"
@@ -75,7 +75,8 @@ where
 | "cCCexp (App e x) =    (\<Lambda> n . (fst (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> (esing x \<cdot> (up\<cdot>0)),          snd (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> ccProd {x} (insert x (fv e))))"
 | "cCCexp (Let \<Gamma> e) =    (\<Lambda> n . combined_restrict (fv (Let \<Gamma> e)) (CoCallArityAnalysis.cccFix_choose cCCexp \<Gamma> \<cdot> (cCCexp e\<cdot>n)))"
 | "cCCexp (Bool b) =     \<bottom>"
-| "cCCexp (scrut ? e1 : e2) = \<bottom>"
+| "cCCexp (scrut ? e1 : e2) = (\<Lambda> n. (fst (cCCexp scrut\<cdot>0) \<squnion> fst (cCCexp e1\<cdot>n) \<squnion> fst (cCCexp e2\<cdot>n),
+     snd (cCCexp scrut\<cdot>0) \<squnion> (snd (cCCexp e1\<cdot>n) \<squnion> snd (cCCexp e2\<cdot>n)) \<squnion> ccProd (edom (fst (cCCexp scrut\<cdot>0))) (edom (fst (cCCexp e1\<cdot>n)) \<union> edom (fst (cCCexp e2\<cdot>n)))))"
 proof-
 case goal1
     show ?case
@@ -146,7 +147,8 @@ lemma cCCexp_eq[simp]:
   "cCCexp (App e x)\<cdot>n =    (fst (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> (esing x \<cdot> (up\<cdot>0)),          snd (cCCexp e\<cdot>(inc\<cdot>n)) \<squnion> ccProd {x} (insert x (fv e)))"
   "cCCexp (Let \<Gamma> e)\<cdot>n =    combined_restrict (fv (Let \<Gamma> e)) (CoCallArityAnalysis.cccFix_choose cCCexp \<Gamma> \<cdot> (cCCexp e\<cdot>n))"
   "cCCexp (Bool b)\<cdot>n = \<bottom>"
-  "cCCexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
+  "cCCexp (scrut ? e1 : e2)\<cdot>n = (fst (cCCexp scrut\<cdot>0) \<squnion> fst (cCCexp e1\<cdot>n) \<squnion> fst (cCCexp e2\<cdot>n),
+        snd (cCCexp scrut\<cdot>0) \<squnion> (snd (cCCexp e1\<cdot>n) \<squnion> snd (cCCexp e2\<cdot>n)) \<squnion> ccProd (edom (fst (cCCexp scrut\<cdot>0))) (edom (fst (cCCexp e1\<cdot>n)) \<union> edom (fst (cCCexp e2\<cdot>n))))"
 by (simp_all)
 declare cCCexp.simps[simp del]
 
@@ -158,7 +160,7 @@ lemma Aexp_simps[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|` (fv (Let \<Gamma> e))"
   "atom x \<sharp> e \<Longrightarrow> Aexp (let x be e in exp)\<cdot>n = (fup\<cdot>(Aexp e)\<cdot>(ABind_nonrec x e \<cdot> (Aexp exp\<cdot>n, CCexp exp\<cdot>n)) \<squnion> Aexp exp\<cdot>n) f|` (fv (let x be e in exp))"
   "Aexp (Bool b)\<cdot>n = \<bottom>"
-  "Aexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
+  "Aexp (scrut ? e1 : e2)\<cdot>n = Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>n \<squnion> Aexp e2\<cdot>n"
  by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq)+
 
 
@@ -170,13 +172,15 @@ lemma CCexp_simps[simp]:
   "atom x \<sharp> e \<Longrightarrow> CCexp (let x be e in exp)\<cdot>n =
     cc_restr (fv (let x be e in exp)) (ccBind x e \<cdot>(Aheap_nonrec x e\<cdot>(Aexp exp\<cdot>n, CCexp exp\<cdot>n), CCexp exp\<cdot>n) \<squnion> ccProd (fv e) (ccNeighbors x (CCexp exp\<cdot>n) - (if isVal e then {} else {x})) \<squnion> CCexp exp\<cdot>n)"
   "CCexp (Bool b)\<cdot>n = \<bottom>"
-  "CCexp (scrut ? e1 : e2)\<cdot>n = \<bottom>"
- by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq predCC_eq)+
-
-lemma ccField_CCexp:
-  "ccField (CCexp e\<cdot>n) \<subseteq> fv e"
-by (induction e arbitrary: n rule: exp_induct_rec)
-   (auto simp add: ccField_ccProd predCC_eq dest: set_mp[OF ccField_cc_restr])
+  "CCexp (scrut ? e1 : e2)\<cdot>n = CCexp scrut\<cdot>0 \<squnion> (CCexp e1\<cdot>n \<squnion> CCexp e2\<cdot>n) \<squnion> ccProd (edom (Aexp scrut\<cdot>0)) (edom (Aexp e1\<cdot>n) \<union> edom (Aexp e2\<cdot>n))"
+by (simp add: cccFix_eq Aexp_eq fup_Aexp_eq CCexp_eq fup_CCexp_eq predCC_eq)+
+
+lemma 
+  shows ccField_CCexp: "ccField (CCexp e\<cdot>n) \<subseteq> fv e" and Aexp_edom': "edom (Aexp e\<cdot>n) \<subseteq> fv e"
+  apply (induction e arbitrary: n rule: exp_induct_rec)
+  apply (auto simp add: predCC_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_ccProd_subset])
+  apply fastforce+
+  done
 
 lemma cc_restr_CCexp[simp]:
   "cc_restr (fv e) (CCexp e\<cdot>a) = CCexp e\<cdot>a"
@@ -190,10 +194,6 @@ lemma cc_restr_fup_ccExp_useless[simp]: "cc_restr (fv e) (fup\<cdot>(CCexp e)\<c
   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')
 
 
index e4c9500..60252c6 100644 (file)
@@ -12,6 +12,7 @@ locale CoCallArityCorrect = CoCallArity + CoCallAnalyisHeap + CorrectArityAnalys
   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: "isVal 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 ccExp_IfThenElse: "ccExp scrut\<cdot>0 \<squnion> (ccExp e1\<cdot>a \<squnion> ccExp e2\<cdot>a) \<squnion> ccProd (edom (Aexp scrut\<cdot>0)) (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a)) \<sqsubseteq> ccExp (scrut ? e1 : e2)\<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"
index 03bcab0..5a68de5 100644 (file)
@@ -660,6 +660,11 @@ lemma ccFTree_mono2:
   apply (erule (1) order_trans[OF _ ccNeighbors_mono])
   done
 
+lemma ccFTree_mono:
+  "S \<subseteq> S' \<Longrightarrow> G \<sqsubseteq> G' \<Longrightarrow> ccFTree S G \<sqsubseteq> ccFTree S' G'"
+  by (metis below_trans[OF ccFTree_mono1 ccFTree_mono2])
+
+
 lemma cont_ccFTree2:
   "cont (ccFTree S)"
   apply (rule contI2)
@@ -719,6 +724,11 @@ lemma ccFTree_cong_below: "cc_restr S G \<sqsubseteq> cc_restr S G' \<Longrighta
 lemma ccFTree_cong: "cc_restr S G = cc_restr S G' \<Longrightarrow> ccFTree S G = ccFTree S G'"
   by (metis ccFTree_cc_restr)
 
+lemma either_ccFTree:
+  "ccFTree S G \<oplus>\<oplus> ccFTree S' G' \<sqsubseteq> ccFTree (S \<union> S') (G \<squnion> G')"
+  by (auto intro!: either_belowI ccFTree_mono)
+
 lemma interleave_ccFTree: 
    "ccFTree S G \<otimes>\<otimes> ccFTree S' G' \<sqsubseteq> ccFTree (S \<union> S') (G \<squnion> G' \<squnion> ccProd S S')"
    by transfer' (auto, erule (2) interleave_valid_list)
index 8380dc0..6420bcd 100644 (file)
@@ -1,5 +1,5 @@
 theory CoCallGraph
-imports Main Vars "HOLCF-Join-Classes" "Set-Cpo"
+imports Main Vars "HOLCF-Join-Classes" "HOLCF-Utils" "Set-Cpo"
 begin
 
 default_sort type
@@ -289,22 +289,35 @@ lift_definition ccNeighbors :: "var \<Rightarrow> CoCalls \<Rightarrow> var set"
 
 lemma ccNeighbors_bot[simp]: "ccNeighbors x \<bottom> = {}" by transfer auto
 
-lemma cont_ccProd_ccNeighbors[THEN cont_compose, cont2cont, simp]:
-  "cont (\<lambda>y. ccProd S (ccNeighbors x y))"
+lemma cont_ccProd1:
+  "cont (\<lambda> S. ccProd S S')"
   apply (rule contI)
   apply (thin_tac "chain ?x")
+  apply (subst lub_set)
   apply transfer
   apply auto
   done
 
-lemma cont_ccProd_ccNeighbors_Diff[THEN cont_compose, cont2cont, simp]:
-  "cont (\<lambda>y. ccProd S (ccNeighbors x y - S''))"
+lemma cont_ccProd2:
+  "cont (\<lambda> S'. ccProd S S')"
   apply (rule contI)
   apply (thin_tac "chain ?x")
+  apply (subst lub_set)
   apply transfer
   apply auto
   done
 
+lemmas cont_compose2[OF cont_ccProd1 cont_ccProd2, simp, cont2cont]
+
+lemma cont_ccNeighbors[THEN cont_compose, cont2cont, simp]:
+  "cont (\<lambda>y. ccNeighbors x y)"
+  apply (rule set_contI)
+  apply (thin_tac "chain ?x")
+  apply transfer
+  apply auto
+  done 
+
+
 lemma ccNeighbors_join[simp]: "ccNeighbors x (G \<squnion> G') = ccNeighbors x G \<union> ccNeighbors x G'"
   by transfer auto
 
@@ -432,6 +445,9 @@ lemma ccField_ccProd:
   "ccField (ccProd S S') = (if S = {} then {} else if S' = {} then {} else  S \<union> S')"
   by transfer (auto simp add: Field_def)
 
+lemma ccField_ccProd_subset:
+  "ccField (ccProd S S') \<subseteq>  S \<union> S'"
+  by (simp add: ccField_ccProd)
 
 lemma cont_ccField[THEN cont_compose, simp, cont2cont]:
   "cont ccField"
index c6b5e5e..af91f51 100644 (file)
@@ -183,6 +183,16 @@ next
 
   show "Aexp (let x' be e in exp )[y::=x]\<cdot>a f|` S = Aexp (let x' be e in exp )\<cdot>a f|` S"
     by (simp add: env_restr_join env_delete_env_restr_swap[symmetric] ABind_nonrec_eq)
+next
+  case (IfThenElse scrut e1 e2)
+  case 2[simp]
+    from IfThenElse
+    show "cc_restr S (CCexp (scrut ? e1 : e2)[y::=x]\<cdot>a) = cc_restr S (CCexp (scrut ? e1 : e2)\<cdot>a)"
+      by (auto simp del: edom_env env_restr_empty env_restr_empty_iff simp  add: edom_env[symmetric])
+
+    from IfThenElse(2,4,6)
+    show "Aexp (scrut ? e1 : e2)[y::=x]\<cdot>a f|` S = Aexp (scrut ? e1 : e2)\<cdot>a f|` S"
+       by (auto simp add: env_restr_join simp del: fun_meet_simp)
 qed auto
    
 sublocale CorrectArityAnalysis Aexp
@@ -495,6 +505,10 @@ next
     by (subst Afix_unroll) simp
 
   show "(Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0" by (auto simp add: Aheap_nonrec_simp ABind_nonrec_eq)
+next
+  fix scrut e1 a e2
+  show "CCexp scrut\<cdot>0 \<squnion> (CCexp e1\<cdot>a \<squnion> CCexp e2\<cdot>a) \<squnion> ccProd (edom (Aexp scrut\<cdot>0)) (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a)) \<sqsubseteq> CCexp (scrut ? e1 : e2)\<cdot>a"
+    by simp
 qed
 end
 
index c5a67ca..8e58193 100644 (file)
@@ -143,6 +143,29 @@ next
   thus "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
     unfolding Fexp_simp by (auto intro: single_below)
 next
+  fix scrut e1 a e2
+  have "ccFTree (edom (Aexp e1\<cdot>a)) (ccExp e1\<cdot>a) \<oplus>\<oplus> ccFTree (edom (Aexp e2\<cdot>a)) (ccExp e2\<cdot>a)
+    \<sqsubseteq> ccFTree (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a)) (ccExp e1\<cdot>a \<squnion> ccExp e2\<cdot>a)"
+      by (rule either_ccFTree)
+  note both_mono2'[OF this]
+  also
+  have "ccFTree (edom (Aexp scrut\<cdot>0)) (ccExp scrut\<cdot>0) \<otimes>\<otimes> ccFTree (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a)) (ccExp e1\<cdot>a \<squnion> ccExp e2\<cdot>a)
+    \<sqsubseteq> ccFTree (edom (Aexp scrut\<cdot>0) \<union> (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a))) (ccExp scrut\<cdot>0 \<squnion> (ccExp e1\<cdot>a \<squnion> ccExp e2\<cdot>a) \<squnion> ccProd (edom (Aexp scrut\<cdot>0)) (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a)))"
+    by (rule interleave_ccFTree)
+  also
+  have "edom (Aexp scrut\<cdot>0) \<union> (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a)) = edom (Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a)" by auto
+  also
+  have "Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a \<sqsubseteq> Aexp (scrut ? e1 : e2)\<cdot>a"
+    by (rule Aexp_IfThenElse)
+  also
+  have "ccExp scrut\<cdot>0 \<squnion> (ccExp e1\<cdot>a \<squnion> ccExp e2\<cdot>a) \<squnion> ccProd (edom (Aexp scrut\<cdot>0)) (edom (Aexp e1\<cdot>a) \<union> edom (Aexp e2\<cdot>a)) \<sqsubseteq>
+        ccExp (scrut ? e1 : e2)\<cdot>a"
+    by (rule ccExp_IfThenElse)
+  finally
+  show "Fexp scrut\<cdot>0 \<otimes>\<otimes> (Fexp e1\<cdot>a \<oplus>\<oplus> Fexp e2\<cdot>a) \<sqsubseteq> Fexp (scrut ? e1 : e2)\<cdot>a"
+    unfolding Fexp_simp
+    by this simp_all
+next
   fix e
   assume "isVal e"
   hence [simp]: "ccExp e\<cdot>0 = ccSquare (fv e)" by (rule ccExp_pap)
index 30f56e0..fb4496a 100644 (file)
@@ -166,7 +166,6 @@ case (goal19 as body as' body')
 qed auto
 nominal_termination (eqvt) by lexicographic_order
 
-
 lemma subst_restrictA[simp]:
   "(restrictA S \<Gamma>)[y::h=x] = restrictA S (\<Gamma>[y::h=x])"
   by (induction \<Gamma>) auto
@@ -253,5 +252,4 @@ case (Let \<Gamma> e y x)
   by (auto simp add: fresh_star_at_base fv_subst_eq fresh_star_Pair pure_fresh simp del: Let_eq_iff)
 qed auto
 
-
 end
index 4b07774..f380a08 100644 (file)
@@ -78,12 +78,33 @@ lemma rdch_Cons[simp]:
   unfolding rdcH_def
   by (auto simp add: clearjunk_restrict[symmetric] delete_map_ran[symmetric] simp del: delete_map_ran)
 
+fun rdcS :: "stack \<Rightarrow> stack" where
+  "rdcS [] = []"
+| "rdcS (Alts e1 e2 # S) = (Alts (remove_dead_code e1) (remove_dead_code e2) # rdcS S)"
+| "rdcS (x # S) = x # rdcS S"
+
+lemma rdcS_fresh[intro]: "a \<sharp> S \<Longrightarrow> a \<sharp> rdcS S"
+  by (induction S rule: rdcS.induct)
+     (auto simp add:  fresh_Cons  eqvt_fresh_cong1[OF remove_dead_code.eqvt])
+
+lemma fv_rdcS: "fv (rdcS S) \<subseteq> fv S"
+    using rdcS_fresh by (auto simp add: fresh_def fv_def)
+
+lemma rdcS_Dummy[simp]: "rdcS (map Dummy L) = map Dummy L" 
+  by (induction L) auto
+     
 inductive dc_rel :: "(heap \<times> exp \<times> stack) \<Rightarrow> (heap \<times> exp \<times> stack) \<Rightarrow>  bool" ("_ \<triangleright> _" [50,50] 50 )
-  where "V \<subseteq> domA \<Gamma> \<union> fv S \<Longrightarrow> V \<inter> fv (rdcH V \<Gamma>, remove_dead_code e, S) = {} \<Longrightarrow> (\<Gamma>, e, S) \<triangleright> (rdcH V \<Gamma>, remove_dead_code e, S)"
+  where "V \<subseteq> domA \<Gamma> \<union> upds S \<Longrightarrow> V \<inter> fv (rdcH V \<Gamma>, remove_dead_code e, rdcS S) = {} \<Longrightarrow> (\<Gamma>, e, S) \<triangleright> (rdcH V \<Gamma>, remove_dead_code e, rdcS S)"
 
 inductive_cases dc_rel_elim: "(\<Gamma>, e, S) \<triangleright> (\<Gamma>', e', S')"
 
-lemma dc_relI: "V \<subseteq> domA \<Gamma> \<union> fv S \<Longrightarrow> V \<inter> fv (rdcH V \<Gamma>, remove_dead_code e, S) = {} \<Longrightarrow> \<Gamma>' = rdcH V \<Gamma> \<Longrightarrow> e' = remove_dead_code e \<Longrightarrow> S' = S \<Longrightarrow>  (\<Gamma>, e, S) \<triangleright> (\<Gamma>', e', S')"
+lemma dc_relI:
+  "V \<subseteq> domA \<Gamma> \<union> upds S \<Longrightarrow>
+   V \<inter> fv (rdcH V \<Gamma>, remove_dead_code e, rdcS S) = {} \<Longrightarrow>
+  \<Gamma>' = rdcH V \<Gamma> \<Longrightarrow>
+  e' = remove_dead_code e \<Longrightarrow>
+  S' = rdcS S \<Longrightarrow> 
+  (\<Gamma>, e, S) \<triangleright> (\<Gamma>', e', S')"
   by (auto intro!: dc_rel.intros)
 
 
@@ -144,29 +165,29 @@ theorem DeadCodeRemovalCorrectStep:
 using assms(2)
 proof(rule dc_rel_elim)
   fix V
-  assume V\<^sub>1: "V \<subseteq> domA \<Gamma> \<union> fv S"
-  assume V\<^sub>2: "V \<inter> (fv (rdcH V \<Gamma>) \<union> (fv (remove_dead_code e) \<union> fv S)) = {}"
-  assume eqs: "\<Gamma>' = rdcH V \<Gamma>" "e' = remove_dead_code e" "S' = S"
+  assume V\<^sub>1: "V \<subseteq> domA \<Gamma> \<union> upds S"
+  assume V\<^sub>2: "V \<inter> (fv (rdcH V \<Gamma>) \<union> (fv (remove_dead_code e) \<union> fv (rdcS S))) = {}"
+  assume eqs: "\<Gamma>' = rdcH V \<Gamma>" "e' = remove_dead_code e" "S' = rdcS S"
 
-  have "\<exists> \<Delta>' z' T'. (\<Delta>, z, T) \<triangleright> (\<Delta>', z', T') \<and> (rdcH V \<Gamma>, remove_dead_code e, S) \<Rightarrow>\<^sup>* (\<Delta>', z', T')"
+  have "\<exists> \<Delta>' z' T'. (\<Delta>, z, T) \<triangleright> (\<Delta>', z', T') \<and> (rdcH V \<Gamma>, remove_dead_code e, rdcS S) \<Rightarrow>\<^sup>* (\<Delta>', z', T')"
   using assms(1)
   proof(cases rule: step.cases)
   case (app\<^sub>1 x)
     from V\<^sub>1 V\<^sub>2
-    have "(\<Gamma>, z, Arg x # S) \<triangleright> (rdcH V \<Gamma>, remove_dead_code z, Arg x # S)"
-      unfolding app\<^sub>1  by -(rule dc_relI[where V = V], auto)
+    have "(\<Gamma>, z, Arg x # S) \<triangleright> (rdcH V \<Gamma>, remove_dead_code z, Arg x # rdcS S)"
+      unfolding app\<^sub>1 by -(rule dc_relI[where V = V], auto)
     moreover
-    have "(rdcH V \<Gamma>, remove_dead_code (App z x), S) \<Rightarrow> (rdcH V \<Gamma>, remove_dead_code z, Arg x # S)"
+    have "(rdcH V \<Gamma>, remove_dead_code (App z x), rdcS S) \<Rightarrow> (rdcH V \<Gamma>, remove_dead_code z, Arg x # rdcS S)"
       by simp rule
     ultimately
     show ?thesis unfolding app\<^sub>1 by blast
   next
   case (app\<^sub>2 y e' x)
     from V\<^sub>1 V\<^sub>2
-    have "(\<Gamma>, e'[y::=x], T) \<triangleright> (rdcH V \<Gamma>, remove_dead_code (e'[y::=x]), T)"
+    have "(\<Gamma>, e'[y::=x], T) \<triangleright> (rdcH V \<Gamma>, remove_dead_code (e'[y::=x]), rdcS T)"
       unfolding app\<^sub>2 eqs by -(rule dc_relI[where V = V], auto simp add: fv_subst_eq subst_remove_dead_code[symmetric])
     moreover
-    have "(rdcH V \<Gamma>, remove_dead_code (Lam [y]. e'), Arg x # T) \<Rightarrow> (rdcH V \<Gamma>, remove_dead_code (e'[y::=x]), T)"
+    have "(rdcH V \<Gamma>, remove_dead_code (Lam [y]. e'), rdcS (Arg x # T)) \<Rightarrow> (rdcH V \<Gamma>, remove_dead_code (e'[y::=x]), rdcS T)"
       by (simp add: subst_remove_dead_code[symmetric]) rule
     ultimately
     show ?thesis unfolding app\<^sub>2 by blast
@@ -183,12 +204,12 @@ proof(rule dc_rel_elim)
     have **: "fv (remove_dead_code z) \<subseteq> fv (rdcH V \<Gamma>)" by (metis domA_from_set map_of_fv_subset map_of_is_SomeD option.sel)
 
     from V\<^sub>1 V\<^sub>2
-    have "(delete x \<Gamma>, z, Upd x # S) \<triangleright> (rdcH V (delete x \<Gamma>), remove_dead_code z, Upd x # S)"
+    have "(delete x \<Gamma>, z, Upd x # S) \<triangleright> (rdcH V (delete x \<Gamma>), remove_dead_code z, rdcS (Upd x # S))"
       unfolding var\<^sub>1(1)
       by -(rule dc_relI[where V = V], auto dest: set_mp[OF *] set_mp[OF **])
     moreover
     from  `map_of (rdcH V \<Gamma>) x = Some (remove_dead_code z)`
-    have "(rdcH V \<Gamma>, remove_dead_code (Var x), S) \<Rightarrow> (rdcH V (delete x \<Gamma>), remove_dead_code z, Upd x # S)"
+    have "(rdcH V \<Gamma>, remove_dead_code (Var x), rdcS S) \<Rightarrow> (rdcH V (delete x \<Gamma>), remove_dead_code z, rdcS (Upd x # S))"
       by (simp add: delete_rdcH[symmetric] del: delete_rdcH) rule
     ultimately
     show ?thesis unfolding var\<^sub>1 by blast
@@ -202,12 +223,14 @@ proof(rule dc_rel_elim)
 
 
     from V\<^sub>1 V\<^sub>2
-    have "((x, e) # \<Gamma>, e, T) \<triangleright> ((x,remove_dead_code e) # rdcH V \<Gamma>, remove_dead_code e, T)"
+    have "((x, e) # \<Gamma>, e, T) \<triangleright> ((x,remove_dead_code e) # rdcH V \<Gamma>, remove_dead_code e, rdcS T)"
       unfolding var\<^sub>2(1-1)
       by -(rule dc_relI[where V = V], auto)
     moreover
-    have "(rdcH V \<Gamma>, remove_dead_code e, Upd x # T) \<Rightarrow> ((x,remove_dead_code e) # rdcH V \<Gamma>, remove_dead_code e, T)"
+    have "(rdcH V \<Gamma>, remove_dead_code e, Upd x # rdcS T) \<Rightarrow> ((x,remove_dead_code e) # rdcH V \<Gamma>, remove_dead_code e, rdcS T)"
       by rule simp_all
+    hence "(rdcH V \<Gamma>, remove_dead_code e, rdcS (Upd x # T)) \<Rightarrow> ((x,remove_dead_code e) # rdcH V \<Gamma>, remove_dead_code e, rdcS T)"
+      by simp
     ultimately
     show ?thesis unfolding eqs var\<^sub>2 by blast
   next
@@ -215,7 +238,7 @@ proof(rule dc_rel_elim)
     let "(?\<Delta>', ?body')" = "((restrict_reachable (map_ran (\<lambda>_. remove_dead_code) \<Delta>) (remove_dead_code z)), (remove_dead_code z))"
     let "?V'" = "domA \<Delta> - reachable (map_ran (\<lambda>_. remove_dead_code) \<Delta>) ?body'"
 
-    from fresh_distinct[OF let\<^sub>1(4)] fresh_distinct_fv[OF let\<^sub>1(5)] V\<^sub>1
+    from fresh_distinct[OF let\<^sub>1(4)] fresh_distinct_fv[OF let\<^sub>1(5)] V\<^sub>1 ups_fv_subset
     have "V \<inter> domA \<Delta> = {}" by blast
     hence [simp]: "(rdcH (?V' \<union> V) \<Delta>) = ?\<Delta>'"
       unfolding restrict_reachable_def rdcH_def
@@ -225,7 +248,7 @@ proof(rule dc_rel_elim)
       using fresh_distinct[OF let\<^sub>1(4)]
       by (auto intro: rdcH_cong_set simp add: fresh_star_at_base)
 
-    have "?V' \<union> V \<subseteq> domA (\<Delta> @ \<Gamma>) \<union> fv S" using V\<^sub>1 by auto
+    have "?V' \<union> V \<subseteq> domA (\<Delta> @ \<Gamma>) \<union> upds S" using V\<^sub>1 by auto
     moreover
     {
     have "?V' \<inter> fv ?\<Delta>' = {}" using fv_heap_reachable by auto
@@ -237,7 +260,7 @@ proof(rule dc_rel_elim)
     moreover
     have "?V' \<inter> fv ?body' = {}" using fv_e_reachable by auto
     moreover
-    have "?V' \<inter> fv S = {}" using fresh_distinct_fv[OF let\<^sub>1(5)] by auto
+    have "?V' \<inter> fv (rdcS S) = {}" using fresh_distinct_fv[OF let\<^sub>1(5)] by (auto dest: set_mp[OF fv_rdcS])
     moreover
     have "V \<inter> fv ?\<Delta>' = {}" using V\<^sub>2 `V \<inter> domA \<Delta> = {}` unfolding let\<^sub>1 by auto
     moreover
@@ -245,21 +268,41 @@ proof(rule dc_rel_elim)
     moreover
     have "V \<inter> fv ?body' = {}" using V\<^sub>2  `V \<inter> domA \<Delta> = {}` unfolding let\<^sub>1 by auto
     moreover
-    have "V \<inter> fv S = {}"  using V\<^sub>2 by auto
+    have "V \<inter> fv (rdcS S) = {}"  using V\<^sub>2 by auto
     ultimately
-    have "(?V' \<union> V) \<inter> fv (rdcH (?V' \<union> V) (\<Delta> @ \<Gamma>), ?body', S) = {}"
-      using fresh_distinct[OF let\<^sub>1(4)] by auto
+    have "(?V' \<union> V) \<inter> fv (rdcH (?V' \<union> V) (\<Delta> @ \<Gamma>), ?body', rdcS S) = {}"
+      using fresh_distinct[OF let\<^sub>1(4)] by (auto )
     }
     ultimately
-    have "(\<Delta> @ \<Gamma>, z, S) \<triangleright> (rdcH (?V' \<union> V) (\<Delta> @ \<Gamma>), ?body', S)"..
+    have "(\<Delta> @ \<Gamma>, z, S) \<triangleright> (rdcH (?V' \<union> V) (\<Delta> @ \<Gamma>), ?body', rdcS S)"..
     also
-    have "atom ` domA ?\<Delta>' \<sharp>* rdcH V \<Gamma>" and  "atom ` domA ?\<Delta>' \<sharp>* S"
+    have "atom ` domA ?\<Delta>' \<sharp>* rdcH V \<Gamma>" and  "atom ` domA ?\<Delta>' \<sharp>* rdcS S"
       using let\<^sub>1(4,5) by (auto simp add: fresh_star_def fresh_Pair)
     from SmartLet_stepI[OF this]
-    have "(rdcH V \<Gamma>, remove_dead_code (Terms.Let \<Delta> z), S) \<Rightarrow>\<^sup>* (rdcH (?V' \<union> V) (\<Delta> @ \<Gamma>), ?body', S)"
+    have "(rdcH V \<Gamma>, remove_dead_code (Terms.Let \<Delta> z), rdcS S) \<Rightarrow>\<^sup>* (rdcH (?V' \<union> V) (\<Delta> @ \<Gamma>), ?body', rdcS S)"
       using fresh_distinct[OF let\<^sub>1(4)] by simp
     ultimately
     show ?thesis unfolding let\<^sub>1 by blast
+  next
+    case (if\<^sub>1 e1 e2)
+    from V\<^sub>1 V\<^sub>2
+    have "(\<Gamma>, z, Alts e1 e2 # S) \<triangleright> (rdcH V \<Gamma>, remove_dead_code z, Alts (remove_dead_code e1) (remove_dead_code e2) # rdcS S)"
+      unfolding if\<^sub>1 by -(rule dc_relI[where V = V], auto)
+    moreover
+    have "(rdcH V \<Gamma>, remove_dead_code (z ? e1 : e2), rdcS S) \<Rightarrow> (rdcH V \<Gamma>, remove_dead_code z,  Alts (remove_dead_code e1) (remove_dead_code e2) # rdcS S)"
+      by simp rule
+    ultimately
+    show ?thesis unfolding if\<^sub>1 by blast
+  next
+    case (if\<^sub>2 b e1 e2)
+    from V\<^sub>1 V\<^sub>2
+    have "(\<Gamma>, (if b then e1 else e2), T) \<triangleright> (rdcH V \<Gamma>, (if b then remove_dead_code e1 else remove_dead_code e2), rdcS T)"
+      unfolding if\<^sub>2 by -(rule dc_relI[where V = V],auto)
+    moreover
+    have "(rdcH V \<Gamma>, remove_dead_code (Bool b), rdcS (Alts e1 e2 # T)) \<Rightarrow> (rdcH V \<Gamma>, (if b then remove_dead_code e1 else remove_dead_code e2), rdcS T)"
+      by (auto intro:  step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
+    ultimately
+    show ?thesis unfolding if\<^sub>2 by blast
   qed
   thus ?thesis unfolding eqs.
 qed
@@ -276,27 +319,27 @@ corollary
    shows  "\<exists> \<Delta>' z'. [] : remove_dead_code e \<Down>\<^bsub>L\<^esub> \<Delta>' : z'"
 proof-
   let "?S" = "map Dummy L"
-  have *: "set (map Dummy L) \<subseteq> range Dummy" by auto
+  have *: "set (rdcS ?S) \<subseteq> range Dummy" by auto
 
   have "L = flattn ?S" by (induction L) auto
   from lemma_2[OF assms(1) this]
   have "([], e, ?S) \<Rightarrow>\<^sup>* (\<Delta>, z, ?S)".
   moreover
-  have "([], e, ?S) \<triangleright> (rdcH {} [], remove_dead_code e, ?S)" by (rule dc_rel.intros) auto
-  hence "([], e, ?S) \<triangleright> ([], remove_dead_code e, ?S)" by simp
+  have "([], e, ?S) \<triangleright> (rdcH {} [], remove_dead_code e, rdcS ?S)" by (rule dc_rel.intros) auto
+  hence "([], e, ?S) \<triangleright> ([], remove_dead_code e, rdcS  ?S)" by simp
   ultimately
-  obtain \<Delta>' z' T' where "(\<Delta>, z, ?S) \<triangleright> (\<Delta>', z', T')" and "([], remove_dead_code e, ?S) \<Rightarrow>\<^sup>* (\<Delta>', z', T')"
+  obtain \<Delta>' z' T' where "(\<Delta>, z, ?S) \<triangleright> (\<Delta>', z', T')" and "([], remove_dead_code e, rdcS  ?S) \<Rightarrow>\<^sup>* (\<Delta>', z', T')"
     by (metis DeadCodeRemovalCorrectSteps)
-  hence "([], remove_dead_code e, ?S) \<Rightarrow>\<^sup>* (\<Delta>', remove_dead_code z, ?S)" by (auto elim: dc_rel.cases)
+  hence "([], remove_dead_code e, rdcS ?S) \<Rightarrow>\<^sup>* (\<Delta>', remove_dead_code z, rdcS ?S)" by (auto elim: dc_rel.cases)
   from dummy_stack_balanced[OF * this]
-  obtain T where "bal ([], remove_dead_code e, map Dummy L) T (\<Delta>', remove_dead_code z, map Dummy L)".
+  obtain T where "bal ([], remove_dead_code e, rdcS ?S) T (\<Delta>', remove_dead_code z, rdcS ?S)".
   moreover
   have "isLam z" using assms(1) by (induction) simp
   hence "isLam (remove_dead_code z)" by (rule isLam_remove_dead_code)
   ultimately
-  have "[] : remove_dead_code e \<Down>\<^bsub>flattn ?S\<^esub> \<Delta>' : remove_dead_code z"
+  have "[] : remove_dead_code e \<Down>\<^bsub>flattn (rdcS ?S)\<^esub> \<Delta>' : remove_dead_code z"
     by (rule lemma_3)
-  also have "flattn ?S = L" by (induction L) auto
+  also have "flattn (rdcS ?S) = L" by (induction L) auto
   finally
   show ?thesis by blast
 qed
index 234950e..156eae8 100644 (file)
@@ -70,7 +70,7 @@ lemma env_restr_empty_iff[simp]: "m f|` S = \<bottom> \<longleftrightarrow> edom
   apply metis
   apply (fastforce simp add: edom_def env_restr_def lambda_strict[symmetric]  split:if_splits)
   done
-lemmas iffD2[OF env_restr_empty_iff, simp]
+lemmas env_restr_empty = iffD2[OF env_restr_empty_iff, simp]
 
 lemma lookup_env_restr[simp]: "x \<in> S \<Longrightarrow> (m f|` S) x = m x"
   by (fastforce simp add: env_restr_def)
index 46b11e0..c436110 100644 (file)
@@ -59,18 +59,27 @@ lemma carrier_mono: "t \<sqsubseteq> t' \<Longrightarrow> carrier t \<subseteq>
 lemma nxt_mono: "t \<sqsubseteq> t' \<Longrightarrow> nxt t x \<sqsubseteq> nxt t' x"
   by transfer auto
 
-lemma both_above_arg1: "t \<sqsubseteq> both t t'"
+lemma either_above_arg1: "t \<sqsubseteq> t \<oplus>\<oplus> t'"
   by transfer fastforce
 
-lemma both_above_arg2: "t' \<sqsubseteq> both t t'"
+lemma either_above_arg2: "t' \<sqsubseteq> t \<oplus>\<oplus> t'"
+  by transfer fastforce
+
+lemma either_belowI: "t \<sqsubseteq> t'' \<Longrightarrow> t' \<sqsubseteq> t'' \<Longrightarrow> t \<oplus>\<oplus> t' \<sqsubseteq> t''"
+  by transfer auto
+
+lemma both_above_arg1: "t \<sqsubseteq> t \<otimes>\<otimes> t'"
+  by transfer fastforce
+
+lemma both_above_arg2: "t' \<sqsubseteq> t \<otimes>\<otimes> t'"
   by transfer fastforce
 
 lemma both_mono1':
-  "t \<sqsubseteq> t' \<Longrightarrow> both t t'' \<sqsubseteq> both t' t''"
+  "t \<sqsubseteq> t' \<Longrightarrow> t \<otimes>\<otimes> t'' \<sqsubseteq> t' \<otimes>\<otimes> t''"
   using  both_mono1[folded below_set_def, unfolded paths_mono_iff].
 
 lemma both_mono2':
-  "t \<sqsubseteq> t' \<Longrightarrow> both t'' t \<sqsubseteq> both t'' t'"
+  "t \<sqsubseteq> t' \<Longrightarrow> t'' \<otimes>\<otimes> t \<sqsubseteq> t'' \<otimes>\<otimes> t'"
   using  both_mono2[folded below_set_def, unfolded paths_mono_iff].
 
 lemma substitute_mono1': "f \<sqsubseteq> f'\<Longrightarrow> substitute f T t \<sqsubseteq> substitute f' T t"
index 6790e18..74e456c 100644 (file)
@@ -311,6 +311,15 @@ lemma nxt_either[simp]: "nxt (t \<oplus>\<oplus> t') x = nxt t x \<oplus>\<oplus
 lemma paths_either[simp]: "paths (t \<oplus>\<oplus> t') = paths t \<union> paths t'"
   by transfer simp
 
+lemma carrier_either[simp]:
+  "carrier (t \<oplus>\<oplus> t') = carrier t \<union> carrier t'"
+  by transfer simp
+
+lemma either_contains_arg1: "paths t \<subseteq> paths (t \<oplus>\<oplus> t')"
+  by transfer fastforce
+
+lemma either_contains_arg2: "paths t' \<subseteq> paths (t \<oplus>\<oplus> t')"
+  by transfer fastforce
 
 lift_definition Either :: "'a ftree set \<Rightarrow> 'a ftree"  is "\<lambda> S. insert [] (\<Union>S)"
   by (auto simp add: downset_def)
index 0937e8d..97f4d09 100644 (file)
@@ -13,6 +13,7 @@ locale FTreeAnalysisCorrect = FTreeAnalysisCarrier +
   assumes Fexp_subst: "Fexp (e[y::=x])\<cdot>a \<sqsubseteq> many_calls x \<otimes>\<otimes> without y ((Fexp e)\<cdot>a)"
   assumes Fexp_Var: "single v \<sqsubseteq> Fexp (Var v)\<cdot>a"
   assumes Fun_repeatable: "isVal e \<Longrightarrow> repeatable (Fexp e\<cdot>0)"
+  assumes Fexp_IfThenElse: "Fexp scrut\<cdot>0 \<otimes>\<otimes> (Fexp e1\<cdot>a \<oplus>\<oplus> Fexp e2\<cdot>a) \<sqsubseteq> Fexp (scrut ? e1 : e2)\<cdot>a"
 
 locale FTreeAnalysisCardinalityHeap = 
   FTreeAnalysisCorrect + CorrectArityAnalysisLet + 
index 75b1827..6b9ba62 100644 (file)
@@ -14,18 +14,21 @@ fun unstack :: "stack \<Rightarrow> exp \<Rightarrow> exp" where
 | "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 (Alts e1 e2 # S) = Fstack S"
-  | "Fstack (Upd x # S) = Fstack S"
-  | "Fstack (Arg x # S) = many_calls x \<otimes>\<otimes> Fstack S"
-  | "Fstack (Dummy x # S) = Fstack S"
+fun Fstack :: "Arity list \<Rightarrow> stack \<Rightarrow> var ftree"
+  where "Fstack _ [] = \<bottom>"
+  | "Fstack (a#as) (Alts e1 e2 # S) = (Fexp e1\<cdot>a \<oplus>\<oplus> Fexp e2\<cdot>a) \<otimes>\<otimes> Fstack as S"
+  | "Fstack as (Arg x # S) = many_calls x \<otimes>\<otimes> Fstack as S"
+  | "Fstack as (_ # S) = Fstack as 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)))"
+fun prognosis :: "AEnv \<Rightarrow> Arity list \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> var \<Rightarrow> two"
+   where "prognosis ae as a (\<Gamma>, e, S) = pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack as S)))"
 end
 
 end
index 86a366b..7e1163d 100644 (file)
@@ -20,6 +20,10 @@ lemma const_on_edom_disj: "const_on f S empty \<longleftrightarrow> edom f \<int
 
 context FTreeAnalysisCarrier
 begin
+  lemma carrier_Fstack: "carrier (Fstack as S) \<subseteq> fv S"
+    by (induction S rule: Fstack.induct)
+       (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: set_mp[OF Aexp_edom])
+
   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] )
@@ -33,125 +37,119 @@ begin
 
   sublocale CardinalityPrognosisShape prognosis
   proof
-    fix \<Gamma> :: heap and ae ae' :: AEnv and u e S
+    fix \<Gamma> :: heap and ae ae' :: AEnv and u e S as
     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
+    show "prognosis ae as u (\<Gamma>, e, S) = prognosis ae' as 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"
+    fix ae as a \<Gamma> e S
+    show "const_on (prognosis ae as a (\<Gamma>, e, S)) (ap S) many"
     proof
       fix x
       assume "x \<in> ap S"
-      hence "[x,x] \<in> paths (Fstack S)"
+      hence "[x,x] \<in> paths (Fstack as 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)"
+      hence "[x,x] \<in> paths (Fexp e\<cdot>a \<otimes>\<otimes> Fstack as 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))" 
+      hence "[x,x] \<in> paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack as 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"
+      hence "pathCard [x,x] x \<sqsubseteq> pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack as 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"
+      show "prognosis ae as 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
+    fix \<Gamma> \<Delta> :: heap and e :: exp and ae :: AEnv and as 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)
+    thus "prognosis ae as u (\<Gamma>, e, S) = prognosis ae as u (\<Delta>, e, S)"  by simp
   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
+    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and as u S x
+    show "prognosis ae as u (\<Gamma>, e, S) \<sqsubseteq> prognosis ae as u (\<Gamma>, e, Upd x # S)" by simp
   next
-  fix \<Gamma> :: heap and e :: exp and ae :: AEnv and a S x
+  fix \<Gamma> :: heap and e :: exp and ae :: AEnv and as 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)"
+  show "prognosis ae as a (\<Gamma>, e, S) \<sqsubseteq> prognosis ae as a (delete x \<Gamma>, e, S)"
     by (simp add: substitute_T_delete empty_is_bottom)
   next
-    fix ae a \<Gamma> x S
+    fix ae as 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
+    also have "\<dots> \<sqsubseteq> Fexp (Var x)\<cdot>a \<otimes>\<otimes> Fstack as 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 as S)" by (rule substitute_above_arg)
+    also have "pathsCard (paths \<dots>) x = prognosis ae as a (\<Gamma>, Var x, S) x" by simp
     finally
-    show "once \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S) x"
+    show "once \<sqsubseteq> prognosis ae as 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"
+    fix ae as a \<Gamma> e x S
+    have "Fexp e\<cdot>(inc\<cdot>a)  \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack as S = many_calls x  \<otimes>\<otimes> (Fexp e)\<cdot>(inc\<cdot>a) \<otimes>\<otimes> Fstack as 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)"
+    thus "prognosis ae as (inc\<cdot>a) (\<Gamma>, e, Arg x # S) \<sqsubseteq> prognosis ae as 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
+    fix ae as 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"
+    moreover have "Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> many_calls x \<otimes>\<otimes> Fstack as S = many_calls x  \<otimes>\<otimes> Fexp (Lam [y]. e)\<cdot>a \<otimes>\<otimes> Fstack as 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)"
+    show "prognosis ae as (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae as 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
+    fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and as 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))"
+    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack as S))) = pathsCard (paths (nxt (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack as 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)))))"
+    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 as 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  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack as 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  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack as 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 "isVal 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))"
+    hence "and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack as S \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack as 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')
+    have "and_then x (Fstack as S) \<sqsubseteq> single x \<otimes>\<otimes> Fstack as 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)
+    have "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))))" 
+    have "pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack as S))) \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a \<otimes>\<otimes> Fstack as 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
+    thus "prognosis ae as u (\<Gamma>, e, S) \<sqsubseteq> record_call x\<cdot>(prognosis ae as a (\<Gamma>, Var x, S))" by simp
   next
-    fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
+    fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and as u a S
     assume "map_of \<Gamma> x = Some e"
     assume "ae x = up\<cdot>u"
     assume "\<not> isVal e"
@@ -159,36 +157,36 @@ begin
     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)))"
+    have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack as S)))
+       =  pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fexp e\<cdot>u \<otimes>\<otimes> Fstack as 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))"
+    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 as 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)))))"
+    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 as 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  \<otimes>\<otimes> Fexp e\<cdot>u)))))"
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack as 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  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
+    have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack as 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))"
+    have "and_then x (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks \<Gamma>) (Fstack as S \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)) = substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (and_then x (Fstack as 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')
+    have "and_then x (Fstack as S) \<sqsubseteq> single x \<otimes>\<otimes> Fstack as 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)
+    have "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))))" 
+    have "pathsCard (paths (substitute (FBinds (delete x \<Gamma>)\<cdot>ae) (thunks (delete x \<Gamma>)) (Fexp e\<cdot>u  \<otimes>\<otimes> Fstack as S)))
+       \<sqsubseteq> record_call x\<cdot>(pathsCard (paths (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Var x)\<cdot>a  \<otimes>\<otimes> Fstack as 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
+    thus "prognosis ae as u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x\<cdot>(prognosis ae as a (\<Gamma>, Var x, S))" by simp
   next
-    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and  x :: var and  S
+    fix \<Gamma> :: heap and e :: exp and ae :: AEnv and  x :: var and as S
     assume "isVal e"
     hence "repeatable (Fexp e\<cdot>0)" by (rule Fun_repeatable)
 
@@ -199,16 +197,36 @@ begin
       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)"
+    hence "substitute ((FBinds \<Gamma>\<cdot>ae)(x := fup\<cdot>(Fexp e)\<cdot>(ae x))) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack as S) \<sqsubseteq> substitute ((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack as 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)"
+    also have "\<dots> = substitute (((FBinds \<Gamma>\<cdot>ae)(x := Fexp e\<cdot>0))(x := empty)) (thunks \<Gamma>) (Fexp e\<cdot>0 \<otimes>\<otimes> Fstack as 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)"
+    show "prognosis ae as 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae as 0 (\<Gamma>, e, Upd x # S)"
       by (simp, intro pathsCard_mono' paths_mono)
   qed
+
+  sublocale CardinalityPrognosisIfThenElse prognosis
+  proof default
+    fix ae as \<Gamma> scrut e1 e2 S a
+    have "Fexp scrut\<cdot>0 \<otimes>\<otimes> (Fexp e1\<cdot>a \<oplus>\<oplus> Fexp e2\<cdot>a) \<sqsubseteq> Fexp (scrut ? e1 : e2)\<cdot>a"
+      by (rule Fexp_IfThenElse)
+    hence "substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp scrut\<cdot>0 \<otimes>\<otimes> (Fexp e1\<cdot>a \<oplus>\<oplus> Fexp e2\<cdot>a) \<otimes>\<otimes> Fstack as S) \<sqsubseteq> substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (scrut ? e1 : e2)\<cdot>a \<otimes>\<otimes> Fstack as S)"
+      by (rule substitute_mono2'[OF both_mono1'])
+    thus "prognosis ae (a#as) 0 (\<Gamma>, scrut, Alts e1 e2 # S) \<sqsubseteq> prognosis ae as a (\<Gamma>, scrut ? e1 : e2, S)"
+      by (simp, intro pathsCard_mono' paths_mono)
+  next
+    fix ae as a \<Gamma> b e1 e2 S
+    have "Fexp (if b then e1 else e2)\<cdot>a \<sqsubseteq> Fexp e1\<cdot>a \<oplus>\<oplus> Fexp e2\<cdot>a"
+      by (auto simp add: either_above_arg1 either_above_arg2)
+    hence "substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (if b then e1 else e2)\<cdot>a \<otimes>\<otimes> Fstack as S) \<sqsubseteq> substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fexp (Bool b)\<cdot>0 \<otimes>\<otimes> (Fexp e1\<cdot>a \<oplus>\<oplus> Fexp e2\<cdot>a) \<otimes>\<otimes> Fstack as S)"
+      by (rule substitute_mono2'[OF both_mono1'[OF below_trans[OF _ both_above_arg2]]])
+    thus "prognosis ae as a (\<Gamma>, if b then e1 else e2, S) \<sqsubseteq> prognosis ae (a#as) 0 (\<Gamma>, Bool b, Alts e1 e2 # S)"
+      by (auto intro!: pathsCard_mono' paths_mono)
+  qed
+
 end
 
 context FTreeAnalysisCardinalityHeap
@@ -242,17 +260,17 @@ begin
 
   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"
+    fix ae as a \<Gamma> e S
+    show "edom (prognosis ae as 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])
+      apply (auto simp add: carrier_Fexp dest: set_mp[OF Aexp_edom] set_mp[OF carrier_Fstack] 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
+    fix \<Delta> \<Gamma> :: heap and e :: exp and S :: stack and  ae :: AEnv and a :: Arity and as
     assume "atom ` domA \<Delta> \<sharp>* \<Gamma>"
     assume "atom ` domA \<Delta> \<sharp>* S"
     assume "edom ae \<subseteq> domA \<Gamma> \<union> upds S"
@@ -265,9 +283,9 @@ begin
     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"
+    have const_on2:  "const_on (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (carrier (Fstack as 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 ])
+      by (auto dest!: set_mp[OF carrier_FBinds] set_mp[OF carrier_Fstack] 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>`]
@@ -277,9 +295,9 @@ begin
       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
+    have disj2: "\<And> x. carrier (Fstack as S) \<inter> domA \<Delta> = {}"
+      using fresh_distinct_fv[OF `atom \` domA \<Delta> \<sharp>* S`] by (auto dest!: set_mp[OF carrier_Fstack])
+    hence disj2': "carrier (Fstack as S) \<subseteq> - domA \<Delta>" by auto
     
 
     {
@@ -306,8 +324,8 @@ begin
     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))))"
+    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 as 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 as 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)
@@ -317,7 +335,7 @@ begin
       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" 
+    also have "substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a \<otimes>\<otimes> Fstack as S) = substitute (FBinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) (thunks \<Delta>) (Fexp e\<cdot>a) \<otimes>\<otimes> Fstack as S"
       by (rule substitute_only_empty_both[OF const_on2])
     also note calculation
     }
@@ -325,18 +343,18 @@ begin
     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> 
+    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 as 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)))"
+    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 as 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 as 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)"
+    show "prognosis (Aheap \<Delta> e\<cdot>a \<squnion> ae) as a (\<Delta> @ \<Gamma>, e, S) \<sqsubseteq> cHeap \<Delta> e\<cdot>a \<squnion> prognosis ae as a (\<Gamma>, Terms.Let \<Delta> e, S)"
       by (simp add: cHeap_def del: fun_meet_simp) 
   qed
 
index 6de5667..8a8aca4 100644 (file)
@@ -1,5 +1,5 @@
 theory NoCardinalityAnalysis
-imports CardinalityAnalysisSpec
+imports CardinalityAnalysisSpec ArityAnalysisStack
 begin
 
 locale NoCardinalityAnalysis = CorrectArityAnalysisLet +
@@ -50,12 +50,20 @@ sublocale CardinalityHeapCorrect cHeap Aheap
   done
 
 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))"
+  "prognosis ae as a (\<Gamma>, e, S) = ((\<lambda>_. many) f|` (edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp e\<cdot>a) \<union> edom (AEstack as S)))"
 
 lemma record_all_noop[simp]:
   "record_call x\<cdot>((\<lambda>_. many) f|` S) = (\<lambda>_. many) f|` S"
   by (auto simp add: record_call_def lookup_env_restr_eq)
 
+lemma const_on_restr_constI[intro]:
+  "S' \<subseteq> S \<Longrightarrow> const_on ((\<lambda> _. x) f|` S) S' x"
+  by fastforce
+
+lemma ap_subset_edom_AEstack: "ap S \<subseteq> edom (AEstack as S)"
+  by (induction as S rule:AEstack.induct) (auto simp del: fun_meet_simp)
+  
+
 sublocale CardinalityPrognosis prognosis.
 
 sublocale CardinalityPrognosisShape prognosis
@@ -64,19 +72,19 @@ proof
 next
   case goal2 thus ?case by (simp cong: Abinds_reorder)
 next
-  case goal3 thus ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]])
+  case goal3
+  thus ?case 
+  by (auto dest: set_mp[OF ap_subset_edom_AEstack])
 next
-  case goal4 thus ?case by auto
+  case goal4
+  thus ?case by (auto intro: env_restr_mono2 )
 next
   case goal5
-  show ?case by (auto intro: env_restr_mono2 )
-next
-  case goal6
   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
+  case goal6
   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)
@@ -105,13 +113,28 @@ proof
   thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal1(1)])
 next
   case goal2
-  thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal2(1)])
+  thus ?case
+    by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal2(1)])
+       (metis Aexp_Var edomIff not_up_less_UU)
 next
   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]])
 qed
+thm  edom_mono[OF Aexp_IfThenElse, no_vars]
+sublocale CardinalityPrognosisIfThenElse prognosis
+proof default
+  case goal1
+  have "edom (Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a) \<subseteq> edom (Aexp (scrut ? e1 : e2)\<cdot>a)"
+    by (rule edom_mono[OF Aexp_IfThenElse])
+  thus ?case
+    by (auto intro!: env_restr_mono2)
+next
+  case goal2
+  show ?case by (auto intro!: env_restr_mono2)
+qed
+
   
 sublocale CardinalityPrognosisLet prognosis  cHeap Aheap
 proof
@@ -135,13 +158,13 @@ proof
   also have "\<dots> = edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
     by auto
   finally
-  have "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a)".
-  hence "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<union> ap S \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a) \<union> ap S" by auto
+  have "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)".
+  hence "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<union> edom (AEstack as S) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a) \<union> edom (AEstack as S)" by auto
   thus ?case by (simp add: ae2ce_to_env_restr env_restr_join2 Un_assoc[symmetric] env_restr_mono2)
 qed
 
 sublocale CardinalityPrognosisEdom prognosis
-  by default (auto dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF edom_AnalBinds])
+  by default (auto dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF edom_AnalBinds]  set_mp[OF edom_AEstack])
 
 
 sublocale CardinalityPrognosisCorrect prognosis cHeap Aheap Aexp..
index f17b50d..bb93a19 100644 (file)
@@ -23,6 +23,7 @@ lemma supp_Arg[simp]: "supp (Arg v) = supp v"  unfolding supp_def by auto
 lemma supp_Upd[simp]: "supp (Upd v) = supp v"  unfolding supp_def by auto
 lemma supp_Dummy[simp]: "supp (Dummy v) = supp v"  unfolding supp_def by auto
 lemma fresh_Alts[simp]: "a \<sharp> Alts e1 e2 = (a \<sharp> e1 \<and> a \<sharp> e2)" unfolding fresh_def by auto
+lemma fresh_star_Alts[simp]: "a \<sharp>* Alts e1 e2 = (a \<sharp>* e1 \<and> a \<sharp>* e2)" unfolding fresh_star_def by auto
 lemma fresh_Arg[simp]: "a \<sharp> Arg v = a \<sharp> v" unfolding fresh_def by auto
 lemma fresh_Upd[simp]: "a \<sharp> Upd v = a \<sharp> v" unfolding fresh_def by auto
 lemma fresh_Dummy[simp]: "a \<sharp> Dummy v = a \<sharp> v" unfolding fresh_def by auto
index 1fef809..c30807d 100644 (file)
@@ -75,5 +75,10 @@ proof-
   thus ?thesis..
 qed
 
+lemma diff_cont[THEN cont_compose, simp, cont2cont]:
+  fixes S' :: "'a set"
+  shows  "cont (\<lambda>S. S - S')"
+by (rule set_set_contI) simp
+
 
 end
index 47f3012..c5f9d8c 100644 (file)
@@ -105,6 +105,12 @@ begin
   unfolding map_transform_def
      by (induction \<Gamma>) (auto simp add: supp_Pair supp_Cons dest!: set_mp[OF supp_lift_transform])
 
+  lemma fresh_transform[intro]: "a \<sharp> e \<Longrightarrow> a \<sharp> trans n e"
+    by (auto simp add: fresh_def) (auto dest!: set_mp[OF supp_trans])
+
+  lemma fresh_star_transform[intro]: "a \<sharp>* e \<Longrightarrow> a \<sharp>* trans n e"
+    by (auto simp add: fresh_star_def)
+
   lemma fresh_map_transform[intro]: "a \<sharp> \<Gamma> \<Longrightarrow> a \<sharp> map_transform trans ae \<Gamma>"
     unfolding fresh_def using supp_map_transform by auto