Progress towards a correctness proof based on futures
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 31 Oct 2014 10:28:14 +0000 (10:28 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 31 Oct 2014 10:28:14 +0000 (10:28 +0000)
15 files changed:
Launchbury/AbstractTransform.thy
Launchbury/ArityEtaExpand.thy
Launchbury/C.thy
Launchbury/CallArityEtaExpand.thy
Launchbury/CallFutures.thy [new file with mode: 0644]
Launchbury/CoCallsFuture.thy [new file with mode: 0644]
Launchbury/Env.thy
Launchbury/FutureEtaExpand.thy [new file with mode: 0644]
Launchbury/HOLCF-Utils.thy
Launchbury/Nominal-HOLCF.thy
Launchbury/Nominal-Utils.thy
Launchbury/SestoftGC.thy [new file with mode: 0644]
Launchbury/Set_Cpo.thy [new file with mode: 0644]
Launchbury/Set_Cpo_Nominal.thy [new file with mode: 0644]
Launchbury/TransformTools.thy

index 59a1fcd..3ab1ef8 100644 (file)
@@ -15,7 +15,7 @@ locale AbstractAnalProp =
   assumes PropLetHeap_eqvt: "\<pi> \<bullet> PropLetHeap \<equiv> PropLetHeap"
 
 locale AbstractAnalPropSubst = AbstractAnalProp +
-  assumes PropLetHeap_subst:  "x \<notin> domA \<Gamma> \<Longrightarrow> y \<notin> domA \<Gamma> \<Longrightarrow> AnalLet (\<Gamma>[x::h=y]) (e[x::=y]) a = AnalLet \<Gamma> e a"
+  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"
 
 locale AbstractTransform = AbstractAnalProp +
   constrains AnalLet :: "heap \<Rightarrow> exp \<Rightarrow> 'a::pure_cont_pt \<Rightarrow> 'b::cont_pt"
@@ -153,7 +153,7 @@ begin
   proof (nominal_induct e avoiding: x y arbitrary: a  rule: exp_strong_induct_set)
   case (Let \<Delta> body x y)
     hence *: "x \<notin> domA \<Delta>" "y \<notin> domA \<Delta>" by (auto simp add: fresh_star_def fresh_at_base)
-    hence "AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a" by (rule PropLetHeap_subst)
+    hence "AnalLet \<Delta>[x::h=y] body[x::=y] a = AnalLet \<Delta> body a" by (rule AnalLet_subst)
     with Let
     show ?case
     apply (auto simp add: fresh_star_Pair TransLet_subst simp del: Let_eq_iff)
@@ -167,7 +167,10 @@ end
 
 locale AbstractTransformBound = AbstractAnalProp + supp_bounded_transform  +
   constrains PropApp :: "'a \<Rightarrow> 'a::pure_cont_pt"
-  constrains trans :: "'a::pure_cont_pt \<Rightarrow> exp \<Rightarrow> exp"
+  constrains PropLetHeap :: "'b::cont_pt \<Rightarrow> var \<Rightarrow> 'a\<^sub>\<bottom>"
+  constrains trans :: "'c::cont_pt \<Rightarrow> exp \<Rightarrow> exp"
+  fixes PropLetHeapTrans :: "'b\<Rightarrow> var \<Rightarrow> 'c\<^sub>\<bottom>"
+  assumes PropLetHeapTrans_eqvt: "\<pi> \<bullet> PropLetHeapTrans = PropLetHeapTrans"
   assumes TransBound_eqvt: "\<pi> \<bullet> trans = trans"
 begin
   sublocale AbstractTransform PropApp PropLam AnalLet PropLetBody PropLetHeap
@@ -175,9 +178,9 @@ begin
       "(\<lambda> a. Var1)"
       "(\<lambda> a. App)"
       "(\<lambda> a. Terms.Lam)"
-      "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeap b) \<Gamma>) e)"
+      "(\<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] TransBound_eqvt[eqvt]
+  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]
   case goal1
   show ?case
   apply default
@@ -196,7 +199,7 @@ begin
       "(\<lambda> a. Var1)"
       "(\<lambda> a. App)"
       "(\<lambda> a. Terms.Lam)"
-      "(\<lambda> b \<Gamma> e . Let (map_transform trans (PropLetHeap b) \<Gamma>) e)"
+      "(\<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]
   case goal1
index cc0075b..ca30126 100644 (file)
@@ -36,8 +36,9 @@ begin
     "\<lambda> b . fst b"
     "\<lambda> b . snd b"
     "Aeta_expand"
+    "\<lambda> b . snd b"
   apply default
-  apply (((rule eq_reflection)?, perm_simp, rule)+)[6]
+  apply (((rule eq_reflection)?, perm_simp, rule)+)[7]
   done
 
   sublocale AbstractTransformBoundSubst
@@ -47,10 +48,11 @@ begin
     "\<lambda> b . fst b"
     "\<lambda> b . snd b"
     "Aeta_expand"
+    "\<lambda> b . snd b"
   apply default
   apply (simp add: Aheap_subst  Aheap_cong[OF Aexp_subst_restr])[1]
   apply (rule subst_Aeta_expand)  
-   done
+  done
 
   abbreviation Atransform where "Atransform \<equiv> transform"
 
@@ -140,17 +142,14 @@ case (app\<^sub>2 \<Gamma> y e x S)
     apply (rule below_trans[OF monofun_cfun_fun[OF Aexp_subst_App_Lam]])
     apply (auto simp add: Aexp_App Aexp_Lam join_below_iff)
     done
-  hence "consistent (ae, pred \<cdot> a) (\<Gamma>, e[y::=x], S)"  using app\<^sub>2
-    apply  (auto intro!:  below_trans[OF monofun_cfun_fun[OF Aexp_subst_App_Lam]] simp add: Aexp_App join_below_iff monofun_cfun_arg)
-    apply (metis image_eqI singletonD subsetCE)+
-    done
+  hence "consistent (ae, pred \<cdot> a) (\<Gamma>, e[y::=x], S)"  using app\<^sub>2  by fastforce
   moreover
   have "conf_transform (ae, a) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow> conf_transform (ae, pred \<cdot> a) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
   ultimately
   show ?case by (blast del: consistentI consistentE)
 next
 case (thunk \<Gamma> x e S)
-  hence "consistent (ae, 0) (delete x \<Gamma>, e, Upd x # S)" using thunk by (fastforce simp add: join_below_iff)
+  have "consistent (ae, 0) (delete x \<Gamma>, e, Upd x # S)" using thunk by (fastforce simp add: join_below_iff)
   moreover
   {
   from thunk
index bddc984..5941059 100644 (file)
@@ -114,4 +114,5 @@ lemma C_Cpred_id[simp]:
   "r \<noteq> \<bottom> \<Longrightarrow> C\<cdot>(Cpred\<cdot>r) = r"
   by (cases r) auto
 
+
 end
index 90d3222..949a5fa 100644 (file)
@@ -20,7 +20,7 @@ begin
   interpretation AbstractTransformBoundSubst
     "\<lambda> a . inc\<cdot>a"
     "\<lambda> a . pred\<cdot>a"
-    "\<lambda> \<Delta> e a . (a, ccFix \<Delta>\<cdot>(cccExp e\<cdot>a))"
+    "\<lambda> \<Delta> e a . (a, combined_restrict (domA \<Delta>) (ccFix \<Delta>\<cdot>(cccExp e\<cdot>a)))"
     "\<lambda> b . fst b"
     "\<lambda> b . fst (snd b)"
     "Aeta_expand"
diff --git a/Launchbury/CallFutures.thy b/Launchbury/CallFutures.thy
new file mode 100644 (file)
index 0000000..f0e57c5
--- /dev/null
@@ -0,0 +1,145 @@
+theory CallFutures
+imports Vars "Nominal-Utils" "Set_Cpo"
+begin
+
+type_synonym future = "var \<Rightarrow> nat"
+
+definition no_future :: future where "no_future v = 0"
+
+definition possible :: "var \<Rightarrow> future \<Rightarrow> bool"
+  where "possible v f = (f v > 0)"
+
+inductive_set domF :: "future \<Rightarrow> var set" for f
+  where "possible v f \<Longrightarrow> v \<in> domF f"
+
+lemma possible_eqvt[eqvt]: "\<pi> \<bullet> possible v f = possible (\<pi> \<bullet> v) (\<pi> \<bullet> f)"
+  unfolding possible_def by simp
+
+definition after :: "var \<Rightarrow> future \<Rightarrow> future"
+  where "after v f = (f(v := f v - 1))"
+
+lemma after_eqvt[eqvt]: "\<pi> \<bullet> after v f = after (\<pi> \<bullet> v) (\<pi> \<bullet> f)"
+  unfolding after_def by simp
+
+lemma after_swap: "after x (after y f) = after y (after x f)"
+  unfolding after_def by auto
+
+definition without :: "var \<Rightarrow> future \<Rightarrow> future"
+  where "without v f = (f(v := 0))"
+
+lemma without_eqvt[eqvt]: "\<pi> \<bullet> without v f = without (\<pi> \<bullet> v) (\<pi> \<bullet> f)"
+  unfolding without_def by simp
+
+
+type_synonym futures = "var \<Rightarrow> future set"
+
+definition combine :: "future \<Rightarrow> future \<Rightarrow> future"
+  where "combine f1 f2 v = f1 v + f2 v"
+
+(* http://stackoverflow.com/questions/16603886/inductive-set-with-non-fixed-parameters *)
+
+inductive paths' :: "futures \<Rightarrow> future set \<Rightarrow> var list \<Rightarrow> bool" for G
+  where "paths' G current []"
+  | "f \<in> current \<Longrightarrow> possible x f \<Longrightarrow> paths' G (combine (after x f) ` (G x)) path \<Longrightarrow> paths' G current (x#path)"
+
+definition paths  :: "futures \<Rightarrow> future set \<Rightarrow> var list set" 
+  where "paths G current = Collect (paths' G current)"
+lemma elim_paths'[pred_set_conv]: "paths' G f p \<longleftrightarrow> p \<in> paths G f" unfolding paths_def by simp
+
+lemmas paths_intros[intro?] = paths'.intros[unfolded elim_paths']
+lemmas paths_induct[consumes 1, induct set: paths] = paths'.induct[to_set]
+lemmas paths_cases[consumes 1, cases set: paths] = paths'.cases[to_set]
+lemmas paths_simpss = paths'.simps[to_set]
+
+lemma possible_no_future[simp]: "possible xa no_future \<longleftrightarrow> False"
+  by (auto simp add: possible_def no_future_def)
+
+lemma possible_upd[simp]: "possible x' (f(x := n)) \<longleftrightarrow> (x = x' \<and> n > 0) \<or> (possible x' f \<and> x' \<noteq> x)"
+  by (auto simp add: possible_def no_future_def)
+
+lemma after_upd[simp]: "after x (f(x := n)) = f(x := n - 1)"
+  by (auto simp add: after_def)
+
+lemma [simp]: "x \<noteq> y \<Longrightarrow> after x (f(y := n)) =( after x f)(y := n)"
+  by (auto simp add: after_def)
+
+lemma no_future_upd0[simp]: "no_future(x := 0) = no_future"
+  by (auto simp add: no_future_def)
+
+lemma combine_nofuture[simp]: "combine no_future f = f"
+  by (auto simp add: no_future_def combine_def)
+
+definition may_call :: "var \<Rightarrow> future set \<Rightarrow> future set"
+  where "may_call v fs = {f . \<exists> f' \<in> fs. \<forall> x. x \<noteq> v \<longrightarrow> f x = f' x}"
+
+lemma may_call_cont: "cont (may_call v)" sorry
+lemmas may_call_cont[cont2cont, simp]
+
+
+text {* Some tests *}
+
+lemma cons_eq_replicate[simp]: "x'#xs = replicate n x \<longleftrightarrow> x' = x \<and> n > 0 \<and> xs = replicate (n - 1) x"
+  by (cases n) auto
+
+lemma snoc_eq_replicate[simp]: "xs @ [x'] = replicate n x  \<longleftrightarrow> x' = x \<and> n > 0 \<and> xs = replicate (n - 1) x"
+proof-
+  have "xs @ [x'] = replicate n x \<longleftrightarrow> rev (xs @ [x']) = rev (replicate n x)" by (metis rev_rev_ident)
+  also have "\<dots> \<longleftrightarrow> rev (xs @ [x']) = replicate n x" by (metis rev_replicate)
+  also have "\<dots> \<longleftrightarrow> x'# (rev xs)  = replicate n x" by (metis rev.simps(2) rev_rev_ident)
+  also have "\<dots> \<longleftrightarrow> x' = x \<and> n > 0 \<and> rev xs = replicate (n - 1) x" by (rule cons_eq_replicate)
+  also have "\<dots> \<longleftrightarrow> x' = x \<and> n > 0 \<and> xs = replicate (n - 1) x" by (metis rev_rev_ident rev_replicate)
+  finally show ?thesis.
+qed 
+
+lemma [simp]: "replicate n x @ [x'] = replicate n' x \<longleftrightarrow> n' = Suc n \<and> x' = x"
+  by auto
+
+lemma
+  fixes G current
+  assumes [simp]:"G = ((\<lambda> _. {})(x := current))"
+  assumes [simp]:"current = {no_future(x := 1)}"
+  shows "paths G current = {replicate n x | n. True}"
+proof(rule set_eqI, rule)
+  fix p
+  assume "p \<in> paths G current"
+  from  this `current = _` 
+  show "p \<in> {replicate n x |n. True}" by (induction) auto
+next
+  fix p
+  assume "p \<in> {replicate n x |n. True}"
+  then obtain n where "p = replicate n x" by auto
+  thus "p \<in> paths G current"
+  by (induction p arbitrary: n)(auto intro: paths_intros)
+qed   
+
+lemma
+  assumes [simp]: "x\<noteq>y"
+  assumes [simp]:"G = ((\<lambda> _. {})(x := current, y := {no_future}))"
+  assumes [simp]:"current = {no_future(x := 1), no_future(y := 1)}"
+  shows "paths G current = {replicate n x | n. True} \<union> {replicate n x @ [y]| n. True}"
+proof(rule set_eqI, rule)
+  fix p
+  assume "p \<in> paths G current"
+  hence "(current = {no_future} \<Longrightarrow> p = [])" and "current = {no_future(x := 1), no_future(y := 1)} \<Longrightarrow> p \<in> {replicate n x | n. True} \<union>  {replicate n x @ [y]| n. True}"
+    by induction (auto, arith+)
+  with `current = _`
+  show "p \<in> {replicate n x | n. True} \<union>  {replicate n x @ [y]| n. True}" by blast
+next
+  fix p
+  {
+  fix n
+  have "replicate n x \<in> paths G current"
+    by (induction n) (auto intro: paths_intros (1) paths_intros(2)[where f = "no_future(x := Suc 0)"])
+  moreover
+  have "replicate n x @ [y] \<in> paths G current"
+    by (induction n) (auto intro: paths_intros(1) paths_intros(2)[where f = "no_future(x := Suc 0)"]  paths_intros(2)[where f = "no_future(y := Suc 0)"])
+  moreover
+  note calculation
+  }
+  moreover
+  assume  "p \<in> {replicate n x | n. True} \<union>  {replicate n x @ [y]| n. True}"
+  ultimately
+  show "p \<in> paths G current" by blast
+qed
+
+end
diff --git a/Launchbury/CoCallsFuture.thy b/Launchbury/CoCallsFuture.thy
new file mode 100644 (file)
index 0000000..41635eb
--- /dev/null
@@ -0,0 +1,18 @@
+theory CoCallsFuture
+imports CoCallGraph CallFutures
+begin
+
+inductive_set any_future :: "var set \<Rightarrow> future set" for S
+  where "domF f \<subseteq> S \<Longrightarrow> f \<in> any_future S"
+
+definition conformsToCC :: "future \<Rightarrow> CoCalls \<Rightarrow> bool"
+  where "conformsToCC f G \<longleftrightarrow> (\<forall>x y. (x--y\<notin>G) \<longrightarrow> possible x f \<longrightarrow>  \<not> possible y (after x f))"
+
+definition ccFilterFuture  :: "future set \<Rightarrow> CoCalls \<Rightarrow> future set"
+  where "ccFilterFuture S G = {f \<in> S . conformsToCC f G}"
+
+lemma no_future_conforms:  "conformsToCC no_future G"
+  unfolding conformsToCC_def by simp
+
+
+end  
index e39a367..4665073 100644 (file)
@@ -23,6 +23,11 @@ lemma lookup_not_edom: "x \<notin> edom m \<Longrightarrow> m x = \<bottom>"  by
 
 lemma lookup_edom[simp]: "m x \<noteq> \<bottom> \<Longrightarrow> x \<in> edom m"  by (auto iff:edomIff)
 
+lemma edom_mono: "x \<sqsubseteq> y \<Longrightarrow> edom x \<subseteq> edom y"
+  unfolding edom_def
+  by auto (metis below_bottom_iff fun_belowD)
+  
+
 lemma edom_subset_adm[simp]:
   "adm (\<lambda>ae'. edom ae' \<subseteq> S)"
   apply (rule admI)
@@ -193,6 +198,9 @@ lemma env_restr_env_delete_other[simp]: "x \<notin> S \<Longrightarrow> env_dele
 lemma env_delete_restr: "env_delete x m = m f|` (-{x})"
   by (auto simp add: lookup_env_restr_eq)
 
+lemma below_env_deleteI: "f x = \<bottom> \<Longrightarrow> f \<sqsubseteq> g \<Longrightarrow> f \<sqsubseteq> env_delete x g"
+  by (metis env_delete_def env_delete_restr env_restr_mono fun_upd_triv)
+
 subsubsection {* Merging of two functions *}
 
 text {*
diff --git a/Launchbury/FutureEtaExpand.thy b/Launchbury/FutureEtaExpand.thy
new file mode 100644 (file)
index 0000000..6db5314
--- /dev/null
@@ -0,0 +1,343 @@
+theory FutureEtaExpand
+imports CallFutures AEnv Terms EtaExpansionArity EtaExpansionSestoft AbstractTransform Set_Cpo_Nominal  Sestoft SestoftGC
+begin
+
+default_sort type
+
+type_synonym oneShot = "one"
+abbreviation notOneShot :: oneShot where "notOneShot \<equiv> ONE"
+abbreviation oneShot :: oneShot where "oneShot \<equiv> \<bottom>"
+
+type_synonym two = "oneShot\<^sub>\<bottom>"
+abbreviation many :: two where "many \<equiv> up\<cdot>notOneShot"
+abbreviation once :: two where "once \<equiv> up\<cdot>oneShot"
+abbreviation none :: two where "none \<equiv> \<bottom>"
+
+definition two_pred where "two_pred = (\<Lambda> x. if x = once then \<bottom> else x)"
+
+definition record_call where "record_call x = (\<Lambda> ce. (\<lambda> y. if x = y then two_pred\<cdot>(ce y) else ce x))"
+
+lemma two_conj: "c = many \<or> c = once \<or> c = none" sorry
+
+lemma two_cases[case_names many once none]:
+  obtains "c = many" | "c = once" | "c = none" using two_conj by metis
+
+
+definition abstractPath :: "var list set \<Rightarrow> var \<Rightarrow> two"
+  where "abstractPath ps v = undefined"
+
+text {* Expands only if it is safe to do so, i.e. either one-shot or already a function. *}
+
+fun rhsExpand :: "(Arity \<times> one) \<Rightarrow> exp \<Rightarrow> exp"
+  where "rhsExpand (a,c) e = (if isLam e \<or> c = \<bottom> then Aeta_expand a e else e)"
+
+interpretation supp_bounded_transform rhsExpand sorry
+
+lemma rhsExpand[eqvt]: "\<pi> \<bullet> rhsExpand = rhsExpand" sorry
+
+
+fun Astack :: "stack \<Rightarrow> Arity"
+  where "Astack [] = 0"
+      | "Astack (Arg x # S) = inc\<cdot>(Astack S)"
+      | "Astack (Upd x # S) = 0"
+      | "Astack (Dummy x # S) = 0"
+
+
+lemma Aeta_expand_correct:
+  assumes "Astack S \<sqsubseteq> a"
+  shows "(\<Gamma>, Aeta_expand a e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)"
+proof-
+  have "arg_prefix S = Rep_Arity (Astack S)"
+    by (induction S arbitrary: a rule: arg_prefix.induct) (auto simp add: Arity.zero_Arity.rep_eq[symmetric])
+  also
+  from assms(1)
+  have "Rep_Arity a \<le> Rep_Arity (Astack S)" by (metis below_Arity.rep_eq)
+  finally
+  show ?thesis by transfer (rule eta_expansion_correct')
+qed
+
+
+fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
+  where "restr_stack V [] = []"
+      | "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 (insert x V) S)"
+      | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"
+
+lemma Astack_restr_stack_below:
+  "Astack (restr_stack V S) \<sqsubseteq> Astack S"
+  by (induction V S rule: restr_stack.induct) auto
+
+
+
+definition fup_fst :: "(var \<Rightarrow> (Arity \<times> one)\<^sub>\<bottom>) \<Rightarrow> AEnv"
+    where "fup_fst e x = fup\<cdot>(\<Lambda> p. up\<cdot>(cfst\<cdot>p))\<cdot>(e x)"
+
+lemma fup_fst_eqvt[eqvt]: "\<pi> \<bullet> (fup_fst e x) = fup_fst (\<pi> \<bullet> e) (\<pi> \<bullet> x)"
+  unfolding fup_fst_def
+  by perm_simp rule
+
+locale FutureAnalysis =
+  fixes aExp :: "exp \<Rightarrow> Arity \<rightarrow> AEnv"
+  fixes fExp :: "exp \<Rightarrow> Arity \<rightarrow> future set"
+  fixes fHeap :: "heap \<Rightarrow> (AEnv \<times> future set) \<rightarrow> (var \<Rightarrow> (Arity \<times> one)\<^sub>\<bottom>)"
+
+  assumes aExp_Var: "up \<cdot> n \<sqsubseteq> (aExp (Var x)\<cdot>n) x"
+  assumes aExp_App: "aExp (App e x) \<cdot> n = aExp e \<cdot>(inc\<cdot>n) \<squnion> AE_singleton x \<cdot> (up\<cdot>0)"
+  assumes aExp_subst_App_Lam: "aExp (e[y::=x]) \<sqsubseteq> aExp (App (Lam [y]. e) x)"
+  assumes aExp_Lam: "aExp (Lam [y]. e) \<cdot> n = env_delete y (aExp e \<cdot>(pred\<cdot>n))"
+
+
+  assumes fExp_App: "fExp (App e x)\<cdot>n = may_call x (fExp e \<cdot>(inc\<cdot>n))"
+
+  assumes aExp[eqvt]: "\<pi> \<bullet> aExp = aExp"
+  assumes fExp[eqvt]: "\<pi> \<bullet> fExp = fExp"
+  assumes fHeap[eqvt]: "\<pi> \<bullet> fHeap = fHeap"
+begin
+
+  sublocale AbstractTransformBound
+    "\<lambda> a . inc\<cdot>a"
+    "\<lambda> a . pred\<cdot>a"
+    "\<lambda> \<Delta> e a . (a, fHeap \<Delta>\<cdot>(aExp e\<cdot>a, fExp e\<cdot>a))"
+    "fst"
+    "\<lambda> b . fup_fst (snd b)"
+    "rhsExpand"
+    "snd"
+  apply default
+  apply (((rule eq_reflection)?, perm_simp, rule)+)[7]
+  done
+
+  sublocale AbstractTransformBoundSubst
+    "\<lambda> a . inc\<cdot>a"
+    "\<lambda> a . pred\<cdot>a"
+    "\<lambda> \<Delta> e a . (a, fHeap \<Delta>\<cdot>(aExp e\<cdot>a, fExp e\<cdot>a))"
+    "fst"
+    "\<lambda> b . fup_fst (snd b)"
+    "rhsExpand"
+    "snd"
+  apply default
+  apply (simp add: Aheap_subst  Aheap_cong[OF Aexp_subst_restr])[1]
+  apply (rule subst_Aeta_expand)  
+  sorry
+
+  abbreviation ccTransform where "ccTransform \<equiv> transform"
+
+  type_synonym tstate = "(AEnv \<times> (var \<Rightarrow> two) \<times> Arity)"
+
+  fixrec u_com :: "'a::cpo\<^sub>\<bottom> \<rightarrow> 'b::cpo\<^sub>\<bottom> \<rightarrow> ('a \<times> 'b)\<^sub>\<bottom>"
+    where "u_com\<cdot>(up\<cdot>x)\<cdot>(up\<cdot>y) = up\<cdot>(x, y)"
+  lemma u_com_strict[simp]: "u_com\<cdot>\<bottom>\<cdot>\<bottom> = \<bottom>" by fixrec_simp
+
+  definition env_u_com ::  "('c::type \<Rightarrow> 'a::cpo\<^sub>\<bottom>) \<Rightarrow> ('c \<Rightarrow> 'b::cpo\<^sub>\<bottom>) \<Rightarrow> ('c \<Rightarrow> ('a \<times> 'b)\<^sub>\<bottom>)"
+    where [simp]: "env_u_com e1 e2 x = u_com\<cdot>(e1 x)\<cdot>(e2 x)"
+  lemma env_u_com_delete: "env_u_com (env_delete x e1) (env_delete x e2) = env_delete x (env_u_com e1 e2)"
+    by (rule, case_tac "xa = x") auto
+  
+
+  fun conf_transform :: "tstate \<Rightarrow> conf \<Rightarrow> conf"
+  where "conf_transform (ae, ce,  a) (\<Gamma>, e, S) =
+    (map_transform rhsExpand (env_u_com ae ce) (map_transform ccTransform ae \<Gamma>), 
+     ccTransform a e,
+     restr_stack (edom ae) S)"
+
+  definition anal_env :: "(exp \<Rightarrow> 'a::cpo \<rightarrow> 'b::pcpo) \<Rightarrow> heap \<Rightarrow> (var \<Rightarrow> 'a\<^sub>\<bottom>) \<rightarrow> (var \<Rightarrow> 'b)"
+    where "anal_env f \<Gamma> = (\<Lambda> e. (\<lambda> x . fup\<cdot>(f (the (map_of \<Gamma> x)))\<cdot>(e x)))"
+
+  fun fstack :: "stack \<Rightarrow> future set \<rightarrow> future set"
+    where "fstack [] = (\<Lambda> f. f)"
+        | "fstack (Arg x # S) = (\<Lambda> f . fstack S \<cdot> (may_call x f))"
+        | "fstack (Upd x # S) = fstack S"
+        | "fstack (Dummy x # S) = fstack S"
+
+
+  definition const_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
+    where "const_on f S x = (\<forall> y \<in> S . f y = x)"
+
+  lemma const_on_simp:
+   "const_on f S r \<Longrightarrow> x \<in> S \<Longrightarrow> f x = r"
+   by (simp add: const_on_def)
+
+  lemma const_onE[elim]: "const_on f S r ==> x : S ==> r = r' ==> f x = r'"     by (simp add: const_on_def)
+
+  lemma const_on_insert[simp]: "const_on f (insert x S) y \<longleftrightarrow> const_on f S y \<and> f x = y"
+    unfolding const_on_def by auto
+
+  lemma thunks_delete[simp]: "thunks (delete x \<Gamma>) = thunks \<Gamma> - {x}" sorry
+
+  fun prognosis :: "AEnv \<Rightarrow> Arity \<Rightarrow> conf \<Rightarrow> (var \<Rightarrow> two)"
+    where "prognosis ae a (\<Gamma>, e, S) = abstractPath (paths (anal_env fExp \<Gamma> \<cdot> ae) (fstack S \<cdot> (fExp e \<cdot> a)))"
+  lemmas prognosis.simps[simp del]
+
+  inductive consistent :: "tstate \<Rightarrow> conf \<Rightarrow> bool" where
+    consistentI[intro!]: 
+    "edom ae \<subseteq> domA \<Gamma> \<union> upds S
+    \<Longrightarrow> edom ce = edom ae
+    \<Longrightarrow> Astack (restr_stack (edom ae) S) \<sqsubseteq> a
+    \<Longrightarrow> aExp e \<cdot> a \<sqsubseteq> ae
+    \<Longrightarrow> prognosis ae a  (\<Gamma>, e, S) \<sqsubseteq> ce
+    \<Longrightarrow> (\<And> x. x \<in> thunks \<Gamma> \<Longrightarrow>  many \<sqsubseteq> ce x \<Longrightarrow> ae x = up\<cdot>0)
+    \<Longrightarrow> (\<And> x e'. map_of \<Gamma> x = Some e' \<Longrightarrow> x \<in> edom (prognosis ae a  (\<Gamma>, e, S)) \<Longrightarrow> fup\<cdot>(aExp e')\<cdot>(ae x) \<sqsubseteq> ae)
+    \<Longrightarrow> const_on ae (ap S) (up\<cdot>0)
+    \<Longrightarrow> consistent (ae, ce, a) (\<Gamma>, e, S)"  
+  inductive_cases consistentE[elim!]: "consistent (ae, ce, a) (\<Gamma>, e, S)"
+  
+  lemma foo:
+    fixes c c' R 
+    assumes "c \<Rightarrow>\<^sup>* c'" and "\<not> boring_step c'" and "consistent (ae,ce,a) c"
+    shows "\<exists>ae' ce' a'. consistent (ae',ce',a') c' \<and> conf_transform (ae,ce,a) c \<Rightarrow>\<^sub>G\<^sup>* conf_transform (ae',ce',a') c'"
+  using assms
+  proof(induction c c' arbitrary: ae ce a rule:step_induction)
+  case (app\<^sub>1 \<Gamma> e x S)
+    have " prognosis ae (inc\<cdot>a) (\<Gamma>, e, Arg x # S) = prognosis ae a (\<Gamma>, App e x, S)" sorry
+    with app\<^sub>1 have "consistent (ae, ce, inc\<cdot>a) (\<Gamma>, e, Arg x # S)"
+      by (auto simp add: join_below_iff fExp_App aExp_App)
+    moreover
+    have "conf_transform (ae, ce, a) (\<Gamma>, App e x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, inc\<cdot>a) (\<Gamma>, e, Arg x # S)"
+      by simp rule
+    ultimately
+    show ?case by (blast del: consistentI consistentE)
+  next
+case (app\<^sub>2 \<Gamma> y e x S)
+  have "aExp (e[y ::= x])\<cdot>(pred\<cdot>a) \<sqsubseteq> ae" using app\<^sub>2
+    apply (auto simp add:  join_below_iff)
+    apply (rule below_trans[OF monofun_cfun_fun[OF aExp_subst_App_Lam]])
+    apply (auto simp add: aExp_App aExp_Lam join_below_iff)
+    done
+  moreover
+  have "fExp e[y::=x]\<cdot>(pred\<cdot>a) \<sqsubseteq> may_call x (fExp (Lam [y]. e)\<cdot>a)" sorry
+  hence "fstack S\<cdot>(fExp e[y::=x]\<cdot>(pred\<cdot>a)) \<sqsubseteq> fstack S\<cdot>(may_call x (fExp (Lam [y]. e)\<cdot>a))" by (rule monofun_cfun_arg)
+  hence "prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S) \<sqsubseteq> prognosis ae a (\<Gamma>, (Lam [y]. e), Arg x # S)"
+    sorry
+  moreover
+  hence "edom (prognosis ae (pred\<cdot>a) (\<Gamma>, e[y::=x], S)) \<subseteq> edom (prognosis ae a (\<Gamma>, (Lam [y]. e), Arg x # S))" 
+    by (rule edom_mono)
+  ultimately
+  have "consistent (ae, ce, pred\<cdot>a) (\<Gamma>, e[y::=x], S)"  using app\<^sub>2
+    by (auto elim: below_trans)
+  moreover
+  have "conf_transform (ae, ce, a) (\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, pred \<cdot> a) (\<Gamma>, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
+  ultimately
+  show ?case by (blast  del: consistentI consistentE)
+next
+case (thunk \<Gamma> x e S)
+  hence "x \<in> thunks \<Gamma>" sorry
+
+  from thunk have "aExp (Var x)\<cdot>a \<sqsubseteq> ae" by auto
+  from below_trans[OF aExp_Var fun_belowD[OF this] ]
+  have "up\<cdot>a \<sqsubseteq> ae x".    
+  then obtain u where "ae x = up\<cdot>u" and "a \<sqsubseteq> u" by (cases "ae x") auto
+  hence [simp]: "x \<in> edom ae" by (simp add: edom_def)
+
+  have "Astack (restr_stack (edom ae) S) \<sqsubseteq> u" using thunk `a \<sqsubseteq> u` by (auto elim: below_trans)
+
+  have "x \<in> edom (prognosis ae a (\<Gamma>, Var x, S))" sorry
+  hence "fup\<cdot>(aExp e)\<cdot>(ae x) \<sqsubseteq> ae " using  thunk by blast
+  hence "aExp e\<cdot>u \<sqsubseteq> ae" using  `ae x = up\<cdot>u` by auto
+
+
+  show ?case
+  proof(cases "ce x" rule:two_cases)
+    case none
+    hence "ae x = \<bottom>"  using none thunk by (auto simp add: edom_def)
+    with `x \<in> edom ae` have False by (auto simp add: edom_def)
+    thus ?thesis..
+  next
+    case once
+
+    note `ae x = up\<cdot>u` `a \<sqsubseteq> u`
+    moreover
+
+    have "prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce" using thunk by auto
+    hence "prognosis ae a (\<Gamma>, Var x, S) x \<sqsubseteq> once"
+      using once by (metis (mono_tags) fun_belowD)
+    hence "x \<notin> ap S" sorry
+    moreover
+
+    have *: "prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)"
+      sorry
+
+    from `prognosis ae a (\<Gamma>, Var x, S) x \<sqsubseteq> once`
+    have **:  "prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S) x = \<bottom>" sorry
+  
+    have "prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> env_delete x ce"
+      using ** below_trans[OF * `prognosis ae a (\<Gamma>, Var x, S) \<sqsubseteq> ce`]
+      by (rule below_env_deleteI)
+    moreover
+
+    from **
+    have "(aExp e\<cdot>u) x = \<bottom>" sorry
+    hence "aExp e\<cdot>u \<sqsubseteq> env_delete x ae" using `aExp e\<cdot>u \<sqsubseteq> ae` by (metis below_env_deleteI)
+    moreover
+
+    {
+    fix x' e'
+    assume "map_of \<Gamma> x' = Some e'" and "x' \<noteq> x"
+    moreover
+    assume "x' \<in> edom (prognosis (env_delete x ae) u (delete x \<Gamma>, e, Upd x # S))"
+    hence "x' \<in> edom (prognosis ae a (\<Gamma>, Var x, S))" using edom_mono[OF *]..
+    ultimately
+    have "fup\<cdot>(aExp e')\<cdot>(ae x') \<sqsubseteq> ae" using thunk by auto
+    moreover
+    have "(fup\<cdot>(aExp e')\<cdot>(ae x')) x = \<bottom>" sorry
+    ultimately
+    have "fup\<cdot>(aExp e')\<cdot>(ae x') \<sqsubseteq> env_delete x ae" sorry
+    }
+    moreover
+
+    have "const_on ae (ap S) (up\<cdot>0)" using thunk by auto
+    hence "const_on (env_delete x ae) (ap S) (up\<cdot>0)" using `x \<notin>  ap S`
+      by (auto simp add: const_on_def env_delete_def)
+    ultimately
+
+    have "consistent (env_delete x ae, env_delete x ce, u) (delete x \<Gamma>, e, Upd x # S)" using thunk
+      by (auto simp add: join_below_iff insert_absorb elim:below_trans)
+     
+    moreover
+    
+    {
+    from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>u` once
+    have "map_of (map_transform rhsExpand (env_u_com ae ce) (map_transform ccTransform ae \<Gamma>)) x = Some (Aeta_expand u (transform u e))"
+      by (simp add: map_of_map_transform)
+    hence "(map_transform rhsExpand (env_u_com ae ce) (map_transform ccTransform ae \<Gamma>), Var x, restr_stack (edom ae) S) \<Rightarrow>\<^sub>G
+           (delete x (map_transform rhsExpand (env_u_com ae ce) (map_transform ccTransform ae \<Gamma>)), Aeta_expand u (ccTransform u e), Upd x # restr_stack (edom ae) S)"
+        by (auto simp add: env_u_com_delete  map_transform_delete delete_map_transform_env_delete insert_absorb)
+    also
+    have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (delete x (map_transform rhsExpand (env_u_com ae ce) (map_transform ccTransform ae \<Gamma>)), Aeta_expand u (ccTransform u e), restr_stack (edom ae) S)"
+      by (rule r_into_rtranclp, rule)
+    also
+    have "\<dots> \<Rightarrow>\<^sub>G\<^sup>* (delete x (map_transform rhsExpand (env_u_com ae ce) (map_transform ccTransform ae \<Gamma>)), ccTransform u e, restr_stack (edom ae) S)"
+      by (intro normal_trans Aeta_expand_correct `Astack (restr_stack (edom ae) S) \<sqsubseteq> u`)
+    finally(rtranclp_trans)
+    have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* conf_transform (env_delete x ae, env_delete x ce, u) (delete x \<Gamma>, e, Upd x # S)"
+      by (auto simp add: env_u_com_delete  map_transform_delete delete_map_transform_env_delete insert_absorb)
+    }
+    ultimately
+    show ?thesis by (blast del: consistentI consistentE)
+
+
+  next
+    case many
+    have *: "prognosis ae 0 (delete x \<Gamma>, e, Upd x # S) \<sqsubseteq> prognosis ae a (\<Gamma>, Var x, S)" sorry
+
+    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 * thunk by (auto elim: below_trans)
+    hence "consistent (ae, ce, 0) (delete x \<Gamma>, e, Upd x # S)" using thunk  `aExp e\<cdot>u \<sqsubseteq> ae` `u = 0` edom_mono[OF *]
+      by (auto simp add: join_below_iff)
+    moreover
+    from  `map_of \<Gamma> x = Some e` `ae x = up\<cdot>0` many
+    have "map_of (map_transform rhsExpand (env_u_com ae ce) (map_transform ccTransform ae \<Gamma>)) x = Some (transform 0 e)"
+      by (simp add: map_of_map_transform)
+    with `\<not> isLam e`
+    have "conf_transform (ae, ce, a) (\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G conf_transform (ae, ce, 0) (delete x \<Gamma>, e, Upd x # S)"
+      by (auto simp add: map_transform_delete intro!: step.intros)
+    ultimately
+    show ?thesis by (blast del: consistentI consistentE)
+  next
+
+
+
+
+
+
+end
index b259d9c..8fb15ad 100644 (file)
@@ -102,6 +102,26 @@ next
   qed
 qed
 
+fun up2option :: "'a::cpo\<^sub>\<bottom> \<Rightarrow> 'a option"
+  where "up2option Ibottom = None"
+  |     "up2option (Iup a) = Some a"
+
+lemma up2option_simps[simp]:
+  "up2option \<bottom> = None"
+  "up2option (up\<cdot>x) = Some x"
+  unfolding up_def by (simp_all add: cont_Iup inst_up_pcpo)
+
+fun option2up :: "'a option \<Rightarrow> 'a::cpo\<^sub>\<bottom>"
+  where "option2up None = \<bottom>"
+  |     "option2up (Some a) = up\<cdot>a"
+
+lemma option2up_up2option[simp]:
+  "option2up (up2option x) = x"
+  by (cases x) auto
+lemma up2option_option2up[simp]:
+  "up2option (option2up x) = x"
+  by (cases x) auto
+
 subsubsection {* Composition of fun and cfun *}
 
 lemma cont2cont_comp [simp, cont2cont]:
index 4145437..0352326 100644 (file)
@@ -228,7 +228,42 @@ lemma fup_eqvt[eqvt]: "\<pi> \<bullet> fup = fup"
   apply (simp add: permute_self)
   done
 
-subsubsection {* Instance for @{type u} *}
+subsubsection {* Instance for @{type lift} *}
+
+instantiation lift :: (pt) pt
+begin
+  definition "p \<bullet> (x :: 'a lift) = case_lift \<bottom> (\<lambda> x. Def (p \<bullet> x)) x"
+  instance
+  apply default
+  apply (case_tac x) apply (auto simp add: permute_lift_def)
+  apply (case_tac x) apply (auto simp add: permute_lift_def)
+  done
+end
+
+instance lift :: (pt) cont_pt
+proof default
+  fix p
+  (* Fighting eta contraction... *)
+  have "permute p = (\<lambda> x. case_lift \<bottom> (\<lambda> x. Def (p \<bullet> x)) (x::'a lift))" 
+    by (rule ext, rule permute_lift_def)
+  moreover have "cont (\<lambda> x. case_lift \<bottom> (\<lambda> x. Def (p \<bullet> x)) (x::'a lift))" by simp
+  ultimately show "cont (permute p :: 'a lift \<Rightarrow> 'a lift)" by simp
+qed
+
+instance lift :: (pt) pcpo_pt by default
+
+instance lift :: (pure) pure
+  apply default
+  apply (case_tac x) apply (auto simp add: permute_lift_def permute_pure)
+  done  
+
+lemma Def_eqvt[eqvt]: "\<pi> \<bullet> (Def x) = Def (\<pi> \<bullet> x)"
+  by (simp add: permute_lift_def)
+
+lemma case_lift_eqvt[eqvt]: "\<pi> \<bullet> case_lift d f x = case_lift (\<pi> \<bullet> d) (\<pi> \<bullet> f) (\<pi> \<bullet> x)"
+  by (cases x) (auto simp add: permute_self)
+
+subsubsection {* Instance for @{type prod} *}
 
 instance prod :: (cont_pt, cont_pt) cont_pt
 proof default
index 0b2771a..1a988cb 100644 (file)
@@ -127,6 +127,13 @@ lemma case_option_eqvt[eqvt]:
   "\<pi> \<bullet> case_option d f x = case_option (\<pi> \<bullet> d) (\<pi> \<bullet> f) (\<pi> \<bullet> x)"
   by(cases x)(simp_all)
 
+lemma supp_option_eqvt:
+  "supp (case_option d f x) \<subseteq> supp d \<union> supp f \<union> supp x"
+  apply (cases x)
+  apply (auto simp add: supp_Some )
+  apply (metis (mono_tags) Un_iff subsetCE supp_fun_app)
+  done
+
 lemma funpow_eqvt[simp,eqvt]:
   "\<pi> \<bullet> ((f :: 'a \<Rightarrow> 'a::pt) ^^ n) = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> n)"
  apply (induct n)
diff --git a/Launchbury/SestoftGC.thy b/Launchbury/SestoftGC.thy
new file mode 100644 (file)
index 0000000..b75326a
--- /dev/null
@@ -0,0 +1,34 @@
+theory SestoftGC
+imports Sestoft 
+begin
+
+inductive gc_step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightarrow>\<^sub>G" 50) where
+  normal:  "c \<Rightarrow> c' \<Longrightarrow> c \<Rightarrow>\<^sub>G c'"
+| drop:    "(\<Gamma>, e, S) \<Rightarrow>\<^sub>G (restrictA V \<Gamma>, e, S)"
+| dropUpd: "(\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (\<Gamma>, e, S)"
+
+lemmas gc_step_intros[intro] =
+  normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
+  normal[OF step.intros(4)] normal[OF step.intros(5)] drop dropUpd
+
+
+abbreviation gc_steps (infix "\<Rightarrow>\<^sub>G\<^sup>*" 50) where "gc_steps \<equiv> gc_step\<^sup>*\<^sup>*"
+
+lemma var_onceI:
+  assumes "map_of \<Gamma> x = Some e"
+  shows "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e , S)"
+proof-
+  from assms 
+  have "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e , Upd x # S)"..
+  moreover
+  have "\<dots> \<Rightarrow>\<^sub>G  (delete x \<Gamma>, e , S)"..
+  ultimately
+  show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
+qed
+
+lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c \<Rightarrow>\<^sub>G\<^sup>* c'"
+  by (induction rule:rtranclp_induct) (auto dest: normal)
+
+
+end
+
diff --git a/Launchbury/Set_Cpo.thy b/Launchbury/Set_Cpo.thy
new file mode 100644 (file)
index 0000000..93abcab
--- /dev/null
@@ -0,0 +1,38 @@
+theory Set_Cpo
+imports HOLCF
+begin
+
+instantiation set :: (type) below
+begin
+  definition below_set where "op \<sqsubseteq> = op \<subseteq>"
+instance..  
+end
+
+instance set :: (type) po
+  by default (auto simp add: below_set_def)
+
+lemma is_lub_fun:
+  "S <<| \<Union>S"
+  by(auto simp add: is_lub_def below_set_def is_ub_def)
+  
+instance set  :: (type) cpo
+  by default (rule exI, rule is_lub_fun)
+
+lemma minimal_set: "{} \<sqsubseteq> S"
+  unfolding below_set_def by simp
+
+instance set  :: (type) pcpo
+  by default (rule+, rule minimal_set)
+
+lemma set_contI:
+  assumes  "\<And> S. f (\<Union>S) = \<Union> (f ` S)"
+  shows "cont f"
+proof(rule contI)
+  case (goal1 Y)
+  have "f (\<Squnion> i. Y i) = \<Union> (range (\<lambda>i. f (Y i)))" 
+    using assms by (metis Set_Cpo.is_lub_fun image_image lub_eqI)
+  with is_lub_fun
+  show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion> i. Y i)" by metis
+qed
+
+end
diff --git a/Launchbury/Set_Cpo_Nominal.thy b/Launchbury/Set_Cpo_Nominal.thy
new file mode 100644 (file)
index 0000000..7f018d0
--- /dev/null
@@ -0,0 +1,11 @@
+theory Set_Cpo_Nominal
+imports Set_Cpo "Nominal-HOLCF"
+begin
+
+instance set :: (pt) cont_pt
+  apply default
+  apply (rule set_contI)
+  apply perm_simp
+  apply (simp add : permute_set_eq_image)
+  done
+end
index 172b064..65dab77 100644 (file)
@@ -1,5 +1,5 @@
 theory TransformTools
-imports "Nominal-HOLCF" Terms Substitution
+imports "Nominal-HOLCF" Terms Substitution Env
 begin
 
 default_sort type
@@ -42,6 +42,10 @@ lemma map_transform_delete:
   "map_transform t ae (delete x \<Gamma>) = delete x (map_transform t ae \<Gamma>)"
   unfolding map_transform_def by (simp add: map_ran_delete)
 
+lemma delete_map_transform_env_delete:
+  "delete x (map_transform t (env_delete x ae) \<Gamma>) = delete x (map_transform t ae \<Gamma>)"
+  unfolding map_transform_def by (induction \<Gamma>) auto
+
 lemma map_transform_Nil:
   "map_transform t ae [] = []"
   unfolding map_transform_def by simp
@@ -87,7 +91,7 @@ lemma subst_map_transform:
   done
 
 locale supp_bounded_transform = 
-  fixes trans :: "'a::pure_cont_pt \<Rightarrow> exp \<Rightarrow> exp"
+  fixes trans :: "'a::cont_pt \<Rightarrow> exp \<Rightarrow> exp"
   assumes supp_trans: "supp (trans a e) \<subseteq> supp e"
 begin
   lemma supp_lift_transform: "supp (lift_transform trans a e) \<subseteq> supp e"