d0574cc601f3d46eb0f2ac92d6e1e73ae73fcb7d
[darcs-mirror-isa-launchbury.git] / Launchbury / CoCallAnalysisBinds.thy
1 theory CoCallAnalysisBinds
2 imports CoCallAnalysis AEnv  "AList-Utils-HOLCF" "Arity-Nominal""CoCallGraph-Nominal"
3 begin
4
5 context CoCallAnalysis
6 begin
7 definition ccBind :: "var \<Rightarrow> exp \<Rightarrow> ((AEnv \<times> CoCalls) \<rightarrow> CoCalls)"
8   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))"
9 (* paper has:  \<or> ae v = up\<cdot>0, but that is not monotone! But should give the same result. *)
10
11 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))"
12   unfolding ccBind_def
13   apply (rule cfun_beta_Pair)
14   apply (rule cont_if_else_above)
15   apply simp
16   apply simp
17   apply (auto dest: set_mp[OF ccField_cc_restr])[1]
18   (* Abstraction broken! Fix this. *)
19   apply (case_tac p, auto, transfer, auto)[1]
20   apply (rule adm_subst[OF cont_snd])
21   apply (rule admI, thin_tac "chain ?x", transfer, auto)
22   done
23
24 lemma ccBind_strict[simp]: "ccBind v e \<cdot> \<bottom> = \<bottom>"
25   by (auto simp add: inst_prod_pcpo ccBind_eq simp del: Pair_strict)
26
27 definition ccBinds :: "heap \<Rightarrow> ((AEnv \<times> CoCalls) \<rightarrow> CoCalls)"
28   where "ccBinds \<Gamma> = (\<Lambda> i. (\<Squnion>v\<mapsto>e\<in>map_of \<Gamma>. ccBind v e\<cdot>i))"
29
30 lemma ccBinds_eq:
31   "ccBinds \<Gamma>\<cdot>i = (\<Squnion>v\<mapsto>e\<in>map_of \<Gamma>. ccBind v e\<cdot>i)"
32   unfolding ccBinds_def
33   by simp
34
35 lemma ccBinds_strict[simp]: "ccBinds \<Gamma>\<cdot>\<bottom>=\<bottom>"
36   unfolding ccBinds_eq
37   by (cases "\<Gamma> = []") simp_all
38
39 lemma ccBinds_strict'[simp]: "ccBinds \<Gamma>\<cdot>(\<bottom>,\<bottom>)=\<bottom>"
40   by (metis CoCallAnalysis.ccBinds_strict Pair_bottom_iff)
41
42 lemma ccBinds_reorder1:
43   assumes "map_of \<Gamma> v = Some e"
44   shows "ccBinds \<Gamma> = ccBind v e \<squnion> ccBinds (delete v \<Gamma>)"
45 proof-
46   from assms 
47   have "map_of \<Gamma> = map_of ((v,e) # delete v \<Gamma>)" by (metis map_of_delete_insert)
48   thus ?thesis
49     by (auto intro: cfun_eqI simp add: ccBinds_eq delete_set_none)
50 qed
51
52 lemma ccBinds_Nil[simp]:
53   "ccBinds [] = \<bottom>"
54   unfolding ccBinds_def by simp
55
56 lemma ccBinds_Cons[simp]:
57    "ccBinds ((x,e)#\<Gamma>) = ccBind x e \<squnion> ccBinds (delete x \<Gamma>)"
58    by (subst ccBinds_reorder1[where v = x and e = e]) auto
59
60 lemma ccBind_below_ccBinds: "map_of \<Gamma> x = Some e \<Longrightarrow> ccBind x e\<cdot>ae \<sqsubseteq> (ccBinds \<Gamma>\<cdot>ae)"
61   by (auto simp add: ccBinds_eq)
62
63 definition ccBindsExtra :: "heap \<Rightarrow> ((AEnv \<times> CoCalls) \<rightarrow> CoCalls)"
64   where "ccBindsExtra \<Gamma> = (\<Lambda> i.  snd i \<squnion> ccBinds \<Gamma> \<cdot> i  \<squnion> (\<Squnion>x\<mapsto>e\<in>map_of \<Gamma>. ccProd (fv e) (ccNeighbors x (snd i))))"
65
66
67 lemma ccBindsExtra_simp: "ccBindsExtra \<Gamma> \<cdot> i = snd i \<squnion> ccBinds \<Gamma> \<cdot> i \<squnion> (\<Squnion>x\<mapsto>e\<in>map_of \<Gamma>. ccProd (fv e) (ccNeighbors x (snd i)))"
68   unfolding ccBindsExtra_def by simp
69
70 lemma ccBindsExtra_strict[simp]: "ccBindsExtra \<Gamma> \<cdot> \<bottom> = \<bottom>"
71   by (auto simp add: ccBindsExtra_simp inst_prod_pcpo simp del: Pair_strict)
72
73 end
74
75 lemma ccBind_eqvt[eqvt]: "\<pi> \<bullet> (CoCallAnalysis.ccBind cccExp x e) = CoCallAnalysis.ccBind (\<pi> \<bullet> cccExp) (\<pi> \<bullet> x) (\<pi> \<bullet> e)"
76 proof-
77   {
78   fix \<pi> ae G
79   have "\<pi> \<bullet> ((CoCallAnalysis.ccBind cccExp x e) \<cdot> (ae,G)) = CoCallAnalysis.ccBind (\<pi> \<bullet> cccExp) (\<pi> \<bullet> x) (\<pi> \<bullet> e) \<cdot> (\<pi> \<bullet> ae, \<pi> \<bullet> G)"
80     unfolding CoCallAnalysis.ccBind_eq
81     by perm_simp (simp add: Abs_cfun_eqvt)
82   }
83   thus ?thesis by (auto intro: cfun_eqvtI)
84 qed
85
86 lemma ccBinds_eqvt[eqvt]: "\<pi> \<bullet> (CoCallAnalysis.ccBinds cccExp \<Gamma>) = CoCallAnalysis.ccBinds (\<pi> \<bullet> cccExp) (\<pi> \<bullet> \<Gamma>)"
87   apply (rule cfun_eqvtI)
88   unfolding CoCallAnalysis.ccBinds_eq
89   apply (perm_simp) 
90   apply rule
91   done
92
93 lemma ccBindsExtra_eqvt[eqvt]: "\<pi> \<bullet> (CoCallAnalysis.ccBindsExtra cccExp \<Gamma>) = CoCallAnalysis.ccBindsExtra (\<pi> \<bullet> cccExp) (\<pi> \<bullet> \<Gamma>)"
94   by (rule cfun_eqvtI) (simp add: CoCallAnalysis.ccBindsExtra_def)
95
96 lemma ccBind_cong[fundef_cong]:
97   "cccexp1 e = cccexp2 e \<Longrightarrow> CoCallAnalysis.ccBind cccexp1 x e = CoCallAnalysis.ccBind cccexp2 x e "
98   apply (rule cfun_eqI)
99   apply (case_tac xa)
100   apply (auto simp add: CoCallAnalysis.ccBind_eq)
101   done
102
103 lemma ccBinds_cong[fundef_cong]:
104   "\<lbrakk> (\<And> e. e \<in> snd ` set heap2 \<Longrightarrow> cccexp1 e = cccexp2 e); heap1 = heap2 \<rbrakk>
105       \<Longrightarrow> CoCallAnalysis.ccBinds cccexp1 heap1 = CoCallAnalysis.ccBinds cccexp2 heap2"
106   apply (rule cfun_eqI)
107   unfolding CoCallAnalysis.ccBinds_eq
108   apply (rule arg_cong[OF mapCollect_cong])
109   apply (rule arg_cong[OF ccBind_cong])
110   apply auto
111   by (metis imageI map_of_is_SomeD snd_conv)
112
113 lemma ccBindsExtra_cong[fundef_cong]:
114   "\<lbrakk> (\<And> e. e \<in> snd ` set heap2 \<Longrightarrow> cccexp1 e = cccexp2 e); heap1 = heap2 \<rbrakk>
115       \<Longrightarrow> CoCallAnalysis.ccBindsExtra cccexp1 heap1 = CoCallAnalysis.ccBindsExtra cccexp2 heap2"
116   apply (rule cfun_eqI)
117   unfolding CoCallAnalysis.ccBindsExtra_simp
118   apply (rule arg_cong2[OF ccBinds_cong mapCollect_cong]) 
119   apply simp+
120   done
121
122 end