Fix end-to-end proof to finally obtain the unmodified semantics
[darcs-mirror-isa-launchbury.git] / Launchbury / SestoftGC.thy
1 theory SestoftGC
2 imports Sestoft 
3 begin
4
5 inductive gc_step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightarrow>\<^sub>G" 50) where
6   normal:  "c \<Rightarrow> c' \<Longrightarrow> c \<Rightarrow>\<^sub>G c'"
7 | dropUpd: "(\<Gamma>, e, Upd x # S) \<Rightarrow>\<^sub>G (\<Gamma>, e, S @ [Dummy x])"
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 abbreviation gc_steps (infix "\<Rightarrow>\<^sub>G\<^sup>*" 50) where "gc_steps \<equiv> gc_step\<^sup>*\<^sup>*"
14 lemmas converse_rtranclp_into_rtranclp[of gc_step, OF _ r_into_rtranclp, trans]
15
16 lemma var_onceI:
17   assumes "map_of \<Gamma> x = Some e"
18   shows "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G\<^sup>* (delete x \<Gamma>, e , S@[Dummy x])"
19 proof-
20   from assms 
21   have "(\<Gamma>, Var x, S) \<Rightarrow>\<^sub>G (delete x \<Gamma>, e , Upd x # S)"..
22   moreover
23   have "\<dots> \<Rightarrow>\<^sub>G  (delete x \<Gamma>, e, S@[Dummy x])"..
24   ultimately
25   show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
26 qed
27
28 lemma normal_trans:  "c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c \<Rightarrow>\<^sub>G\<^sup>* c'"
29   by (induction rule:rtranclp_induct)
30      (simp, metis normal rtranclp.rtrancl_into_rtrancl)
31
32 fun to_gc_conf :: "var list \<Rightarrow> conf \<Rightarrow> conf"
33   where "to_gc_conf r (\<Gamma>, e, S) = (restrictA (- set r) \<Gamma>, e, restr_stack (- set r) S @ (map Dummy (rev r)))"
34
35 lemma restr_stack_map_Dummy[simp]: "restr_stack V (map Dummy l) = map Dummy l"
36   by (induction l) auto
37
38 lemma restr_stack_append[simp]: "restr_stack V (l@l') = restr_stack V l @ restr_stack V l'"
39   by (induction l rule: restr_stack.induct) auto
40
41 lemma to_gc_conf_append[simp]:
42   "to_gc_conf (r@r') c = to_gc_conf r (to_gc_conf r' c)"
43   by (cases c) auto
44
45 lemma to_gc_conf_eqE[elim!]:
46   assumes  "to_gc_conf r c = (\<Gamma>, e, S)"
47   obtains \<Gamma>' S' where "c = (\<Gamma>', e, S')" and "\<Gamma> = restrictA (- set r) \<Gamma>'" and "S = restr_stack (- set r) S' @ map Dummy (rev r)"
48   using assms by (cases c) auto
49
50 fun safe_hd :: "'a list \<Rightarrow> 'a option"
51  where  "safe_hd (x#_) = Some x"
52      |  "safe_hd [] = None"
53
54 lemma safe_hd_None[simp]: "safe_hd xs = None \<longleftrightarrow> xs = []"
55   by (cases xs) auto
56
57 abbreviation r_ok :: "var list \<Rightarrow> conf \<Rightarrow> bool"
58   where "r_ok r c \<equiv> set r \<subseteq> domA (fst c) \<union> upds (snd (snd c))"
59
60 lemma subset_bound_invariant:
61   "invariant step (r_ok r)"
62 proof
63   fix x y
64   assume "x \<Rightarrow> y" and "r_ok r x" thus "r_ok r y"
65   by (induction) auto
66 qed
67
68 lemma safe_hd_restr_stack[simp]:
69   "Some a = safe_hd (restr_stack V (a # S)) \<longleftrightarrow> restr_stack V (a # S) = a # restr_stack V S"
70   using assms
71   apply (cases a)
72   apply (auto split: if_splits)
73   apply (thin_tac "?P a")
74   apply (induction S rule: restr_stack.induct)
75   apply (auto split: if_splits)
76   done
77
78 lemma sestoftUnGCStack:
79   assumes "heap_upds_ok (\<Gamma>, S)"
80   obtains \<Gamma>' S' where
81     "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
82     "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
83     "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
84 proof-
85   show ?thesis
86   proof(cases "isVal e")
87     case False
88     thus ?thesis using assms  by -(rule that, auto)
89   next
90     case True
91     from that assms 
92     show ?thesis
93     apply (atomize_elim)
94     proof(induction S arbitrary: \<Gamma>)
95       case Nil thus ?case by (fastforce)
96     next
97       case (Cons s S)
98       show ?case
99       proof(cases "Some s = safe_hd (restr_stack (- set r) (s#S))")
100         case True
101         thus ?thesis
102           using `isVal e` `heap_upds_ok (\<Gamma>, s # S)`
103           apply auto
104           apply (intro exI conjI)
105           apply (rule rtranclp.intros(1))
106           apply auto
107           done
108       next
109         case False
110         then obtain x where [simp]: "s = Upd x" and [simp]: "x \<in> set r"
111           by(cases s) (auto split: if_splits)
112       
113         from `heap_upds_ok (\<Gamma>, s # S)` `s = Upd x`
114         have [simp]: "x \<notin> domA \<Gamma>" and "heap_upds_ok ((x,e) # \<Gamma>, S)"
115           by (auto dest: heap_upds_okE) 
116
117         have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>, e, Upd x # S)" unfolding `s = _` ..
118         also have "\<dots> \<Rightarrow> ((x,e) # \<Gamma>, e, S)" by (rule step.var\<^sub>2[OF `x \<notin> domA \<Gamma>` `isVal e`])
119         also
120         from Cons.IH[OF `heap_upds_ok ((x,e) # \<Gamma>, S)` ]
121         obtain \<Gamma>' S' where  "((x,e) # \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
122             and res: "to_gc_conf r ((x,e) # \<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
123                      "(\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'))"
124           by blast
125         note this(1)
126         finally
127         have "(\<Gamma>, e, s # S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')".
128         thus ?thesis  using res by auto
129       qed
130     qed
131   qed
132 qed
133
134 lemma perm_exI_trivial:
135   "P x x \<Longrightarrow> \<exists> \<pi>. P (\<pi> \<bullet> x) x"
136 by (rule exI[where x = "0::perm"]) auto
137
138 lemma upds_list_restr_stack[simp]:
139   "upds_list (restr_stack V S) = filter (\<lambda> x. x\<in>V) (upds_list S)"
140 by (induction S rule: restr_stack.induct) auto
141
142 lemma heap_upd_ok_to_gc_conf:
143   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> to_gc_conf r (\<Gamma>, e, S) = (\<Gamma>'', e'', S'') \<Longrightarrow> heap_upds_ok (\<Gamma>'', S'')"
144 by (auto simp add: heap_upds_ok.simps)
145
146 lemma sestoftUnGCstep:
147   assumes "to_gc_conf r c \<Rightarrow>\<^sub>G d"
148   assumes "heap_upds_ok_conf c"
149   assumes "closed c"
150   and "r_ok r c"
151   shows   "\<exists> r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'"
152 proof-
153   obtain \<Gamma> e S where "c = (\<Gamma>, e, S)" by (cases c) auto
154   with assms
155   have "heap_upds_ok (\<Gamma>,S)" and "closed (\<Gamma>, e, S)" and "r_ok r (\<Gamma>, e, S)" by auto
156   from sestoftUnGCStack[OF this(1)]
157   obtain \<Gamma>' S' where
158     "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
159     and *: "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
160     and disj: "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
161     by metis
162
163   from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` heap_upds_ok_invariant]  `heap_upds_ok (\<Gamma>,S)`
164   have "heap_upds_ok (\<Gamma>', S')" by auto
165
166   from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` closed_invariant  `closed (\<Gamma>, e, S)` ]
167   have "closed (\<Gamma>', e, S')" by auto
168
169   from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` subset_bound_invariant `r_ok r (\<Gamma>, e, S)` ]
170   have "r_ok r (\<Gamma>', e, S')" by auto
171
172   from assms(1)[unfolded `c =_ ` *]
173   have "\<exists> r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')"
174   proof(cases rule: gc_step.cases)
175     case normal
176     hence "\<exists> \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')"
177     proof(cases rule: step.cases)
178       case app\<^sub>1
179       thus ?thesis
180         apply auto
181         apply (intro exI conjI)
182         apply (rule  step.intros)
183         apply auto
184         done
185     next
186       case (app\<^sub>2 \<Gamma> y ea x S)
187       thus ?thesis
188         using disj 
189         apply (cases S')
190         apply auto
191         apply (intro exI conjI)
192         apply (rule step.intros)
193         apply auto
194         done
195     next
196       case var\<^sub>1
197       thus ?thesis
198         apply auto
199         apply (intro  exI conjI)
200         apply (rule step.intros)
201         apply (auto simp add: restr_delete_twist)
202         done
203     next
204       case var\<^sub>2
205       thus ?thesis
206         using disj 
207         apply (cases S')
208         apply auto
209         apply (intro exI conjI)
210         apply (rule step.intros)
211         apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
212         done
213     next
214       case (let\<^sub>1 \<Delta>'' \<Gamma>'' S'' e')
215
216       from `closed (\<Gamma>', e, S')` let\<^sub>1
217       have "closed (\<Gamma>', Let \<Delta>'' e', S')" by simp
218
219       from fresh_distinct[OF let\<^sub>1(3)] fresh_distinct_fv[OF let\<^sub>1(4)]
220       have "domA \<Delta>'' \<inter> domA \<Gamma>'' = {}" and "domA \<Delta>'' \<inter> upds S'' = {}"  and "domA \<Delta>'' \<inter> dummies S'' = {}" 
221         by (auto dest: set_mp[OF ups_fv_subset] set_mp[OF dummies_fv_subset])
222       moreover
223       from let\<^sub>1(1)
224       have "domA \<Gamma>' \<union> upds S' \<subseteq> domA \<Gamma>'' \<union> upds S'' \<union> dummies S''"
225         by auto
226       ultimately
227       have disj: "domA \<Delta>'' \<inter> domA \<Gamma>' = {}" "domA \<Delta>'' \<inter> upds S' = {}"
228         by auto
229       
230       from `domA \<Delta>'' \<inter> dummies S'' = {}` let\<^sub>1(1)
231       have "domA \<Delta>'' \<inter> set r = {}" by auto
232       hence [simp]: "restrictA (- set r) \<Delta>'' = \<Delta>''"
233         by (auto intro: restrictA_noop)
234
235       from let\<^sub>1(1-3)
236       show ?thesis
237         apply auto
238         apply (intro  exI[where x = "r"] exI[where x = "\<Delta>'' @ \<Gamma>'"] exI[where x = "S'"] conjI)
239         apply (rule let\<^sub>1_closed[OF `closed (\<Gamma>', Let \<Delta>'' e', S')` disj])
240         apply (auto simp add: restrictA_append)
241         done
242     next
243       case if\<^sub>1
244       thus ?thesis
245         apply auto
246         apply (intro exI[where x = "0::perm"] exI conjI)
247         unfolding permute_zero
248         apply (rule step.intros)
249         apply (auto)
250         done
251     next
252       case if\<^sub>2
253       thus ?thesis
254         using disj
255         apply (cases S')
256         apply auto
257         apply (intro exI exI conjI)
258         apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
259         apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
260         apply (intro exI conjI)
261         apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
262         apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
263         done
264     qed
265     with invariantE[OF subset_bound_invariant _ `r_ok r (\<Gamma>', e, S')`]
266     show ?thesis by blast
267   next
268   case (dropUpd \<Gamma>'' e'' x S'')
269     from `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
270     have "x \<notin> set r" by (auto dest!: arg_cong[where f = upds])
271     
272     from `heap_upds_ok (\<Gamma>', S')` and `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
273     have "heap_upds_ok (\<Gamma>'', Upd x # S'')" by (rule heap_upd_ok_to_gc_conf)
274     hence [simp]: "x \<notin> domA \<Gamma>''" "x \<notin> upds S''" by (auto dest: heap_upds_ok_upd)
275
276     have "to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x]@ r) (\<Gamma>', e, S')" by simp
277     also have "\<dots> = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))" by (rule to_gc_conf_append)
278     also have "\<dots> = to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'')" unfolding `to_gc_conf r (\<Gamma>', e, S') = _`..
279     also have "\<dots> = (\<Gamma>'', e'', S''@[Dummy x])" by (auto intro: restrictA_noop)
280     also have "\<dots> = d" using ` d= _` by simp
281     finally have "to_gc_conf (x # r) (\<Gamma>', e, S') = d".
282     moreover
283     from `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
284     have "x \<in> upds S'" by (auto dest!: arg_cong[where f = upds])
285     with `r_ok r (\<Gamma>', e, S')`
286     have "r_ok (x # r) (\<Gamma>', e, S')" by auto
287     moreover
288     note `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')`
289     ultimately
290     show ?thesis by fastforce
291   qed
292   then obtain r' \<Gamma>'' e'' S''
293     where "(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')"
294     and "d = to_gc_conf r' (\<Gamma>'', e'', S'')"
295     and "r_ok r' (\<Gamma>'', e'', S'')"
296     by metis 
297
298   from  `(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')` and `(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')`
299   have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')" by (rule rtranclp_trans)
300   with `d = _` `r_ok r' _`
301   show ?thesis unfolding `c = _` by auto
302 qed
303
304
305 lemma sestoftUnGC:
306   assumes "(to_gc_conf r c) \<Rightarrow>\<^sub>G\<^sup>* d" and "heap_upds_ok_conf c" and "closed c" and "r_ok r c"
307   shows   "\<exists> r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'"
308 using assms
309 proof(induction rule: rtranclp_induct)
310   case base
311   thus ?case by blast
312 next
313   case (step d' d'')
314   then obtain r' c' where "c \<Rightarrow>\<^sup>*  c'" and "d' = to_gc_conf r' c'" and "r_ok r' c'"  by auto
315
316   from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` heap_upds_ok_invariant]  `heap_upds_ok _`
317   have "heap_upds_ok_conf c'".
318
319   from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` closed_invariant]  `closed _` 
320   have "closed c'".
321
322   from step `d' = to_gc_conf r' c'`
323   have "to_gc_conf r' c' \<Rightarrow>\<^sub>G d''" by simp
324   from this `heap_upds_ok_conf c'` `closed c'` `r_ok r' c'`
325   have "\<exists> r'' c''. c' \<Rightarrow>\<^sup>* c'' \<and> d'' = to_gc_conf r'' c'' \<and> r_ok r'' c''"
326     by (rule sestoftUnGCstep)
327   then obtain r'' c'' where "c' \<Rightarrow>\<^sup>* c''" and "d'' = to_gc_conf r'' c''" and "r_ok r'' c''" by auto
328   
329   from `c' \<Rightarrow>\<^sup>*  c''` `c \<Rightarrow>\<^sup>*  c'`
330   have "c \<Rightarrow>\<^sup>* c''" by auto
331   with `d'' = _` `r_ok r'' c''`
332   show ?case by blast
333 qed
334
335 lemma dummies_unchanged_invariant:
336   "invariant step (\<lambda> (\<Gamma>, e, S) . dummies S = V)" (is "invariant _ ?I")
337 proof
338   fix c c'
339   assume "c \<Rightarrow> c'" and "?I c"
340   thus "?I c'" by (induction) auto
341 qed
342   
343 lemma sestoftUnGC':
344   assumes "([], e, []) \<Rightarrow>\<^sub>G\<^sup>* (\<Gamma>, e', map Dummy r)"
345   assumes "isVal e'"
346   assumes "fv e = ({}::var set)"
347   shows   "\<exists> \<Gamma>''. ([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>'', e', []) \<and> \<Gamma> = restrictA (- set r) \<Gamma>'' \<and> set r \<subseteq> domA \<Gamma>''"
348 proof-
349  from sestoftUnGC[where r = "[]" and c = "([], e, [])", simplified, OF assms(1,3)]
350  obtain r' \<Gamma>' S'
351   where "([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')"
352     and "\<Gamma> = restrictA (- set r') \<Gamma>'"
353     and "map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')"
354     and "r_ok r' (\<Gamma>', e', S')"
355     by auto
356
357   from invariant_starE[OF `([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')` dummies_unchanged_invariant]
358   have "dummies S' = {}" by auto
359   with  `map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')`
360   have "restr_stack (- set r') S' = []" and [simp]: "r = rev r'"
361   by (induction S' rule: restr_stack.induct) (auto split: if_splits)
362   
363   from invariant_starE[OF `_ \<Rightarrow>\<^sup>* _` heap_upds_ok_invariant]
364   have "heap_upds_ok (\<Gamma>', S')" by auto
365  
366   from `isVal e'` sestoftUnGCStack[where e = e', OF `heap_upds_ok (\<Gamma>', S')` ]
367   obtain \<Gamma>'' S''
368     where "(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')"
369     and "to_gc_conf r (\<Gamma>', e', S') = to_gc_conf r (\<Gamma>'', e', S'')"
370     and "safe_hd S'' = safe_hd (restr_stack (- set r) S'')"
371     by metis
372
373   from this (2,3) `restr_stack (- set r') S' = []`
374   have "S'' = []" by auto
375
376   from  `([], e, []) \<Rightarrow>\<^sup>* (\<Gamma>', e', S')`  and `(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')` and `S'' = []`
377   have "([], e, []) \<Rightarrow>\<^sup>*  (\<Gamma>'', e', [])" by auto
378   moreover
379   have "\<Gamma> = restrictA (- set r) \<Gamma>''" using `to_gc_conf r _ = _` `\<Gamma> = _` by auto
380   moreover
381   from invariant_starE[OF `(\<Gamma>', e', S') \<Rightarrow>\<^sup>* (\<Gamma>'', e', S'')` subset_bound_invariant `r_ok r' (\<Gamma>', e', S')`]
382   have "set r \<subseteq> domA \<Gamma>''" using `S'' = []` by auto
383   ultimately
384   show ?thesis by blast
385 qed
386
387 end
388