Use isVal everywhere
authorJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 15:10:17 +0000 (15:10 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Thu, 15 Jan 2015 15:10:17 +0000 (15:10 +0000)
28 files changed:
Launchbury/AbstractTransform.thy
Launchbury/ArityEtaExpandCorrect.thy
Launchbury/ArityStack.thy
Launchbury/CallArityCorrectEnd2End.thy
Launchbury/CallArityEnd2End.thy
Launchbury/CardinalityAnalysisSpec.thy
Launchbury/CardinalityEtaExpandCorrect.thy
Launchbury/CoCallAnalysisBinds.thy
Launchbury/CoCallAnalysisImpl.thy
Launchbury/CoCallAnalysisSpec.thy
Launchbury/CoCallFix.thy
Launchbury/CoCallGraph.thy
Launchbury/CoCallImplCorrect.thy
Launchbury/CoCallImplFTreeCorrect.thy
Launchbury/DeadCodeRemoval2Correct.thy
Launchbury/DeadCodeRemoval2CorrectSestoft.thy
Launchbury/EtaExpansion.thy
Launchbury/EtaExpansionArity.thy
Launchbury/EtaExpansionSestoft.thy
Launchbury/FTreeAnalysisSpec.thy
Launchbury/FTreeImplCardinality.thy
Launchbury/FTreeImplCardinalityCorrect.thy
Launchbury/Nominal-Utils.thy
Launchbury/Sestoft.thy
Launchbury/SestoftConf.thy
Launchbury/SestoftCorrect.thy
Launchbury/Substitution.thy
Launchbury/Terms.thy

index 7391d5b..c5d9621 100644 (file)
@@ -190,6 +190,10 @@ begin
   lemma isLam_transform[simp]:
     "isLam (transform a e) \<longleftrightarrow> isLam e"
     by (induction e rule:isLam.induct) auto
+
+  lemma isVal_transform[simp]:
+    "isVal (transform a e) \<longleftrightarrow> isVal e"
+    by (induction e rule:isLam.induct) auto
 end
 
 locale AbstractTransformBoundSubst = AbstractAnalPropSubst + AbstractTransformBound + 
index d0c0176..74cc60e 100644 (file)
@@ -102,7 +102,7 @@ case (thunk \<Gamma> x e S)
   from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0`
   have "map_of (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)) x = Some (transform 0 e)"
     by (simp add: map_of_map_transform)
-  with `\<not> isLam e`
+  with `\<not> isVal e`
   have "conf_transform (ae, a) (\<Gamma>, Var x, S) \<Rightarrow> conf_transform (ae, 0) (delete x \<Gamma>, e, Upd x # S)"
     by (auto simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
   ultimately
@@ -128,11 +128,11 @@ case (lamvar \<Gamma> x e S)
   have "Astack S \<sqsubseteq> u" using lamvar  below_trans[OF _ `a \<sqsubseteq> u`] by auto
 
   {
-  from `isLam e`
-  have "isLam (transform u e)" by simp
-  hence "isLam (Aeta_expand u (transform u e))" by (rule isLam_Aeta_expand)
+  from `isVal e`
+  have "isVal (transform u e)" by simp
+  hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
   moreover
-  from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u`  `isLam (transform u e)`
+  from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u`  `isVal (transform u e)`
   have "map_of (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)) x = Some (Aeta_expand u (transform u e))"
     by (simp add: map_of_map_transform)
   ultimately
@@ -140,7 +140,7 @@ case (lamvar \<Gamma> x e S)
         ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>)), Aeta_expand u  (transform u e), S)"
      by (auto intro: lambda_var simp add: map_transform_delete simp del: restr_delete)
   also have "\<dots> = ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x \<Gamma>))), Aeta_expand u (transform u e), S)"
-    using `ae x = up \<cdot> u` `isLam (transform u e)`
+    using `ae x = up \<cdot> u` `isVal (transform u e)`
     by (simp add: map_transform_Cons map_transform_delete restr_delete_twist del: restr_delete)
   also(subst[rotated]) have "\<dots> \<Rightarrow>\<^sup>* conf_transform (ae, u) ((x, e) # delete x \<Gamma>, e, S)"
     by simp (rule Aeta_expand_correct[OF `Astack S \<sqsubseteq> u`])
index 49c9347..ef80f50 100644 (file)
@@ -5,6 +5,7 @@ begin
 fun Astack :: "stack \<Rightarrow> Arity"
   where "Astack [] = 0"
       | "Astack (Arg x # S) = inc\<cdot>(Astack S)"
+      | "Astack (Alts e1 e2 # S) = 0"
       | "Astack (Upd x # S) = 0"
       | "Astack (Dummy x # S) = 0"
 
index 4ac5bc8..151693e 100644 (file)
@@ -56,7 +56,7 @@ lemma example1:
   assumes Aexp_e: "\<And>a. Aexp e\<cdot>a = esing x\<cdot>(up\<cdot>a) \<squnion> esing y\<cdot>(up\<cdot>a)"
   assumes ccExp_e: "\<And>a. CCexp e\<cdot>a = \<bottom>"
   assumes [simp]: "transform 1 e = e"
-  assumes "isLam e"
+  assumes "isVal e"
   assumes disj: "y \<noteq> f" "y \<noteq> g" "x \<noteq> y" "z \<noteq> f" "z \<noteq> g" "y \<noteq> x"
   assumes fresh: "atom z \<sharp> e"
   shows "transform 1 (let y be  App (Var f) g in (let x be e in (Var x))) = 
@@ -68,7 +68,7 @@ proof-
   hence [simp]: "\<not> nonrec [(x,e)]"
     by (simp add: nonrec_def)
  
-  from `isLam e`
+  from `isVal e`
   have [simp]: "thunks [(x, e)] = {}"
     by (simp add: thunks_Cons)
 
index a994a5e..39c67e2 100644 (file)
@@ -15,7 +15,7 @@ lemma example1:
   assumes Aexp_e: "\<And>a. Aexp e\<cdot>a = esing x\<cdot>(up\<cdot>a) \<squnion> esing y\<cdot>(up\<cdot>a)"
   assumes ccExp_e: "\<And>a. CCexp e\<cdot>a = \<bottom>"
   assumes [simp]: "transform 1 e = e"
-  assumes "isLam e"
+  assumes "isVal e"
   assumes disj: "y \<noteq> f" "y \<noteq> g" "x \<noteq> y" "z \<noteq> f" "z \<noteq> g" "y \<noteq> x"
   assumes fresh: "atom z \<sharp> e"
   shows "transform 1 (let y be  App (Var f) g in (let x be e in (Var x))) = 
@@ -27,7 +27,7 @@ proof-
   hence [simp]: "\<not> nonrec [(x,e)]"
     by (simp add: nonrec_def)
  
-  from `isLam e`
+  from `isVal e`
   have [simp]: "thunks [(x, e)] = {}"
     by (simp add: thunks_Cons)
 
index 1d2ee44..2cfe496 100644 (file)
@@ -22,9 +22,9 @@ locale CardinalityPrognosisLam = CardinalityPrognosis +
   assumes prognosis_subst_Lam: "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae a (\<Gamma>, Lam [y]. e, Arg x # S)"
 
 locale CardinalityPrognosisVar = CardinalityPrognosis +
-  assumes prognosis_Var_lam: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> isLam e \<Longrightarrow> prognosis ae u (\<Gamma>, e, S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-  assumes prognosis_Var_thunk: "map_of \<Gamma> x = Some e \<Longrightarrow> ae x = up\<cdot>u \<Longrightarrow> \<not> isLam e \<Longrightarrow> prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-  assumes prognosis_Var2: "isLam e \<Longrightarrow> x \<notin> domA \<Gamma> \<Longrightarrow> prognosis ae 0 ((x, e) # \<Gamma>, e, S) \<sqsubseteq> prognosis ae 0 (\<Gamma>, e, Upd x # S)"
+  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)"
 
 locale CardinalityPrognosisLet = CardinalityPrognosis + CardinalityHeap + ArityAnalysisHeap +
   assumes prognosis_Let:
index a68ccef..8547c54 100644 (file)
@@ -146,7 +146,7 @@ begin
       hence "x \<notin> ap S" using prognosis_ap[of ae a \<Gamma> "(Var x)" S] by auto
       
   
-      from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isLam e`
+      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))"
         by (rule prognosis_Var_thunk)
   
@@ -214,7 +214,7 @@ begin
     next
       case many
   
-      from `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `\<not> isLam e`
+      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))"
         by (rule prognosis_Var_thunk)
       also note record_call_below_arg
@@ -235,7 +235,7 @@ begin
       from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0` many
       have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae \<Gamma>)) x = Some (transform 0 e)"
         by (simp add: map_of_map_transform)
-      with `\<not> isLam e`
+      with `\<not> isVal e`
       have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0) (delete x \<Gamma>, e, Upd x # S)"
         by (auto simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
       ultimately
@@ -265,7 +265,7 @@ begin
     have "prognosis ae u ((x, e) # delete x \<Gamma>, e, S) = prognosis ae u (\<Gamma>, e, S)"
       using `map_of \<Gamma> x = Some e` by (auto intro!: prognosis_reorder)
     also have "\<dots> \<sqsubseteq> record_call x \<cdot> (prognosis ae a (\<Gamma>, Var x, S))"
-       using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` `isLam e`  by (rule prognosis_Var_lam)
+       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
   
@@ -277,11 +277,11 @@ begin
     have "Astack (restr_stack (edom ce) S) \<sqsubseteq> u" using lamvar below_trans[OF _ `a \<sqsubseteq> u`] by auto
   
     {
-    from `isLam e`
-    have "isLam (transform u e)" by simp
-    hence "isLam (Aeta_expand u (transform u e))" by (rule isLam_Aeta_expand)
+    from `isVal e`
+    have "isVal (transform u e)" by simp
+    hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
     moreover
-    from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isLam (transform u e)`
+    from  `map_of \<Gamma> x = Some e`  `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isVal (transform u e)`
     have "map_of (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))) x = Some (Aeta_expand u (transform u e))"
       by (simp add: map_of_map_transform)
     ultimately
@@ -289,7 +289,7 @@ begin
           ((x, Aeta_expand u (transform u e)) # delete x (restrictA (edom ce) (map_transform Aeta_expand ae (map_transform transform ae \<Gamma>))), Aeta_expand u  (transform u e), restr_stack (edom ce) S)"
        by (auto intro: lambda_var simp add: map_transform_delete simp del: restr_delete)
     also have "\<dots> = (restrictA (edom ce) ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x \<Gamma>)))), Aeta_expand u  (transform u e), restr_stack (edom ce) S)"
-      using `ae x = up \<cdot> u` `ce x = up\<cdot>c` `isLam (transform u e)`
+      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) ((x, e) # delete x \<Gamma>, e, S)"
       by simp (rule Aeta_expand_correct[OF `Astack (restr_stack (edom ce) S) \<sqsubseteq> u`])
@@ -310,7 +310,7 @@ begin
       have "Astack (Upd x # S) \<sqsubseteq> a" using var\<^sub>2 by auto
       hence "a = 0" by auto
   
-      from `isLam e` `x \<notin> domA \<Gamma>`
+      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 "consistent (ae, ce, 0) ((x, e) # \<Gamma>, e, S)"
index 5a5fcc2..b763eb0 100644 (file)
@@ -5,10 +5,10 @@ begin
 context CoCallAnalysis
 begin
 definition ccBind :: "var \<Rightarrow> exp \<Rightarrow> ((AEnv \<times> CoCalls) \<rightarrow> CoCalls)"
-  where "ccBind v e = (\<Lambda> (ae, G).  if (v--v\<notin>G) \<or> \<not> isLam e then cc_restr (fv e) (fup\<cdot>(ccExp e)\<cdot>(ae v)) else ccSquare (fv e))"
+  where "ccBind v e = (\<Lambda> (ae, G).  if (v--v\<notin>G) \<or> \<not> isVal e then cc_restr (fv e) (fup\<cdot>(ccExp e)\<cdot>(ae v)) else ccSquare (fv e))"
 (* paper has:  \<or> ae v = up\<cdot>0, but that is not monotone! But should give the same result. *)
 
-lemma ccBind_eq: "ccBind v e \<cdot> (ae, G) = (if (v--v\<notin>G) \<or> \<not> isLam e then cc_restr (fv e) (fup\<cdot>(ccExp e)\<cdot>(ae v)) else ccSquare (fv e))"
+lemma ccBind_eq: "ccBind v e \<cdot> (ae, G) = (if (v--v\<notin>G) \<or> \<not> isVal e then cc_restr (fv e) (fup\<cdot>(ccExp e)\<cdot>(ae v)) else ccSquare (fv e))"
   unfolding ccBind_def
   apply (rule cfun_beta_Pair)
   apply (rule cont_if_else_above)
index 35760a8..77c9881 100644 (file)
@@ -168,7 +168,7 @@ lemma CCexp_simps[simp]:
   "CCexp (App e x)\<cdot>n = CCexp e\<cdot>(inc\<cdot>n) \<squnion> ccProd {x} (insert x (fv e))"
   "\<not> nonrec \<Gamma> \<Longrightarrow> CCexp (Let \<Gamma> e)\<cdot>n = cc_restr (fv (Let \<Gamma> e)) (CCfix \<Gamma>\<cdot>(Afix \<Gamma>\<cdot>(Aexp e\<cdot>n  \<squnion> (\<lambda>_.up\<cdot>0) f|` (thunks \<Gamma>)), CCexp e\<cdot>n))"
   "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 isLam e then {} else {x})) \<squnion> CCexp 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 Null\<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)+
index 675dcb6..e4c9500 100644 (file)
@@ -10,7 +10,7 @@ locale CoCallArityCorrect = CoCallArity + CoCallAnalyisHeap + CorrectArityAnalys
   assumes ccExp_App: "ccExp e\<cdot>(inc\<cdot>a) \<squnion> ccProd {x} (insert x (fv e)) \<sqsubseteq> ccExp (App e x)\<cdot>a"
   assumes ccExp_Lam: "cc_restr (fv (Lam [y]. e)) (ccExp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> ccExp (Lam [y]. e)\<cdot>n"
   assumes ccExp_subst: "x \<notin>  S \<Longrightarrow> y \<notin> S \<Longrightarrow> cc_restr S (ccExp e[y::=x]\<cdot>a) \<sqsubseteq> cc_restr S (ccExp e\<cdot>a)"
-  assumes ccExp_pap: "isLam e \<Longrightarrow> ccExp e\<cdot>0 = ccSquare (fv e)"
+  assumes ccExp_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 ccHeap_Exp: "ccExp e\<cdot>a \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
index c821f66..c343759 100644 (file)
@@ -163,10 +163,10 @@ subsubsection {* The non-recursive case *}
 
 definition ABind_nonrec :: "var \<Rightarrow> exp \<Rightarrow> AEnv \<times> CoCalls \<rightarrow> Arity\<^sub>\<bottom>"
 where
-  "ABind_nonrec x e = (\<Lambda> i. (if isLam e \<or> x--x\<notin>(snd i) then fst i x else up\<cdot>0))"
+  "ABind_nonrec x e = (\<Lambda> i. (if isVal e \<or> x--x\<notin>(snd i) then fst i x else up\<cdot>0))"
 
 lemma ABind_nonrec_eq:
-  "ABind_nonrec x e \<cdot> i = (if isLam e \<or> x--x\<notin>(snd i) then fst i x else up\<cdot>0)"
+  "ABind_nonrec x e \<cdot> i = (if isVal e \<or> x--x\<notin>(snd i) then fst i x else up\<cdot>0)"
   unfolding ABind_nonrec_def
   apply (rule beta_cfun)
   apply (rule cont_if_else_above)
@@ -212,10 +212,10 @@ begin
     by (rule beta_cfun) simp
 
   definition CCfix_nonrec
-   where "CCfix_nonrec x e = (\<Lambda> i. ccBind x e \<cdot> (Aheap_nonrec x e\<cdot>i, snd i)  \<squnion> ccProd (fv e) (ccNeighbors x (snd i) - (if isLam e then {} else {x})) \<squnion> snd i)"
+   where "CCfix_nonrec x e = (\<Lambda> i. ccBind x e \<cdot> (Aheap_nonrec x e\<cdot>i, snd i)  \<squnion> ccProd (fv e) (ccNeighbors x (snd i) - (if isVal e then {} else {x})) \<squnion> snd i)"
 
   lemma CCfix_nonrec_eq[simp]:
-    "CCfix_nonrec x e \<cdot> i = ccBind x e\<cdot>(Aheap_nonrec x e\<cdot>i, snd i)  \<squnion> ccProd (fv e) (ccNeighbors x (snd i) - (if isLam e then {} else {x})) \<squnion> snd i"
+    "CCfix_nonrec x e \<cdot> i = ccBind x e\<cdot>(Aheap_nonrec x e\<cdot>i, snd i)  \<squnion> ccProd (fv e) (ccNeighbors x (snd i) - (if isVal e then {} else {x})) \<squnion> snd i"
     unfolding CCfix_nonrec_def
     by (rule beta_cfun) (intro cont2cont)
 
index 3e7a85d..8380dc0 100644 (file)
@@ -281,6 +281,9 @@ lemma below_ccSquare[iff]: "G \<sqsubseteq> ccSquare S  \<longleftrightarrow> cc
 lemma cc_restr_ccSquare[simp]: "cc_restr S (ccSquare S') = ccSquare (S' \<inter> S)"
   unfolding ccSquare_def by auto
 
+lemma ccSquare_empty[simp]: "ccSquare {} = \<bottom>"
+  unfolding ccSquare_def by simp
+
 lift_definition ccNeighbors :: "var \<Rightarrow> CoCalls \<Rightarrow> var set" 
   is "\<lambda> x G. {y .(y,x) \<in> G \<or> (x,y) \<in> G}".
 
index 98b077d..c6b5e5e 100644 (file)
@@ -25,7 +25,7 @@ lemma CCexp_Let_simp1[simp]:
   by (rule cc_restr_intersect)  (auto dest!: set_mp[OF ccField_CCfix])
 
 lemma CCexp_Let_simp2[simp]:
-  "atom x \<sharp> e \<Longrightarrow> CCexp (let x be e in exp)\<cdot>n = cc_restr (- {x}) (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 isLam e then {} else {x})) \<squnion> CCexp exp\<cdot>n)"
+  "atom x \<sharp> e \<Longrightarrow> CCexp (let x be e in exp)\<cdot>n = cc_restr (- {x}) (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)"
   unfolding CCexp_simps
   by (rule cc_restr_intersect)
      (auto simp add: ccField_ccProd ccBind_eq dest!: set_mp[OF ccField_CCexp]  set_mp[OF ccField_fup_CCexp] set_mp[OF ccField_cc_restr] set_mp[OF ccNeighbors_ccField])
@@ -322,9 +322,9 @@ next
     by (rule eq_imp_below[OF CCexp_subst])
 next
   fix e
-  assume "isLam e"
-  thus "CCexp  e\<cdot>0 = ccSquare (fv e)"
-    by (induction e rule: isLam.induct) (auto simp add: predCC_eq)
+  assume "isVal e"
+  thus "CCexp e\<cdot>0 = ccSquare (fv e)"
+    by (induction e rule: isVal.induct) (auto simp add: predCC_eq)
 next
   fix \<Gamma> e a
   show "cc_restr (- domA \<Gamma>) (ccHeap \<Gamma> e\<cdot>a) \<sqsubseteq> CCexp (Let \<Gamma> e)\<cdot>a"
@@ -374,7 +374,7 @@ next
     hence [simp]: "x \<notin> fv e'" by (auto simp add: fresh_def fv_def)
 
     show ?thesis
-    proof(cases "x--x\<notin>CCexp e\<cdot>a \<or> isLam e'")
+    proof(cases "x--x\<notin>CCexp e\<cdot>a \<or> isVal e'")
       case True
       with `(Aheap \<Delta> e\<cdot>a) x = up\<cdot>a'`
       have [simp]: "(CoCallArityAnalysis.Aexp cCCexp e\<cdot>a) x = up\<cdot>a'"
@@ -422,20 +422,20 @@ next
      by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp])
 
     show ?thesis
-    proof(cases "isLam e' \<and> x--x\<in>CCexp e\<cdot>a")
+    proof(cases "isVal e' \<and> x--x\<in>CCexp e\<cdot>a")
     case True
 
     have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a) =
         ccNeighbors x (ccBind x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) \<union>
-        ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x}))) \<union>
+        ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isVal e' then {} else {x}))) \<union>
         ccNeighbors x (CCexp e\<cdot>a)" by (auto simp add: ccHeap_simp2 )
     also have "ccNeighbors x (ccBind  x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) = {}"
        by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp])
-    also have "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x})))
+    also have "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isVal e' then {} else {x})))
       \<subseteq> ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a)))" by (simp add: ccNeighbors_ccProd)
     also have "\<dots> \<subseteq> fv e'" by (simp add: ccNeighbors_ccProd)
     finally
-    have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a)  - {x} \<inter> thunks \<Delta> \<subseteq> ccNeighbors x (CCexp e\<cdot>a) \<union> fv e'" by auto
+    have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta> \<subseteq> ccNeighbors x (CCexp e\<cdot>a) \<union> fv e'" by auto
     hence "ccProd (fv e') (ccNeighbors x (ccHeap \<Delta> e\<cdot>a) - {x} \<inter> thunks \<Delta>) \<sqsubseteq> ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) \<union> fv e')" by (rule ccProd_mono2)
     also have "\<dots> \<sqsubseteq> ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a)) \<squnion> ccProd (fv e') (fv e')" by simp
     also have "ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a)) \<sqsubseteq> ccHeap \<Delta> e\<cdot>a"
@@ -451,11 +451,11 @@ next
     case False
     have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a) =
         ccNeighbors x (ccBind x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) \<union>
-        ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x}))) \<union>
+        ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isVal e' then {} else {x}))) \<union>
         ccNeighbors x (CCexp e\<cdot>a)" by (auto simp add: ccHeap_simp2 )
     also have "ccNeighbors x (ccBind  x e'\<cdot>(Aheap_nonrec x e'\<cdot>(Aexp e\<cdot>a, CCexp e\<cdot>a), CCexp e\<cdot>a)) = {}"
        by (auto simp add: ccBind_eq dest!: set_mp[OF ccField_cc_restr] set_mp[OF ccField_fup_CCexp])
-    also have  "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isLam e' then {} else {x}) )) 
+    also have  "ccNeighbors x (ccProd (fv e') (ccNeighbors x (CCexp e\<cdot>a) - (if isVal e' then {} else {x}) )) 
       = {}" using False by (auto simp add: ccNeighbors_ccProd)
     finally
     have "ccNeighbors x (ccHeap \<Delta> e\<cdot>a) \<subseteq> ccNeighbors x (CCexp e\<cdot>a)" by auto
@@ -485,7 +485,7 @@ next
   assume "nonrec \<Gamma>"
   then obtain x' e' where [simp]: "\<Gamma> = [(x',e')]" "atom x' \<sharp> e'" by (auto elim: nonrecE)
   assume "x \<in> thunks \<Gamma>"
-  hence [simp]: "x = x'" "\<not> isLam e'" by (auto simp add: thunks_Cons split: if_splits)
+  hence [simp]: "x = x'" "\<not> isVal e'" by (auto simp add: thunks_Cons split: if_splits)
 
   assume "x \<in> ccManyCalls (CCexp e\<cdot>a)"
   hence [simp]: "x'--x'\<in> CCexp  e\<cdot>a" by simp
index f76973c..c5a67ca 100644 (file)
@@ -144,7 +144,7 @@ next
     unfolding Fexp_simp by (auto intro: single_below)
 next
   fix e
-  assume "isLam e"
+  assume "isVal e"
   hence [simp]: "ccExp e\<cdot>0 = ccSquare (fv e)" by (rule ccExp_pap)
   thus "repeatable (Fexp e\<cdot>0)"
     unfolding Fexp_simp by (auto intro: repeatable_ccFTree_ccSquare[OF Aexp_edom])
index 1b515eb..6b3ed1f 100644 (file)
@@ -20,9 +20,6 @@ lemma delete_rdcH[simp]: "delete x (rdcH S \<Gamma>) = rdcH S (delete x \<Gamma>
   by (induction \<Gamma> rule:clearjunk.induct) 
      (auto simp add: rdcH_def  delete_twist split: if_splits)
 
-lemma map_ran_append[simp]: "map_ran f (\<Gamma>1 @ \<Gamma>2) = map_ran f \<Gamma>1 @ map_ran f \<Gamma>2"
-  by (induction \<Gamma>1) auto
-
 lemma restrictA_UNIV[simp]: "restrictA UNIV \<Gamma> = \<Gamma>"
   by (induction \<Gamma>) auto
 
@@ -35,11 +32,8 @@ lemma clearjunk_append: "clearjunk (\<Gamma>1 @ \<Gamma>2) = clearjunk \<Gamma>1
 lemma restrictA_clearjunk: "restrictA S (clearjunk \<Gamma>) = clearjunk (restrictA S \<Gamma>)"
   by (induction \<Gamma>  rule:clearjunk.induct) (auto simp add: Compl_insert)
 
-lemma restrictA_append[simp]: "restrictA S (\<Gamma>1 @ \<Gamma>2) = restrictA S \<Gamma>1 @ restrictA S \<Gamma>2"
-  by (induction \<Gamma>1) auto
-
 lemma rdcH_append[simp]: "domA as \<inter> domA \<Gamma> = {} \<Longrightarrow> rdcH S (as @ \<Gamma>) = rdcH S as @ rdcH S \<Gamma>"
-  unfolding rdcH_def apply (simp add: clearjunk_append restrictA_clearjunk)
+  unfolding rdcH_def apply (simp add: clearjunk_append restrictA_clearjunk map_ran_append restrictA_append)
   apply (rule arg_cong) back
   apply (rule restrictA_cong)
   apply auto
index 0835c40..4b07774 100644 (file)
@@ -5,6 +5,9 @@ begin
 lemma isLam_remove_dead_code[simp]: "isLam e \<Longrightarrow> isLam (remove_dead_code e)"
   by (induction e rule:isLam.induct) auto
 
+lemma isVal_remove_dead_code[simp]: "isVal e \<Longrightarrow> isVal (remove_dead_code e)"
+  by (induction e rule:isLam.induct) auto
+
 definition rdcH :: "var set \<Rightarrow> heap \<Rightarrow> heap"
   where "rdcH S \<Gamma> = restrictA (-S) (clearjunk (map_ran (\<lambda> _ e . remove_dead_code e) \<Gamma>))" 
 
@@ -195,7 +198,7 @@ proof(rule dc_rel_elim)
     with `x \<notin> domA \<Gamma>`
     have  "rdcH V ((x, z) # \<Gamma>) = (x,remove_dead_code z) # rdcH V \<Gamma>" by simp
 
-    note `x \<notin> domA \<Gamma>` [simp] and `isLam e` [simp]
+    note `x \<notin> domA \<Gamma>` [simp] and `isVal e` [simp]
 
 
     from V\<^sub>1 V\<^sub>2
index e6d2b6a..9d07c79 100644 (file)
@@ -67,5 +67,9 @@ lemma isLam_eta_expand:
   "isLam e \<Longrightarrow> isLam (eta_expand n e)" and "n > 0 \<Longrightarrow> isLam (eta_expand n e)"
 by (induction n) auto
 
+lemma isVal_eta_expand:
+  "isVal e \<Longrightarrow> isVal (eta_expand n e)" and "n > 0 \<Longrightarrow> isVal (eta_expand n e)"
+by (induction n) auto
+
 
 end
index 97e2315..5b773ea 100644 (file)
@@ -25,6 +25,9 @@ lemma subst_Aeta_expand:
 lemma isLam_Aeta_expand: "isLam e \<Longrightarrow> isLam (Aeta_expand a e)"
   by transfer (rule isLam_eta_expand)
 
+lemma isVal_Aeta_expand: "isVal e \<Longrightarrow> isVal (Aeta_expand a e)"
+  by transfer (rule isVal_eta_expand)
+
 lemma Aeta_expand_fresh[simp]: "a \<sharp> Aeta_expand n e = a \<sharp> e" by transfer simp
 lemma Aeta_expand_fresh_star[simp]: "a \<sharp>* Aeta_expand n e = a \<sharp>* e" by (auto simp add: fresh_star_def)
 
index 56f3a0a..0677d20 100644 (file)
@@ -25,6 +25,7 @@ qed
 fun arg_prefix :: "stack \<Rightarrow> nat" where
   "arg_prefix [] = 0"
 | "arg_prefix (Arg x # S) = Suc (arg_prefix S)"
+| "arg_prefix (Alts e1 e2 # S) = 0"
 | "arg_prefix (Upd x # S) = 0"
 | "arg_prefix (Dummy x # S) = 0"
 
@@ -63,7 +64,7 @@ theorem bound_eta_expansion_correct:
   fixes exp :: "var \<Rightarrow> nat"
   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S')"
   assumes "\<not> boring_step (\<Delta>, z, S')"
-  assumes "\<And> x e'. e = Var x \<Longrightarrow> map_of \<Gamma> x = Some e' \<Longrightarrow> (if isLam e' then exp x \<le> arg_prefix S else exp x = 0)"
+  assumes "\<And> x e'. e = Var x \<Longrightarrow> map_of \<Gamma> x = Some e' \<Longrightarrow> (if isVal e' then exp x \<le> arg_prefix S else exp x = 0)"
   assumes "exp ` (- domA \<Gamma>) \<subseteq> {0}"
   shows "(eta_expand_heap exp \<Gamma>, e, S) \<Rightarrow>\<^sup>* (eta_expand_heap exp \<Delta>, z, S')"
 using assms
@@ -95,7 +96,7 @@ case (lamvar \<Gamma> x e S)
     by (rule step.var\<^sub>1)
   hence "(eta_expand_heap exp \<Gamma>, Var x, S) \<Rightarrow>\<^sup>* (delete x (eta_expand_heap exp \<Gamma>), eta_expand (exp x) e, Upd x # S)"..
   also have "\<dots> \<Rightarrow> ((x, eta_expand (exp x) e) # delete x (eta_expand_heap exp \<Gamma>), eta_expand (exp x) e, S)"
-    using isLam_eta_expand(1)[OF `isLam _`] by (auto intro: var\<^sub>2)
+    using isVal_eta_expand(1)[OF `isVal _`] by (auto intro: var\<^sub>2)
   also have "\<dots> \<Rightarrow>\<^sup>* ((x, eta_expand (exp x) e) # delete x (eta_expand_heap exp \<Gamma>), e, S)"
      by (rule eta_expansion_correct') fact
   also have "delete x (eta_expand_heap exp \<Gamma>) = eta_expand_heap exp (delete x \<Gamma>)" 
index 58e5783..0937e8d 100644 (file)
@@ -12,7 +12,7 @@ locale FTreeAnalysisCorrect = FTreeAnalysisCarrier +
   assumes Fexp_Lam: "without y (Fexp e\<cdot>(pred\<cdot>n)) \<sqsubseteq> Fexp (Lam [y]. e) \<cdot> n"
   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: "isLam e \<Longrightarrow> repeatable (Fexp e\<cdot>0)"
+  assumes Fun_repeatable: "isVal e \<Longrightarrow> repeatable (Fexp e\<cdot>0)"
 
 locale FTreeAnalysisCardinalityHeap = 
   FTreeAnalysisCorrect + CorrectArityAnalysisLet + 
index 8e6cca3..75b1827 100644 (file)
@@ -9,12 +9,14 @@ begin
 
 fun unstack :: "stack \<Rightarrow> exp \<Rightarrow> exp" where
   "unstack [] e = e"
+| "unstack (Alts e1 e2 # S) e = unstack S e"
 | "unstack (Upd x # S) e = unstack S e"
 | "unstack (Arg x # S) e = unstack S (App e x)"
 | "unstack (Dummy x # S) e = unstack S e"
 
 fun Fstack :: "stack \<Rightarrow> var ftree"
   where "Fstack [] = \<bottom>"
+  | "Fstack (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"
index 2444a0b..86a366b 100644 (file)
@@ -135,7 +135,7 @@ begin
     have "\<dots> = record_call x\<cdot>(pathsCard (paths (and_then x (substitute (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) (Fstack S  \<otimes>\<otimes> (FBinds \<Gamma>\<cdot>ae) x)))))"
       using `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` by (simp add: Fexp.AnalBinds_lookup)
     also
-    assume "isLam e"
+    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))"
@@ -154,7 +154,7 @@ begin
     fix \<Gamma> :: heap and e :: exp and x :: var and ae :: AEnv and u a S
     assume "map_of \<Gamma> x = Some e"
     assume "ae x = up\<cdot>u"
-    assume "\<not> isLam e"
+    assume "\<not> isVal e"
     hence "x \<in> thunks \<Gamma>" using `map_of \<Gamma> x = Some e` by (metis thunksI)
     hence [simp]: "f_nxt (FBinds \<Gamma>\<cdot>ae) (thunks \<Gamma>) x = FBinds (delete x \<Gamma>)\<cdot>ae" 
       by (auto simp add: f_nxt_def Fexp.AnalBinds_delete_to_fun_upd empty_is_bottom)
@@ -189,13 +189,13 @@ begin
     thus "prognosis ae u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> record_call x\<cdot>(prognosis ae a (\<Gamma>, Var x, S))" by simp
   next
     fix \<Gamma> :: heap and e :: exp and ae :: AEnv and  x :: var and  S
-    assume "isLam e"
+    assume "isVal e"
     hence "repeatable (Fexp e\<cdot>0)" by (rule Fun_repeatable)
 
     assume [simp]: "x \<notin> domA \<Gamma>"
 
     have [simp]: "thunks ((x, e) # \<Gamma>) = thunks \<Gamma>" 
-      using `isLam e`
+      using `isVal e`
       by (auto simp add: thunks_Cons dest: set_mp[OF thunks_domA])
 
     have "fup\<cdot>(Fexp e)\<cdot>(ae x) \<sqsubseteq> Fexp e\<cdot>0" by (metis fup2 monofun_cfun_arg up_zero_top)
index c4f5995..b71aa72 100644 (file)
@@ -313,6 +313,41 @@ lemma fresh_fv: "finite (fv e :: 'a set) \<Longrightarrow>  atom (x :: ('a::at_b
   unfolding fv_def fresh_def
   by (auto simp add: supp_finite_set_at_base)
 
+lemma finite_fv[simp]: "finite (fv (e::'a::fs) :: ('b::at_base) set)"
+proof-
+  have "finite (supp e)" by (metis finite_supp)
+  hence "finite (atom -` supp e :: 'b set)" 
+    apply (rule finite_vimageI)
+    apply (rule inj_onI)
+    apply (simp)
+    done
+  moreover
+  have "(atom -` supp e  :: 'b set) = fv e"   unfolding fv_def by auto
+  ultimately
+  show ?thesis by simp
+qed
+
+definition fv_list :: "'a::fs \<Rightarrow> 'b::at_base list"
+  where "fv_list e = (SOME l. set l = fv e)"
+
+lemma set_fv_list[simp]: "set (fv_list e) = (fv e :: ('b::at_base) set)"
+proof-
+  have "finite (fv e :: 'b set)" by (rule finite_fv)
+  from finite_list[OF finite_fv]
+  obtain l where "set l = (fv e :: 'b set)"..
+  thus ?thesis
+    unfolding fv_list_def by (rule someI)
+qed
+
+lemma fresh_fv_list[simp]:
+  "a \<sharp> (fv_list e :: 'b::at_base list) \<longleftrightarrow> a \<sharp> (fv e :: 'b::at_base set)"
+proof-
+  have "a \<sharp> (fv_list e :: 'b::at_base list) \<longleftrightarrow> a \<sharp> set (fv_list e :: 'b::at_base list)"
+    by (rule fresh_set[symmetric])
+  also have "\<dots> \<longleftrightarrow> a \<sharp> (fv e :: 'b::at_base set)" by simp
+  finally show ?thesis.
+qed
+
 
 subsubsection {* Other useful lemmas *}
 
index 1ca806a..deaa637 100644 (file)
@@ -6,8 +6,9 @@ inductive step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightar
   app\<^sub>1:  "(\<Gamma>, App e x, S) \<Rightarrow> (\<Gamma>, e , Arg x # S)"
 | app\<^sub>2:  "(\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow> (\<Gamma>, e[y ::= x] , S)"
 | var\<^sub>1:  "map_of \<Gamma> x = Some e \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e , Upd x # S)"
-| var\<^sub>2:  "x \<notin> domA \<Gamma> \<Longrightarrow> isLam e \<Longrightarrow> (\<Gamma>, e, Upd x # S) \<Rightarrow> ((x,e)# \<Gamma>, e , S)"
+| var\<^sub>2:  "x \<notin> domA \<Gamma> \<Longrightarrow> isVal e \<Longrightarrow> (\<Gamma>, e, Upd x # S) \<Rightarrow> ((x,e)# \<Gamma>, e , S)"
 | let\<^sub>1:  "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> (\<Gamma>, Let \<Delta> e, S) \<Rightarrow> (\<Delta>@\<Gamma>, e , S)"
+(* | if\<^sub>1:  "(\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow> (\<Gamma>, scrut, Alts e1 e2 # S)" *)
 
 abbreviation steps (infix "\<Rightarrow>\<^sup>*" 50) where "steps \<equiv> step\<^sup>*\<^sup>*"
 
@@ -15,7 +16,7 @@ lemma SmartLet_stepI:
    "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> (\<Gamma>, SmartLet \<Delta> e, S) \<Rightarrow>\<^sup>*  (\<Delta>@\<Gamma>, e , S)"
 unfolding SmartLet_def by (auto intro: let\<^sub>1)
 
-lemma lambda_var: "map_of \<Gamma> x = Some e \<Longrightarrow> isLam e  \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x,e) # delete x \<Gamma>, e , S)"
+lemma lambda_var: "map_of \<Gamma> x = Some e \<Longrightarrow> isVal e  \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x,e) # delete x \<Gamma>, e , S)"
   by (rule rtranclp_trans[OF r_into_rtranclp r_into_rtranclp])
      (auto intro: var\<^sub>1 var\<^sub>2)
 
@@ -26,9 +27,9 @@ lemma step_induction[consumes 2, case_names app\<^sub>1 app\<^sub>2 thunk lamvar
   assumes "\<not> boring_step c'"
   assumes app\<^sub>1:  "\<And> \<Gamma> e x S . P (\<Gamma>, App e x, S)  (\<Gamma>, e , Arg x # S)"
   assumes app\<^sub>2:  "\<And> \<Gamma> y e x S . P (\<Gamma>, Lam [y]. e, Arg x # S) (\<Gamma>, e[y ::= x] , S)"
-  assumes thunk:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e \<Longrightarrow> P (\<Gamma>, Var x, S) (delete x \<Gamma>, e , Upd x # S)"
-  assumes lamvar:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> isLam e \<Longrightarrow> P (\<Gamma>, Var x, S) ((x,e) # delete x \<Gamma>, e , S)"
-  assumes var\<^sub>2:  "\<And> \<Gamma> x e S . x \<notin> domA \<Gamma> \<Longrightarrow> isLam e \<Longrightarrow> P (\<Gamma>, e, Upd x # S) ((x,e)# \<Gamma>, e , S)"
+  assumes thunk:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isVal e \<Longrightarrow> P (\<Gamma>, Var x, S) (delete x \<Gamma>, e , Upd x # S)"
+  assumes lamvar:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> isVal e \<Longrightarrow> P (\<Gamma>, Var x, S) ((x,e) # delete x \<Gamma>, e , S)"
+  assumes var\<^sub>2:  "\<And> \<Gamma> x e S . x \<notin> domA \<Gamma> \<Longrightarrow> isVal e \<Longrightarrow> P (\<Gamma>, e, Upd x # S) ((x,e)# \<Gamma>, e , S)"
   assumes let\<^sub>1:  "\<And> \<Delta> \<Gamma> e S . atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> P (\<Gamma>, Let \<Delta> e, S) (\<Delta>@\<Gamma>, e, S)"
   assumes refl: "\<And> c. P c c"
   assumes trans[trans]: "\<And> c c' c''. c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c' \<Rightarrow>\<^sup>* c'' \<Longrightarrow> P c c' \<Longrightarrow> P c' c'' \<Longrightarrow> P c c''"
@@ -60,7 +61,7 @@ proof-
       next
         case (var\<^sub>1 \<Gamma> x e S)
         show ?thesis
-        proof (cases "isLam e")
+        proof (cases "isVal e")
           case False with var\<^sub>1 have "P y z" using assms(5) by metis
           with `P c y` show ?thesis by (metis t)
         next
index d1a4992..4952f25 100644 (file)
@@ -2,26 +2,31 @@ theory SestoftConf
 imports Terms Substitution
 begin
 
-datatype stack_elem = Arg var | Upd var | Dummy var
+datatype stack_elem = Alts exp exp | Arg var | Upd var | Dummy var
 
 instantiation stack_elem :: pt
 begin
-definition  "\<pi> \<bullet> x = (case x of (Arg v) \<Rightarrow> Arg (\<pi> \<bullet> v) | (Upd v) \<Rightarrow> Upd (\<pi> \<bullet> v) | (Dummy v) \<Rightarrow> Dummy (\<pi> \<bullet> v))"
+definition  "\<pi> \<bullet> x = (case x of (Alts e1 e2) \<Rightarrow> Alts (\<pi> \<bullet> e1) (\<pi> \<bullet> e2) | (Arg v) \<Rightarrow> Arg (\<pi> \<bullet> v) | (Upd v) \<Rightarrow> Upd (\<pi> \<bullet> v) | (Dummy v) \<Rightarrow> Dummy (\<pi> \<bullet> v))"
 instance
   by default (auto simp add: permute_stack_elem_def split:stack_elem.split)
 end
 
-lemma Arg_eqvt[eqvt]: "\<pi> \<bullet> (Arg v) = Arg (\<pi> \<bullet> v)"
+lemma Alts_eqvt[eqvt]: "\<pi> \<bullet> (Alts e1 e2) = Alts (\<pi> \<bullet> e1) (\<pi> \<bullet> e2)"
+  and Arg_eqvt[eqvt]: "\<pi> \<bullet> (Arg v) = Arg (\<pi> \<bullet> v)"
   and Upd_eqvt[eqvt]: "\<pi> \<bullet> (Upd v) = Upd (\<pi> \<bullet> v)"
   and Dummy_eqvt[eqvt]: "\<pi> \<bullet> (Dummy v) = Dummy (\<pi> \<bullet> v)"
   by (auto simp add: permute_stack_elem_def split:stack_elem.split)
 
+find_theorems supp name:Pair
+lemma supp_Alts[simp]: "supp (Alts e1 e2) = supp e1 \<union> supp e2" unfolding supp_def by (auto simp add: Collect_imp_eq Collect_neg_eq)
 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_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
+lemma fv_Alts[simp]: "fv (Alts e1 e2) = fv e1 \<union> fv e2"  unfolding fv_def by auto
 lemma fv_Arg[simp]: "fv (Arg v) = fv v"  unfolding fv_def by auto
 lemma fv_Upd[simp]: "fv (Upd v) = fv v"  unfolding fv_def by auto
 
@@ -29,24 +34,27 @@ instance stack_elem :: fs  by (default, case_tac x) (auto simp add: finite_supp)
 
 type_synonym stack = "stack_elem list"
 
-
 fun ap :: "stack \<Rightarrow> var set" where
   "ap [] = {}"
+| "ap (Alts e1 e2 # S) = ap S"
 | "ap (Arg x # S) = insert x (ap S)"
 | "ap (Upd x # S) = ap S"
 | "ap (Dummy x # S) = ap S"
 fun upds :: "stack \<Rightarrow> var set" where
   "upds [] = {}"
+| "upds (Alts e1 e2 # S) = upds S"
 | "upds (Upd x # S) = insert x (upds S)"
 | "upds (Arg x # S) = upds S"
 | "upds (Dummy x # S) = upds S"
 fun flattn :: "stack \<Rightarrow> var list" where
   "flattn [] = []"
+| "flattn (Alts e1 e2 # S) = fv_list e1 @ fv_list e2 @ flattn S"
 | "flattn (Upd x # S) = x # flattn S"
 | "flattn (Arg x # S) = x # flattn S"
 | "flattn (Dummy x # S) = x # flattn S"
 fun upds_list :: "stack \<Rightarrow> var list" where
   "upds_list [] = []"
+| "upds_list (Alts e1 e2 # S) = upds_list S"
 | "upds_list (Upd x # S) = x # upds_list S"
 | "upds_list (Arg x # S) = upds_list S"
 | "upds_list (Dummy x # S) = upds_list S"
@@ -60,15 +68,15 @@ lemma ups_fv_subset: "upds S \<subseteq> fv S"
 lemma ap_fv_subset: "ap S \<subseteq> fv S"
   by (induction S rule: upds.induct) auto
 
-lemma fresh_flattn[simp]: "a \<sharp> flattn S \<longleftrightarrow> a \<sharp> S"
-  by (induction S rule:flattn.induct) (auto simp add: fresh_Nil fresh_Cons)
-lemma fresh_star_flattn[simp]: "a \<sharp>* flattn S \<longleftrightarrow> a \<sharp>* S"
+lemma fresh_flattn[simp]: "atom (a::var) \<sharp> flattn S \<longleftrightarrow> atom a \<sharp> S"
+  by (induction S rule:flattn.induct) (auto simp add: fresh_Nil fresh_Cons fresh_append fresh_fv[OF finite_fv])
+lemma fresh_star_flattn[simp]: "atom ` (as:: var set) \<sharp>* flattn S \<longleftrightarrow> atom ` as \<sharp>* S"
   by (auto simp add: fresh_star_def)
 
 type_synonym conf = "(heap \<times> exp \<times> stack)"
 
 inductive boring_step where
-  "isLam e \<Longrightarrow> boring_step (\<Gamma>, e, Upd x # S)"
+  "isVal e \<Longrightarrow> boring_step (\<Gamma>, e, Upd x # S)"
 
 
 fun heap_upds_ok where "heap_upds_ok (\<Gamma>,S) \<longleftrightarrow> domA \<Gamma> \<inter> upds S = {} \<and> distinct (upds_list S)"
@@ -106,6 +114,7 @@ lemmas heap_upds_ok.simps[simp del]
 
 fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
   where "restr_stack V [] = []"
+      | "restr_stack V (Alts e1 e2 # S) = Alts e1 e2 # restr_stack V S"
       | "restr_stack V (Arg x # S) = Arg x # restr_stack V S"
       | "restr_stack V (Upd x # S) = (if x \<in> V then Upd x # restr_stack V S else restr_stack V S)"
       | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"
index 029d1a6..90c9dba 100644 (file)
@@ -33,10 +33,12 @@ case (Variable \<Gamma> x e L \<Delta> z S)
 
   note `L = flattn S`[simp]
 
+  from `isLam z` have "isVal z" by (induction z rule:exp_induct) auto
+
   from `map_of \<Gamma> x = Some e`
   have "(\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e, Upd x # S)"..
   also have "\<dots> \<Rightarrow>\<^sup>* (\<Delta>, z, Upd x # S)" by (rule Variable) simp
-  also have "\<dots> \<Rightarrow> ((x,z)#\<Delta>, z, S)" using `x \<notin> domA \<Delta>` `isLam z` by (rule var\<^sub>2)
+  also have "\<dots> \<Rightarrow> ((x,z)#\<Delta>, z, S)" using `x \<notin> domA \<Delta>` `isVal z` by (rule var\<^sub>2)
   finally show ?case.
 next
 case (Let as \<Gamma> L body \<Delta> z S)
@@ -68,7 +70,7 @@ interpretation balance_trace step  stack
 abbreviation bal_syn ("_ \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>_\<^esub> _" [50,50,50] 50) where "bal_syn \<equiv> bal"
 
 lemma lambda_stop:
-  assumes "isLam e"
+  assumes "isVal e"
   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
   shows "T=[]"
   using assms
@@ -79,7 +81,7 @@ lemma lambda_stop:
   apply auto
   apply (auto elim!: step.cases)
   done
-  
+
 lemma lemma_3:
   assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
   assumes "isLam z"
@@ -147,10 +149,10 @@ proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[w
       moreover
       note `c\<^sub>3 \<Rightarrow> c\<^sub>4`
       ultimately
-      obtain \<Delta>' z' where "c\<^sub>3 = (\<Delta>', z', Upd x # S)" and "c\<^sub>4 = ((x,z')#\<Delta>', z', S)" and "isLam z'"
+      obtain \<Delta>' z' where "c\<^sub>3 = (\<Delta>', z', Upd x # S)" and "c\<^sub>4 = ((x,z')#\<Delta>', z', S)" and "isVal z'"
         by (auto elim!: step.cases simp del: exp_assn.eq_iff)
 
-      from `isLam z'` and prem2[unfolded `c\<^sub>4 = _`]
+      from `isVal z'` and prem2[unfolded `c\<^sub>4 = _`]
       have "T\<^sub>2 = []" by (rule lambda_stop)
       with prem2 `c\<^sub>4 = _`
       have "z' = z" and "\<Delta> = (x,z)#\<Delta>'" by auto
index 3079f47..ce4d11a 100644 (file)
@@ -264,6 +264,10 @@ lemma isLam_subst[simp]: "isLam e[x::=y] = isLam e"
   by (nominal_induct e avoiding: x y  rule: exp_strong_induct)
      (auto simp add: fresh_star_Pair)
 
+lemma isVal_subst[simp]: "isVal e[x::=y] = isVal e"
+  by (nominal_induct e avoiding: x y  rule: exp_strong_induct)
+     (auto simp add: fresh_star_Pair)
+
 lemma thunks_subst[simp]:
   "thunks \<Gamma>[y::h=x] = thunks \<Gamma>"
   by (induction \<Gamma>) (auto simp add: thunks_Cons)
index 411ae3a..192fdf4 100644 (file)
@@ -366,10 +366,6 @@ lemma fv_Null[simp]: "fv Null = {}"
 lemma fv_IfThenElse[simp]: "fv (scrut ? e1 : e2)  = fv scrut \<union> fv e1 \<union> fv e2"
   unfolding fv_def by (auto simp add: exp_assn.supp)
 
-lemma finite_fv_exp[simp]: "finite (fv (e::exp) :: var set)"
-  and finite_fv_heap[simp]: "finite (fv (\<Gamma> :: heap) :: var set)"
-  by (induction e rule:exp_heap_induct) auto
-
 
 lemma fv_delete_heap:
   assumes "map_of \<Gamma> x = Some e"
@@ -508,6 +504,25 @@ nominal_termination (eqvt) by lexicographic_order
 
 lemma isLam_Lam: "isLam (Lam [x]. e)" by simp
 
+nominal_function isVal :: "exp \<Rightarrow> bool" where
+  "isVal (Var x) = False" |
+  "isVal (Lam [x]. e) = True" |
+  "isVal (App e x) = False" |
+  "isVal (Let as e) = False" |
+  "isVal Null = True" |
+  "isVal (scrut ? e1 : e2) = False"
+  unfolding isVal_graph_aux_def eqvt_def
+  apply simp
+  apply simp
+  apply (metis exp_strong_exhaust)
+  apply auto
+  done
+nominal_termination (eqvt) by lexicographic_order
+
+lemma isVal_Lam: "isVal (Lam [x]. e)" by simp
+lemma isVal_Null: "isVal Null" by simp
+
+
 subsubsection {* The notion of thunks *}
 (*
 fun thunks :: "heap \<Rightarrow> var set" where
@@ -516,14 +531,14 @@ fun thunks :: "heap \<Rightarrow> var set" where
 *)
 
 definition thunks :: "heap \<Rightarrow> var set" where
-  "thunks \<Gamma> = {x . case map_of \<Gamma> x of Some e \<Rightarrow> \<not> isLam e | None \<Rightarrow> False}"
+  "thunks \<Gamma> = {x . case map_of \<Gamma> x of Some e \<Rightarrow> \<not> isVal e | None \<Rightarrow> False}"
 
 lemma thunks_Nil[simp]: "thunks [] = {}" by (auto simp add: thunks_def)
 
 lemma thunks_domA: "thunks \<Gamma> \<subseteq> domA \<Gamma>"
   by (induction \<Gamma> ) (auto simp add: thunks_def)
 
-lemma thunks_Cons: "thunks ((x,e)#\<Gamma>) = (if isLam e then thunks \<Gamma> - {x} else insert x (thunks \<Gamma>))"
+lemma thunks_Cons: "thunks ((x,e)#\<Gamma>) = (if isVal e then thunks \<Gamma> - {x} else insert x (thunks \<Gamma>))"
   by (auto simp add: thunks_def )
 
 lemma thunks_append[simp]: "thunks (\<Delta>@\<Gamma>) = thunks \<Delta> \<union> (thunks \<Gamma> - domA \<Delta>)"
@@ -532,10 +547,10 @@ lemma thunks_append[simp]: "thunks (\<Delta>@\<Gamma>) = thunks \<Delta> \<union
 lemma thunks_delete[simp]: "thunks (delete x \<Gamma>) = thunks \<Gamma> - {x}"
   by (induction \<Gamma>) (auto simp add: thunks_def )
 
-lemma thunksI[intro]: "map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e \<Longrightarrow> x \<in> thunks \<Gamma>"
+lemma thunksI[intro]: "map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isVal e \<Longrightarrow> x \<in> thunks \<Gamma>"
   by (induction \<Gamma>) (auto simp add: thunks_def )
 
-lemma thunksE[intro]: "x \<in> thunks \<Gamma> \<Longrightarrow> map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isLam e"
+lemma thunksE[intro]: "x \<in> thunks \<Gamma> \<Longrightarrow> map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isVal e"
   by (induction \<Gamma>) (auto simp add: thunks_def )
 
 lemma thunks_cong: "map_of \<Gamma> = map_of \<Delta> \<Longrightarrow> thunks \<Gamma> = thunks \<Delta>"