7d3919efb11cf87087b4944b311e0959df539a17
[darcs-mirror-isa-launchbury.git] / Launchbury / ArityConsistent.thy
1 theory ArityConsistent
2 imports  CardinalityAnalysisSpec ArityStack ArityAnalysisStack
3 begin
4
5 context CorrectArityAnalysisLet
6 begin
7
8 type_synonym astate = "(AEnv \<times> Arity \<times> Arity list)"
9
10 inductive stack_consistent :: "Arity list \<Rightarrow> stack \<Rightarrow> bool"
11   where 
12     "stack_consistent [] []"
13   | "Astack S \<sqsubseteq> a \<Longrightarrow> stack_consistent as S \<Longrightarrow> stack_consistent (a#as) (Alts e1 e2 # S)"
14   | "stack_consistent as S \<Longrightarrow> stack_consistent as (Upd x # S)"
15   | "stack_consistent as S \<Longrightarrow> stack_consistent as (Arg x # S)"
16 inductive_simps stack_consistent_foo[simp]:
17   "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)"
18 inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"
19
20 inductive a_consistent :: "astate \<Rightarrow> conf \<Rightarrow> bool" where
21   a_consistentI:
22   "edom ae \<subseteq> domA \<Gamma> \<union> upds S
23   \<Longrightarrow> heap_upds_ok (\<Gamma>, S)
24   \<Longrightarrow> Astack S \<sqsubseteq> a
25   \<Longrightarrow> (ABinds \<Gamma>\<cdot>ae \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae
26   \<Longrightarrow> stack_consistent as S
27   \<Longrightarrow> a_consistent (ae, a, as) (\<Gamma>, e, S)"  
28 inductive_cases a_consistentE: "a_consistent (ae, a, as) (\<Gamma>, e, S)"
29
30 lemma a_consistent_restrictA:
31   assumes "a_consistent (ae, a, as) (\<Gamma>, e, S)"
32   assumes "edom ae \<subseteq> V"
33   shows "a_consistent (ae, a, as) (restrictA V \<Gamma>, e, S)"
34 proof-
35   have "domA \<Gamma> \<inter> V \<union> upds S \<subseteq> domA \<Gamma> \<union> upds S" by auto
36   note * = below_trans[OF env_restr_mono2[OF this]]
37   
38   show " a_consistent (ae, a, as) (restrictA V \<Gamma>, e, S)"
39     using assms
40     by (auto simp add: a_consistent.simps env_restr_join join_below_iff ABinds_restrict_edom
41                   intro: * below_trans[OF env_restr_mono[OF ABinds_restrict_below]])
42 qed
43
44 lemma a_consistent_edom_subsetD:
45   "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> edom ae \<subseteq> domA \<Gamma> \<union> upds S"
46   by (rule a_consistentE)
47
48 lemma a_consistent_stackD:
49   "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> Astack S \<sqsubseteq> a"
50   by (rule a_consistentE)
51
52 lemma a_consistent_heap_upds_okD:
53   "a_consistent (ae, a, as) (\<Gamma>, e, S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)"
54   by (rule a_consistentE)
55
56 lemma a_consistent_app\<^sub>1:
57   "a_consistent (ae, a, as) (\<Gamma>, App e x, S) \<Longrightarrow> a_consistent (ae, inc\<cdot>a, as) (\<Gamma>, e, Arg x # S)"
58   by (auto simp add: join_below_iff env_restr_join a_consistent.simps
59            dest!: below_trans[OF env_restr_mono[OF Aexp_App]]
60            elim: below_trans)
61
62 lemma a_consistent_app\<^sub>2:
63   assumes "a_consistent (ae, a, as) (\<Gamma>, (Lam [y]. e), Arg x # S)"
64   shows "a_consistent (ae, (pred\<cdot>a), as) (\<Gamma>, e[y::=x], S)"
65 proof-
66   have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` (domA \<Gamma> \<union> upds S)  \<sqsubseteq> (env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<squnion> esing x\<cdot>(up\<cdot>0)) f|` (domA \<Gamma> \<union> upds S)" by (rule env_restr_mono[OF Aexp_subst])
67   also have "\<dots> =  env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) f|` (domA \<Gamma> \<union> upds S) \<squnion> esing x\<cdot>(up\<cdot>0) f|` (domA \<Gamma> \<union> upds S)" by (simp add: env_restr_join)
68   also have "env_delete y ((Aexp e)\<cdot>(pred\<cdot>a)) \<sqsubseteq> Aexp (Lam [y]. e)\<cdot>a" by (rule Aexp_Lam)
69   also have "\<dots> f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" using assms  by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
70   also have "esing x\<cdot>(up\<cdot>0) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" using assms
71     by (cases "x\<in>edom ae") (auto simp add: env_restr_join join_below_iff a_consistent.simps)
72   also have "ae \<squnion> ae = ae" by simp
73   finally
74   have "Aexp (e[y::=x])\<cdot>(pred\<cdot>a) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by this simp_all
75   thus ?thesis using assms
76     by (auto elim: below_trans edom_mono  simp add: join_below_iff env_restr_join a_consistent.simps)
77 qed
78
79 lemma a_consistent_thunk_0:
80   assumes "a_consistent (ae, a, as) (\<Gamma>, Var x, S)"
81   assumes "map_of \<Gamma> x = Some e"
82   assumes "ae x = up\<cdot>0"
83   shows "a_consistent (ae, 0, as) (delete x \<Gamma>, e, Upd x # S)"
84 proof-
85   from assms(2)
86   have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
87
88   from assms(3)
89   have [simp]: "x \<in> edom ae" by (auto simp add: edom_def)
90
91   have "x \<in> domA \<Gamma>" by (metis assms(2) domI dom_map_of_conv_domA)
92   hence [simp]: "insert x (domA \<Gamma> - {x} \<union> upds S)  = (domA \<Gamma> \<union> upds S)"
93     by auto
94
95   from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>0`
96   have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>0 = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
97   moreover have "(\<dots> \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
98     using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
99   ultimately have "((ABinds (delete x \<Gamma>))\<cdot>ae \<squnion> Aexp e\<cdot>0 \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by simp
100   then
101   show ?thesis
102      using `ae x = up\<cdot>0` assms(1)
103      by (auto simp add: join_below_iff env_restr_join  a_consistent.simps)
104 qed
105
106 lemma a_consistent_thunk_once:
107   assumes "a_consistent (ae, a, as) (\<Gamma>, Var x, S)"
108   assumes "map_of \<Gamma> x = Some e"
109   assumes [simp]: "ae x = up\<cdot>u"
110   shows "a_consistent (env_delete x ae, u, as) (delete x \<Gamma>, e, S)"
111 proof-
112   from assms(2)
113   have [simp]: "x \<in> domA \<Gamma>" by (metis domI dom_map_of_conv_domA)
114
115   from assms(1) have "Aexp (Var x)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
116   from fun_belowD[where x = x, OF this] 
117   have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> up\<cdot>u" by simp
118   from below_trans[OF Aexp_Var this]
119   have "a \<sqsubseteq> u" by simp
120
121   from assms(1)
122   have "x \<notin> upds S" by (auto simp add: a_consistent.simps elim!: heap_upds_okE)
123   hence [simp]: "(- {x} \<inter> (domA \<Gamma> \<union> upds S)) = (domA \<Gamma> - {x} \<union> upds S)" by auto
124
125   have "Astack S \<sqsubseteq> u" using assms(1) `a \<sqsubseteq> u`
126     by (auto elim: below_trans simp add: a_consistent.simps)
127   
128   from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
129   have "ABinds (delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
130   moreover
131   have "(\<dots> \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
132     using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
133   ultimately
134   have "((ABinds (delete x \<Gamma>))\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by simp
135   hence "((ABinds (delete x \<Gamma>))\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
136     by (auto simp add: join_below_iff env_restr_join elim:  below_trans[OF env_restr_mono[OF monofun_cfun_arg[OF env_delete_below_arg]]])
137   hence "env_delete x (((ABinds (delete x \<Gamma>))\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S)) \<sqsubseteq> env_delete x ae"
138     by (rule env_delete_mono)
139   hence "(((ABinds (delete x \<Gamma>))\<cdot>(env_delete x ae) \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA (delete x \<Gamma>) \<union> upds S)) \<sqsubseteq> env_delete x ae"
140     by (simp add: env_delete_restr)
141   then
142   show ?thesis
143      using `ae x = up\<cdot>u` `Astack S \<sqsubseteq> u` assms(1)
144      by (auto simp add: join_below_iff env_restr_join  a_consistent.simps elim : below_trans)
145 qed
146
147 lemma a_consistent_lamvar:
148   assumes "a_consistent (ae, a, as) (\<Gamma>, Var x, S)"
149   assumes "map_of \<Gamma> x = Some e"
150   assumes [simp]: "ae x = up\<cdot>u"
151   shows "a_consistent (ae, u, as) ((x,e)# delete x \<Gamma>, e, S)"
152 proof-
153   have [simp]: "x \<in> domA \<Gamma>" by (metis assms(2) domI dom_map_of_conv_domA)
154   have [simp]: "insert x (domA \<Gamma> \<union> upds S) = (domA \<Gamma> \<union> upds S)" 
155     by auto
156
157   from assms(1) have "Aexp (Var x)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
158   from fun_belowD[where x = x, OF this] 
159   have "(Aexp (Var x)\<cdot>a) x \<sqsubseteq> up\<cdot>u" by simp
160   from below_trans[OF Aexp_Var this]
161   have "a \<sqsubseteq> u" by simp
162
163   have "Astack S \<sqsubseteq> u" using assms(1) `a \<sqsubseteq> u`
164     by (auto elim: below_trans simp add: a_consistent.simps)
165   
166   from Abinds_reorder1[OF `map_of \<Gamma> x = Some e`] `ae x = up\<cdot>u`
167   have "ABinds ((x,e) # delete x \<Gamma>)\<cdot>ae \<squnion> Aexp e\<cdot>u = ABinds \<Gamma>\<cdot>ae" by (auto intro: join_comm)
168   moreover
169   have "(\<dots> \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
170     using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
171   ultimately
172   have "((ABinds ((x,e) # delete x \<Gamma>))\<cdot>ae \<squnion> Aexp e\<cdot>u \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by simp
173   then
174   show ?thesis
175      using `ae x = up\<cdot>u` `Astack S \<sqsubseteq> u` assms(1)
176      by (auto simp add: join_below_iff env_restr_join  a_consistent.simps)
177 qed
178
179 lemma 
180   assumes "a_consistent (ae, a, as) (\<Gamma>, e, Upd x # S)"
181   and "x \<in> edom ae"
182   shows a_consistent_var\<^sub>2: "a_consistent (ae, a, as) ((x, e) # \<Gamma>, e, S)" 
183     and a_consistent_UpdD: "ae x = up\<cdot>0""a = 0"
184     using assms
185     by (auto simp add: join_below_iff env_restr_join a_consistent.simps 
186                elim:below_trans[OF env_restr_mono[OF ABinds_delete_below]])
187
188 lemma a_consistent_let:
189   assumes "a_consistent (ae, a, as) (\<Gamma>, Let \<Delta> e, S)"
190   assumes "atom ` domA \<Delta> \<sharp>* \<Gamma>"
191   assumes "atom ` domA \<Delta> \<sharp>* S"
192   assumes "edom ae \<inter> domA \<Delta> = {}"
193   shows "a_consistent (Aheap \<Delta> e\<cdot>a \<squnion> ae, a, as) (\<Delta> @ \<Gamma>, e, S)"
194 proof-
195   txt {*
196     First some boring stuff about scope:
197   *}
198   
199   have [simp]: "\<And> S. S \<subseteq> domA \<Delta> \<Longrightarrow> ae f|` S = \<bottom>" using assms(4) by auto
200   have [simp]: "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a)"
201     by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
202
203   have [simp]: "Aheap \<Delta> e\<cdot>a f|` domA \<Gamma> = \<bottom>"
204     using fresh_distinct[OF assms(2)]
205     by (auto intro: env_restr_empty dest!: set_mp[OF edom_Aheap])
206
207   have [simp]: "ABinds \<Gamma>\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) = ABinds \<Gamma>\<cdot>ae"
208     by (rule Abinds_env_restr_cong) (simp add: env_restr_join)
209
210   have [simp]: "ABinds \<Gamma>\<cdot>ae f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S)  = ABinds \<Gamma>\<cdot>ae f|` (domA \<Gamma> \<union> upds S)" 
211     using fresh_distinct_fv[OF assms(2)]
212     by (auto intro: env_restr_cong dest!: set_mp[OF edom_AnalBinds])
213
214   have [simp]: "AEstack as S f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S) = AEstack as S f|` (domA \<Gamma> \<union> upds S)" 
215     using fresh_distinct_fv[OF assms(3)]
216     by (auto intro: env_restr_cong dest!:  set_mp[OF edom_AEstack])
217
218   have [simp]: "Aexp (Let \<Delta> e)\<cdot>a f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S) = Aexp (Terms.Let \<Delta> e)\<cdot>a f|` (domA \<Gamma> \<union> upds S)"
219     by (rule env_restr_cong) (auto dest!: set_mp[OF Aexp_edom])
220   
221   have [simp]: "Aheap \<Delta> e\<cdot>a f|` (domA \<Delta> \<union> domA \<Gamma> \<union> upds S) = Aheap \<Delta> e\<cdot>a "
222     by (rule env_restr_useless) (auto dest!: set_mp[OF edom_Aheap])
223
224   have "((ABinds \<Gamma>)\<cdot>ae \<squnion> AEstack as S) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
225   moreover
226   have" Aexp (Let \<Delta> e)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"  using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
227   moreover
228   have "ABinds \<Delta>\<cdot>(Aheap \<Delta> e\<cdot>a) \<squnion> Aexp e\<cdot>a \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> Aexp (Let \<Delta> e)\<cdot>a" by (rule Aexp_Let)
229   ultimately
230   have "(ABinds (\<Delta> @ \<Gamma>)\<cdot>(Aheap \<Delta> e\<cdot>a \<squnion> ae) \<squnion> Aexp e\<cdot>a \<squnion> AEstack as S) f|` (domA (\<Delta>@\<Gamma>) \<union> upds S) \<sqsubseteq> Aheap \<Delta> e\<cdot>a \<squnion> ae"
231     by (auto 4 4 simp add: env_restr_join Abinds_append_disjoint[OF fresh_distinct[OF assms(2)]] join_below_iff
232                  simp del: join_comm
233                  elim: below_trans below_trans[OF env_restr_mono])
234   moreover
235   note fresh_distinct[OF assms(2)]
236   moreover
237   from fresh_distinct_fv[OF assms(3)]
238   have  "domA \<Delta> \<inter> upds S = {}" by (auto dest!: set_mp[OF ups_fv_subset])
239   ultimately
240   show ?thesis using assms(1)
241     by (auto simp add: a_consistent.simps dest!: set_mp[OF edom_Aheap] intro: heap_upds_ok_append)
242 qed
243
244 lemma a_consistent_if\<^sub>1:
245   assumes "a_consistent (ae, a, as) (\<Gamma>, scrut ? e1 : e2, S)"
246   shows "a_consistent (ae, 0, a#as) (\<Gamma>, scrut, Alts e1 e2 # S)"
247 proof-
248   from assms
249   have "Aexp (scrut ? e1 : e2)\<cdot>a f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae" by (auto simp add: a_consistent.simps env_restr_join join_below_iff)
250   hence "(Aexp scrut\<cdot>0 \<squnion> Aexp e1\<cdot>a \<squnion> Aexp e2\<cdot>a) f|` (domA \<Gamma> \<union> upds S) \<sqsubseteq> ae"
251     by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]])
252   thus ?thesis
253     using assms
254     by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
255 qed
256
257 lemma a_consistent_if\<^sub>2:
258   assumes "a_consistent (ae, a, a'#as') (\<Gamma>, Bool b, Alts e1 e2 # S)"
259   shows "a_consistent (ae, a', as') (\<Gamma>, if b then e1 else e2, S)"
260 using assms by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
261
262 lemma a_consistent_alts_on_stack:
263   assumes "a_consistent (ae, a, as) (\<Gamma>, Bool b, Alts e1 e2 # S)"
264   obtains a' as' where "as = a' # as'" "a = 0"
265 using assms by (auto simp add: a_consistent.simps)
266
267 lemma closed_a_consistent:
268   "fv e = ({}::var set) \<Longrightarrow> a_consistent (\<bottom>, 0, []) ([], e, [])"
269   by (auto simp add: edom_empty_iff_bot a_consistent.simps  dest!: set_mp[OF Aexp_edom])
270
271 end
272
273 end