c56d89fcc5351ac8a93018f40e7a340e7ee813c6
[darcs-mirror-isa-launchbury.git] / Launchbury / NoCardinalityAnalysis.thy
1 theory NoCardinalityAnalysis
2 imports CardinalityAnalysis
3 begin
4
5 locale NoCardinalityAnalysis = CorrectArityAnalysisLet +
6   assumes Aheap_thunk: "x \<in> thunks \<Gamma> \<Longrightarrow> (Aheap \<Gamma> e\<cdot>a) x = up\<cdot>0"
7 begin
8
9 definition a2c :: "Arity\<^sub>\<bottom> \<rightarrow> two" where "a2c = (\<Lambda> a. if a \<sqsubseteq> \<bottom> then \<bottom> else many)"
10 lemma a2c_simp: "a2c\<cdot>a = (if a \<sqsubseteq> \<bottom> then \<bottom> else many)"
11   unfolding a2c_def by (rule beta_cfun[OF cont_if_else_above]) auto
12
13
14 lemma a2c_eqvt[eqvt]: "\<pi> \<bullet> a2c = a2c"
15   unfolding a2c_def
16   apply perm_simp
17   apply (rule Abs_cfun_eqvt)
18   apply (rule cont_if_else_above)
19   apply auto
20   done
21
22 definition ae2ce :: "AEnv \<Rightarrow> (var \<Rightarrow> two)" where "ae2ce ae x = a2c\<cdot>(ae x)"
23
24 lemma ae2ce_cont: "cont ae2ce"
25   by (auto simp add: ae2ce_def) 
26 lemmas cont_compose[OF ae2ce_cont, cont2cont, simp]
27
28 lemma ae2ce_eqvt[eqvt]: "\<pi> \<bullet> ae2ce ae x = ae2ce (\<pi> \<bullet> ae) (\<pi> \<bullet> x)"
29   unfolding ae2ce_def by perm_simp rule
30
31 lemma ae2ce_to_env_restr: "ae2ce ae = (\<lambda>_ . many) f|` edom ae"
32   by (auto simp add: ae2ce_def lookup_env_restr_eq edom_def a2c_simp)
33
34 lemma edom_ae2ce[simp]: "edom (ae2ce ae) = edom ae"
35   unfolding edom_def
36   by (auto simp add: ae2ce_def  a2c_simp)
37
38
39 definition cHeap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> (var \<Rightarrow> two)"
40   where "cHeap \<Gamma> e = (\<Lambda> a. ae2ce (Aheap \<Gamma> e\<cdot>a))"
41 lemma cHeap_simp[simp]: "cHeap \<Gamma> e\<cdot>a = ae2ce (Aheap \<Gamma> e\<cdot>a)"
42   unfolding cHeap_def by simp
43
44 (*
45 lemma cHeap_eqvt[eqvt]: "\<pi> \<bullet> cHeap \<Gamma> e = cHeap (\<pi> \<bullet> \<Gamma>) (\<pi> \<bullet> e)"
46   unfolding cHeap_def
47   apply perm_simp
48   apply (rule Abs_cfun_eqvt)
49   apply simp
50   done
51 *)
52
53 sublocale CardinalityHeap Aexp Aheap cHeap
54   apply default
55 (*  apply (perm_simp, rule) *)
56   apply (erule Aheap_thunk)
57   apply simp
58   done
59   
60 (*
61 fun prognosis where 
62   "prognosis ae a (\<Gamma>, e, S) = ae2ce (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a) \<squnion> ((\<lambda>_. many) f|` ap S)"
63 *)
64
65 fun prognosis where 
66   "prognosis ae a (\<Gamma>, e, S) = ((\<lambda>_. many) f|` (edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp e\<cdot>a) \<union> ap S))"
67
68 lemma record_all_noop[simp]:
69   "record_call x\<cdot>((\<lambda>_. many) f|` S) = (\<lambda>_. many) f|` S"
70   by (auto simp add: record_call_def lookup_env_restr_eq)
71
72 sublocale CardinalityPrognosis prognosis.
73
74 sublocale CardinalityPrognosisCorrect prognosis
75 proof
76   case goal1 thus ?case by (simp cong: Abinds_env_restr_cong)
77 next
78   case goal2 thus ?case by (simp cong: Abinds_reorder)
79 next
80   case goal3 thus ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]])
81 next
82   case goal4 thus ?case by auto
83 next
84   case goal5 thus ?case
85     using edom_mono[OF Aexp_App] by (auto intro!: env_restr_mono2)
86 next
87   case goal6
88   from edom_mono[OF Aexp_App]
89   have "insert x (edom (Aexp e\<cdot>(inc\<cdot>a))) \<subseteq> edom (Aexp (App e x)\<cdot>a)" by auto
90   thus ?case by (auto intro: env_restr_mono2 )
91 next
92   case goal7
93   have "edom (Aexp e[y::=x]\<cdot>(pred\<cdot>a)) \<subseteq> insert x (edom (env_delete y (Aexp e\<cdot>(pred\<cdot>a))))"
94     by (auto dest: set_mp[OF edom_mono[OF Aexp_subst]] )
95   also have "\<dots> \<subseteq> insert x (edom (Aexp (Lam [y]. e)\<cdot>a))"
96     using edom_mono[OF Aexp_Lam] by auto
97   finally show ?case by (auto intro!: env_restr_mono2)
98 next
99   case goal8
100   thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal8(1)])
101 next
102   case goal9
103   thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF goal9(1)])
104 next
105   case goal10
106   have "fup\<cdot>(Aexp e)\<cdot>(ae x) \<sqsubseteq> Aexp e\<cdot>0" by (cases "ae x") (auto intro: monofun_cfun_arg)
107   from edom_mono[OF this]
108   show ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]])
109 next
110   case goal11
111   from `ae x = \<bottom>`
112   have "ABinds (delete x \<Gamma>)\<cdot>ae = ABinds \<Gamma>\<cdot>ae" by (rule ABinds_delete_bot)
113   thus ?case by simp
114 next
115   case goal12
116   from Aexp_Var[where n = a and x = x]
117   have "(Aexp (Var x)\<cdot>a) x \<noteq> \<bottom>" by auto
118   hence "x \<in> edom (Aexp (Var x)\<cdot>a)" by (simp add: edomIff)
119   thus ?case by simp
120 qed
121   
122 sublocale CardinalityPrognosisCorrectLet prognosis Aexp Aheap cHeap
123 proof
124   case goal1
125
126   from set_mp[OF goal1(3)] fresh_distinct[OF goal1(1)] fresh_distinct_fv[OF goal1(2)]
127   have  "ae f|` domA \<Delta> = \<bottom>"
128     by (auto dest: set_mp[OF ups_fv_subset])
129   hence [simp]: "ABinds \<Delta>\<cdot>(ae \<squnion> Aheap \<Delta> e\<cdot>a) = ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)" by (simp cong: Abinds_env_restr_cong add: env_restr_join)
130
131   from  fresh_distinct[OF goal1(1)]
132   have "Aheap \<Delta> e\<cdot>a f|` domA \<Gamma> = \<bottom>" by (auto dest!: set_mp[OF edom_Aheap])
133   hence [simp]: "ABinds \<Gamma>\<cdot>(ae \<squnion> Aheap \<Delta> e\<cdot>a) = ABinds \<Gamma>\<cdot>ae" by (simp cong: Abinds_env_restr_cong add: env_restr_join)
134   
135   have "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a)  = edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union>  edom (Aexp e\<cdot>a) "
136     by (simp add: Abinds_append_disjoint[OF fresh_distinct[OF goal1(1)]] Un_commute)
137   also have "\<dots> = edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a)"
138     by force
139   also have "\<dots> \<subseteq> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a)"
140     using  edom_mono[OF Aexp_Let] by force
141   also have "\<dots> = edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Let \<Delta> e)\<cdot>a)"
142     by auto
143   finally
144   have "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a)".
145   hence "edom (ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae)) \<union> edom (Aexp e\<cdot>a) \<union> ap S \<subseteq> edom (Aheap \<Delta> e\<cdot>a) \<union> edom (ABinds \<Gamma>\<cdot>ae) \<union> edom (Aexp (Terms.Let \<Delta> e)\<cdot>a) \<union> ap S" by auto
146   thus ?case by (simp add: ae2ce_to_env_restr env_restr_join2 Un_assoc[symmetric] env_restr_mono2)
147 qed
148
149 sublocale CardinalityPrognosisEdom prognosis Aexp Aheap
150   by default (auto dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF edom_AnalBinds])
151
152 end
153
154 end