838323c3789cc5233caa58d008d0170db17d7bcc
[darcs-mirror-isa-launchbury.git] / Launchbury / SestoftGC.thy
1 theory SestoftGC
2 imports Sestoft 
3 begin
4
5 inductive gc_step :: "(var list \<times> conf) \<Rightarrow> (var list \<times> conf) \<Rightarrow> bool" (infix "\<Rightarrow>\<^sub>G" 50) where
6   normal:  "c \<Rightarrow> c' \<Longrightarrow> (r, c) \<Rightarrow>\<^sub>G (r, c')"
7 | dropUpd: "(r, \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (x # r, \<Gamma>, e, S)"
8
9 lemmas gc_step_intros[intro] =
10   normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
11   normal[OF step.intros(4)] normal[OF step.intros(5)]  dropUpd
12
13
14 abbreviation gc_steps (infix "\<Rightarrow>\<^sub>G\<^sup>*" 50) where "gc_steps \<equiv> gc_step\<^sup>*\<^sup>*"
15 lemmas converse_rtranclp_into_rtranclp[of gc_step, OF _ r_into_rtranclp, trans]
16
17 lemma var_onceI:
18   assumes "map_of \<Gamma> x = Some e"
19   shows "(r, \<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (x#r, delete x \<Gamma>, e , S)"
20 proof-
21   from assms 
22   have "(r, \<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (r, delete x \<Gamma>, e , Upd x # S)"..
23   moreover
24   have "\<dots> \<Rightarrow>\<^sub>G  (x #r, delete x \<Gamma>, e , S)"..
25   ultimately
26   show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
27 qed
28
29 lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> (r, c) \<Rightarrow>\<^sub>G\<^sup>* (r, c')"
30   by (induction rule:rtranclp_induct)
31      (simp, metis normal rtranclp.rtrancl_into_rtrancl)
32
33 fun to_gc_conf :: "var list \<Rightarrow> conf \<Rightarrow> conf"
34   where "to_gc_conf r (\<Gamma>, e, S) = (restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S)"
35
36 lemma to_gc_conf_append[simp]:
37   "to_gc_conf (r@r') c = to_gc_conf r (to_gc_conf r' c)"
38   by (cases c) auto
39
40 lemma to_gc_conf_eqE[elim!]:
41   assumes  "to_gc_conf r c = (\<Gamma>, e, S)"
42   obtains \<Gamma>' S' where "c = (\<Gamma>', e, S')" and "\<Gamma> = restrictA (- set r) \<Gamma>'" and "S = restr_stack (- set r) S'"
43   using assms
44   by (cases c) auto
45
46 fun safe_hd :: "'a list \<Rightarrow> 'a option"
47  where  "safe_hd (x#_) = Some x"
48      |  "safe_hd [] = None"
49
50 lemma safe_hd_None[simp]: "safe_hd xs = None \<longleftrightarrow> xs = []"
51   by (cases xs) auto
52
53 abbreviation r_ok :: "(var list \<times> conf) \<Rightarrow> bool"
54   where "r_ok c \<equiv> set (fst c) \<subseteq> domA (fst (snd c)) \<union> upds (snd (snd (snd c)))"
55
56
57 lemma sestoftUnGCStack:
58   assumes "heap_upds_ok (\<Gamma>, S)"
59   assumes "set r \<subseteq> domA \<Gamma> \<union> upds S"
60   obtains \<Gamma>' S' where
61     "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
62     "heap_upds_ok (\<Gamma>', S')"
63     "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
64     "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
65     "set r \<subseteq> domA \<Gamma>' \<union> upds S'"
66 (*proof(atomize_elim)
67   show "\<exists>\<Gamma>' S'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S') \<and> heap_upds_ok (\<Gamma>', S') \<and> to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S') \<and> (\<not> isVal e \<or>  safe_hd S' = safe_hd (restr_stack (- set r) S'))"
68 *)
69 proof-
70   show ?thesis
71   proof(cases "isVal e")
72     case False
73     thus ?thesis using assms  by -(rule that, auto)
74   next
75     case True
76     from that assms 
77     show ?thesis
78     apply (atomize_elim)
79     proof(induction S arbitrary: \<Gamma>)
80       case Nil thus ?case by (fastforce)
81     next
82       case (Cons s S)
83       show ?case
84       proof(cases "Some s = safe_hd (restr_stack (- set r) (s#S))")
85         case True
86         thus ?thesis
87           using `isVal e` `heap_upds_ok (\<Gamma>, s # S)` `set r \<subseteq> domA \<Gamma> \<union> upds (s # S)`
88           apply auto
89           apply (intro exI conjI)
90           apply (rule rtranclp.intros(1))
91           apply auto
92           done
93       next
94         case False
95         then obtain x where [simp]: "s = Upd x" and [simp]: "x \<in> set r"
96           by(cases s) (auto split: if_splits)
97       
98         from `heap_upds_ok (\<Gamma>, s # S)` `s = Upd x`
99         have [simp]: "x \<notin> domA \<Gamma>" and "heap_upds_ok ((x,e) # \<Gamma>, S)"
100           by (auto dest: heap_upds_okE) 
101
102         from `set r \<subseteq> domA \<Gamma> \<union> upds (s # S)`
103         have "set r \<subseteq> domA ((x,e) # \<Gamma>) \<union> upds S" by auto
104         
105         have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)" unfolding `s = _` ..
106         also have "\<dots> \<Rightarrow> ((x,e) # \<Gamma>, e, S)" by (rule var\<^sub>2[OF `x \<notin> domA \<Gamma>` `isVal e`])
107         also
108         from Cons.IH[OF `heap_upds_ok ((x,e) # \<Gamma>, S)`  `set r \<subseteq> domA ((x,e) # \<Gamma>) \<union> upds S`]
109         obtain \<Gamma>' S' where  "((x,e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
110             and res: "heap_upds_ok (\<Gamma>', S')"
111                      "to_gc_conf r ((x,e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
112                      "(\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))"
113                      "set r \<subseteq> domA \<Gamma>' \<union> upds S'"
114           by blast
115         note this(1)
116         finally
117         have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')".
118         thus ?thesis  using res by auto
119       qed
120     qed
121   qed
122 qed
123   
124
125 lemma sestoftUnGCstep:
126   assumes "to_gc_conf r c \<Rightarrow> d"
127   assumes "heap_upds_ok_conf c"
128   assumes "r_ok (r, c)"
129   shows   "\<exists> c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r c' \<and> heap_upds_ok_conf c' \<and> r_ok (r, c')"
130 proof-
131   obtain \<Gamma> e S where "c = (\<Gamma>, e, S)" by (cases c) auto
132   with assms
133   have "heap_upds_ok (\<Gamma>,S)" and "set r \<subseteq> domA \<Gamma> \<union> upds S" by auto
134   from sestoftUnGCStack[OF this]
135   obtain \<Gamma>' S' where
136     "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
137     and *: "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
138     and disj: "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
139     and "heap_upds_ok (\<Gamma>', S')"
140     and "set r \<subseteq> domA \<Gamma>' \<union> upds S'" by metis
141   note this(1)
142   also
143
144   from assms(1)[unfolded `c =_ ` *]
145   have "\<exists> \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'')  \<and> d = to_gc_conf r (\<Gamma>'', e'', S'') \<and> heap_upds_ok (\<Gamma>'', S'') \<and> set r \<subseteq> domA \<Gamma>'' \<union> upds S''"
146   proof(cases rule: step.cases)
147     case app\<^sub>1
148     thus ?thesis
149       using `heap_upds_ok (\<Gamma>', S')` and `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
150       apply auto
151       apply (intro exI conjI)
152       apply (rule step.intros)
153       apply auto
154       done
155   next
156     case app\<^sub>2
157     thus ?thesis
158       using disj  `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
159       apply (cases S')
160       apply auto
161       apply (intro exI conjI)
162       apply (rule step.intros)
163       apply auto
164       done
165   next
166     case var\<^sub>1
167     thus ?thesis
168       using `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
169       apply auto
170       apply (intro exI conjI)
171       apply (rule step.intros)
172       apply (auto simp add: restr_delete_twist)
173       done
174   next
175     case var\<^sub>2
176     thus ?thesis
177       using disj `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
178       apply (cases S')
179       apply auto
180       apply (intro exI conjI)
181       apply (rule step.intros)
182       apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
183       done
184   next
185     case (let\<^sub>1 \<Delta>'' \<Gamma>'' S'' e')
186     thus ?thesis
187       using `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
188       apply auto
189       apply (intro exI conjI)
190       apply (rule step.intros)
191       apply (auto simp add: restrictA_append)
192       sorry
193   next
194     case if\<^sub>1
195     thus ?thesis
196       using `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
197       apply auto
198       apply (intro exI conjI)
199       apply (rule step.intros)
200       apply (auto)
201       done
202   next
203     case if\<^sub>2
204     thus ?thesis
205       using disj `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`
206       apply (cases S')
207       apply auto
208       apply (intro exI conjI)
209       apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
210       apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
211       apply (intro exI conjI)
212       apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
213       apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
214       done
215   qed
216   then obtain \<Gamma>'' e'' S''
217     where "(\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'')"
218     and "d = to_gc_conf r (\<Gamma>'', e'', S'')"
219     and "heap_upds_ok (\<Gamma>'', S'')"
220     and "set r \<subseteq> domA \<Gamma>'' \<union> upds S''"
221     by blast
222   note this(1)
223   finally
224   have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')".
225   with `d = _` `heap_upds_ok (\<Gamma>'', S'')` `set r \<subseteq> domA \<Gamma>'' \<union> upds S''`
226   show ?thesis unfolding `c = _` by auto
227 qed
228
229
230 lemma sestoftUnGC:
231   assumes "(r, to_gc_conf r c) \<Rightarrow>\<^sub>G\<^sup>* (r', d)" and "heap_upds_ok_conf c" and "r_ok (r, c)"
232   shows   "\<exists> c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> heap_upds_ok_conf c' \<and> r_ok (r', c')"
233 using assms
234 proof(induction r' "d"  rule: rtranclp_induct2)
235   case refl
236   thus ?case by blast
237 next
238   case (step r' d' r'' d'')
239   then obtain c' where "c \<Rightarrow>\<^sup>* c'" and "d' = to_gc_conf r' c'" and "heap_upds_ok_conf c'" and "r_ok (r', c')" by auto
240   with step
241   have "(r', to_gc_conf r' c') \<Rightarrow>\<^sub>G (r'', d'')" by simp
242   hence "\<exists> c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> heap_upds_ok_conf c'' \<and> r_ok (r'', c'')"
243   proof(cases rule: gc_step.cases)
244     case normal
245     from sestoftUnGCstep[OF normal(2) `heap_upds_ok_conf c'` `r_ok (r',c')`] `r'' = r'`
246     show ?thesis by auto
247   next
248     case (dropUpd \<Gamma> e x S)
249     from `to_gc_conf r' c' = (\<Gamma>, e, Upd x # S)`
250     have "x \<notin> set r'" by (auto dest: Upd_eq_restr_stackD)
251     
252     from `heap_upds_ok_conf c'` and `to_gc_conf r' c' = (\<Gamma>, e, Upd x # S)`
253     have "heap_upds_ok (\<Gamma>, Upd x # S)" by fastforce
254     hence [simp]: "x \<notin> domA \<Gamma>" "x \<notin> upds S" by (auto dest: heap_upds_ok_upd)
255
256     from `to_gc_conf r' c' = (\<Gamma>, e, Upd x # S)`
257     have "Upd x # S = restr_stack (- set r') (snd (snd c'))"  by auto
258     from arg_cong[where f = upds, OF this]
259     have "x \<in> upds (snd (snd c'))" by auto
260     with `r_ok (r', c')` have "r_ok (x # r', c')" by auto
261
262     have "to_gc_conf (x # r') c' = to_gc_conf ([x]@ r') c'" by simp
263     also have "\<dots> = to_gc_conf [x] (to_gc_conf r' c')" by (rule to_gc_conf_append)
264     also have "\<dots> = to_gc_conf [x] (\<Gamma>, e, Upd x # S)" unfolding `to_gc_conf r' c' = _`..
265     also have "\<dots> = (\<Gamma>, e, S)" by (auto intro: restrictA_noop)
266     finally have "to_gc_conf (x # r') c' = (\<Gamma>, e, S)".
267     with dropUpd  `heap_upds_ok_conf c'` `r_ok (x # r', c')`
268     show ?thesis by fastforce
269   qed
270   then obtain c'' where "c' \<Rightarrow>\<^sup>* c''" and "d'' = to_gc_conf r'' c''" and "heap_upds_ok_conf c''" and "r_ok (r'', c'')" by auto
271   with `c \<Rightarrow>\<^sup>* c'` `c' \<Rightarrow>\<^sup>* c''`
272   have "c \<Rightarrow>\<^sup>* c''" by auto
273   with `d'' = _` `heap_upds_ok_conf c''` `r_ok (r'', c'')`
274   show ?case by blast
275 qed
276   
277 lemma sestoftUnGC':
278   assumes "([], [], e, []) \<Rightarrow>\<^sub>G\<^sup>* (r, \<Gamma>, e', [])"
279   assumes "isVal e'"
280   shows   "\<exists> \<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''"
281 proof-
282  from sestoftUnGC[where r = "[]" and c = "([], e, [])", simplified, OF assms(1)]
283  obtain \<Gamma>' S'
284   where "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')"
285     and "\<Gamma> = restrictA (- set r) \<Gamma>'"
286     and "restr_stack (- set r) S' = []"
287     and "heap_upds_ok (\<Gamma>', S')"
288     and "set r \<subseteq> domA \<Gamma>' \<union> upds S'"
289     by auto
290  
291   from `isVal e'` sestoftUnGCStack[where e = e', OF `heap_upds_ok (\<Gamma>', S')` `set r \<subseteq> domA \<Gamma>' \<union> upds S'`]
292   obtain \<Gamma>'' S''
293     where "(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')"
294     and   "heap_upds_ok (\<Gamma>'', S'')"
295     and "to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')"
296     and "safe_hd S'' = safe_hd (restr_stack (- set r) S'')"
297     and "set r \<subseteq> domA \<Gamma>'' \<union> upds S''"
298     by metis
299   from this (3,4) `restr_stack (- set r) S' = []`
300   have "S'' = []" by auto
301  
302   from `([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')` and `(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')` and `S'' = []`
303   have "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', [])" by auto
304   moreover
305   have "\<Gamma> = restrictA (- set r) \<Gamma>''" using `to_gc_conf r _ = _` `\<Gamma> = _` by auto
306   moreover
307   from `set r \<subseteq> domA \<Gamma>'' \<union> upds S''` `S'' = []`
308   have "set r \<subseteq> domA \<Gamma>''" by simp
309   ultimately
310   show ?thesis by blast
311 qed
312
313
314 end
315