253 and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+ |
253 and i5: "?I5" and i6: "?I6" and i7: "?I7" by simp+ |
254 have stackDist: "distinct (stack)" using i1 by (rule List_distinct) |
254 have stackDist: "distinct (stack)" using i1 by (rule List_distinct) |
255 |
255 |
256 show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and> |
256 show "(?ifB1 \<longrightarrow> (?ifB2 \<longrightarrow> (\<exists>stack.?popInv stack)) \<and> |
257 (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and> |
257 (\<not>?ifB2 \<longrightarrow> (\<exists>stack.?swInv stack)) ) \<and> |
258 (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))" |
258 (\<not>?ifB1 \<longrightarrow> (\<exists>stack.?puInv stack))" |
259 proof - |
259 proof - |
260 { |
260 { |
261 assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c" |
261 assume ifB1: "t = Null \<or> t^.m" and ifB2: "p^.c" |
262 from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto |
262 from ifB1 whileB have pNotNull: "p \<noteq> Null" by auto |
263 then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto |
263 then obtain addr_p where addr_p_eq: "p = Ref addr_p" by auto |
264 with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" |
264 with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" |
265 by auto |
265 by auto |
266 with i2 have m_addr_p: "p^.m" by auto |
266 with i2 have m_addr_p: "p^.m" by auto |
267 have stackDist: "distinct (stack)" using i1 by (rule List_distinct) |
267 have stackDist: "distinct (stack)" using i1 by (rule List_distinct) |
268 from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp |
268 from stack_eq stackDist have p_notin_stack_tl: "addr p \<notin> set stack_tl" by simp |
269 let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl" |
269 let "?poI1\<and> ?poI2\<and> ?poI3\<and> ?poI4\<and> ?poI5\<and> ?poI6\<and> ?poI7" = "?popInv stack_tl" |
270 have "?popInv stack_tl" |
270 have "?popInv stack_tl" |
271 proof - |
271 proof - |
272 |
272 |
273 -- {*List property is maintained:*} |
273 -- {*List property is maintained:*} |
274 from i1 p_notin_stack_tl ifB2 |
274 from i1 p_notin_stack_tl ifB2 |
275 have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl" |
275 have poI1: "List (S c l (r(p \<rightarrow> t))) (p^.r) stack_tl" |
276 by(simp add: addr_p_eq stack_eq, simp add: S_def) |
276 by(simp add: addr_p_eq stack_eq, simp add: S_def) |
277 |
277 |
278 moreover |
278 moreover |
279 -- {*Everything on the stack is marked:*} |
279 -- {*Everything on the stack is marked:*} |
280 from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq) |
280 from i2 have poI2: "\<forall> x \<in> set stack_tl. m x" by (simp add:stack_eq) |
281 moreover |
281 moreover |
282 |
282 |
283 -- {*Everything is still reachable:*} |
283 -- {*Everything is still reachable:*} |
284 let "(R = reachable ?Ra ?A)" = "?I3" |
284 let "(R = reachable ?Ra ?A)" = "?I3" |
285 let "?Rb" = "(relS {l, r(p \<rightarrow> t)})" |
285 let "?Rb" = "(relS {l, r(p \<rightarrow> t)})" |
286 let "?B" = "{p, p^.r}" |
286 let "?B" = "{p, p^.r}" |
287 -- {*Our goal is @{text"R = reachable ?Rb ?B"}.*} |
287 -- {*Our goal is @{text"R = reachable ?Rb ?B"}.*} |
288 have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R") |
288 have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" (is "?L = ?R") |
289 proof |
289 proof |
290 show "?L \<subseteq> ?R" |
290 show "?L \<subseteq> ?R" |
291 proof (rule still_reachable) |
291 proof (rule still_reachable) |
292 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastsimp simp:addrs_def relS_def rel_def addr_p_eq |
292 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastsimp simp:addrs_def relS_def rel_def addr_p_eq |
293 intro:oneStep_reachable Image_iff[THEN iffD2]) |
293 intro:oneStep_reachable Image_iff[THEN iffD2]) |
294 show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) |
294 show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def) |
295 (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1) |
295 (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1) |
296 qed |
296 qed |
297 show "?R \<subseteq> ?L" |
297 show "?R \<subseteq> ?L" |
298 proof (rule still_reachable) |
298 proof (rule still_reachable) |
299 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A" |
299 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A" |
300 by(fastsimp simp:addrs_def rel_defs addr_p_eq |
300 by(fastsimp simp:addrs_def rel_defs addr_p_eq |
301 intro:oneStep_reachable Image_iff[THEN iffD2]) |
301 intro:oneStep_reachable Image_iff[THEN iffD2]) |
302 next |
302 next |
303 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)" |
303 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)" |
304 by (clarsimp simp:relS_def) |
304 by (clarsimp simp:relS_def) |
305 (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd2) |
305 (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd2) |
306 qed |
306 qed |
307 qed |
307 qed |
308 with i3 have poI3: "R = reachable ?Rb ?B" by (simp add:reachable_def) |
308 with i3 have poI3: "R = reachable ?Rb ?B" by (simp add:reachable_def) |
309 moreover |
309 moreover |
310 |
310 |
311 -- "If it is reachable and not marked, it is still reachable using..." |
311 -- "If it is reachable and not marked, it is still reachable using..." |
312 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4 |
312 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4 |
313 let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m" |
313 let "?Rb" = "relS {l, r(p \<rightarrow> t)} | m" |
314 let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)" |
314 let "?B" = "{p} \<union> set (map (r(p \<rightarrow> t)) stack_tl)" |
315 -- {*Our goal is @{text"\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"}.*} |
315 -- {*Our goal is @{text"\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B"}.*} |
316 let ?T = "{t, p^.r}" |
316 let ?T = "{t, p^.r}" |
317 |
317 |
318 have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
318 have "?Ra\<^sup>* `` addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
319 proof (rule still_reachable) |
319 proof (rule still_reachable) |
320 have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s" |
320 have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s" |
321 by (auto simp add:p_notin_stack_tl intro:fun_upd_other) |
321 by (auto simp add:p_notin_stack_tl intro:fun_upd_other) |
322 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
322 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
323 by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable) |
323 by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable) |
324 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))" |
324 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))" |
325 by (clarsimp simp:restr_def relS_def) |
325 by (clarsimp simp:restr_def relS_def) |
326 (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1) |
326 (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1) |
327 qed |
327 qed |
328 -- "We now bring a term from the right to the left of the subset relation." |
328 -- "We now bring a term from the right to the left of the subset relation." |
329 hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B" |
329 hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B" |
330 by blast |
330 by blast |
331 have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" |
331 have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" |
332 proof (rule allI, rule impI) |
332 proof (rule allI, rule impI) |
333 fix x |
333 fix x |
334 assume a: "x \<in> R \<and> \<not> m x" |
334 assume a: "x \<in> R \<and> \<not> m x" |
335 -- {*First, a disjunction on @{term"p^.r"} used later in the proof*} |
335 -- {*First, a disjunction on @{term"p^.r"} used later in the proof*} |
336 have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 |
336 have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 |
337 by auto |
337 by auto |
338 -- {*@{term x} belongs to the left hand side of @{thm[source] subset}:*} |
338 -- {*@{term x} belongs to the left hand side of @{thm[source] subset}:*} |
339 have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using a i4 by (simp only:reachable_def, clarsimp) |
339 have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using a i4 by (simp only:reachable_def, clarsimp) |
340 have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def) |
340 have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def) |
341 -- {*And therefore also belongs to the right hand side of @{thm[source]subset},*} |
341 -- {*And therefore also belongs to the right hand side of @{thm[source]subset},*} |
342 -- {*which corresponds to our goal.*} |
342 -- {*which corresponds to our goal.*} |
343 from incl excl subset show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def) |
343 from incl excl subset show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def) |
344 qed |
344 qed |
345 moreover |
345 moreover |
346 |
346 |
347 -- "If it is marked, then it is reachable" |
347 -- "If it is marked, then it is reachable" |
348 from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" . |
348 from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" . |
349 moreover |
349 moreover |
350 |
350 |
351 -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*} |
351 -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*} |
352 from i7 i6 ifB2 |
352 from i7 i6 ifB2 |
353 have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" |
353 have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" |
354 by(auto simp: addr_p_eq stack_eq fun_upd_apply) |
354 by(auto simp: addr_p_eq stack_eq fun_upd_apply) |
355 |
355 |
356 moreover |
356 moreover |
357 |
357 |
358 -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*} |
358 -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*} |
359 from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl" |
359 from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl" |
360 by (clarsimp simp:stack_eq addr_p_eq) |
360 by (clarsimp simp:stack_eq addr_p_eq) |
361 |
361 |
362 ultimately show "?popInv stack_tl" by simp |
362 ultimately show "?popInv stack_tl" by simp |
363 qed |
363 qed |
364 hence "\<exists>stack. ?popInv stack" .. |
364 hence "\<exists>stack. ?popInv stack" .. |
365 } |
365 } |
366 moreover |
366 moreover |
367 |
367 |
368 -- "Proofs of the Swing and Push arm follow." |
368 -- "Proofs of the Swing and Push arm follow." |
369 -- "Since they are in principle simmilar to the Pop arm proof," |
369 -- "Since they are in principle simmilar to the Pop arm proof," |
370 -- "we show fewer comments and use frequent pattern matching." |
370 -- "we show fewer comments and use frequent pattern matching." |
371 { |
371 { |
372 -- "Swing arm" |
372 -- "Swing arm" |
373 assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2" |
373 assume ifB1: "?ifB1" and nifB2: "\<not>?ifB2" |
374 from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp |
374 from ifB1 whileB have pNotNull: "p \<noteq> Null" by clarsimp |
375 then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp |
375 then obtain addr_p where addr_p_eq: "p = Ref addr_p" by clarsimp |
376 with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp |
376 with i1 obtain stack_tl where stack_eq: "stack = (addr p) # stack_tl" by clarsimp |
377 with i2 have m_addr_p: "p^.m" by clarsimp |
377 with i2 have m_addr_p: "p^.m" by clarsimp |
378 from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl" |
378 from stack_eq stackDist have p_notin_stack_tl: "(addr p) \<notin> set stack_tl" |
379 by simp |
379 by simp |
380 let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack" |
380 let "?swI1\<and>?swI2\<and>?swI3\<and>?swI4\<and>?swI5\<and>?swI6\<and>?swI7" = "?swInv stack" |
381 have "?swInv stack" |
381 have "?swInv stack" |
382 proof - |
382 proof - |
383 |
383 |
384 -- {*List property is maintained:*} |
384 -- {*List property is maintained:*} |
385 from i1 p_notin_stack_tl nifB2 |
385 from i1 p_notin_stack_tl nifB2 |
386 have swI1: "?swI1" |
386 have swI1: "?swI1" |
387 by (simp add:addr_p_eq stack_eq, simp add:S_def) |
387 by (simp add:addr_p_eq stack_eq, simp add:S_def) |
388 moreover |
388 moreover |
389 |
389 |
390 -- {*Everything on the stack is marked:*} |
390 -- {*Everything on the stack is marked:*} |
391 from i2 |
391 from i2 |
392 have swI2: "?swI2" . |
392 have swI2: "?swI2" . |
393 moreover |
393 moreover |
394 |
394 |
395 -- {*Everything is still reachable:*} |
395 -- {*Everything is still reachable:*} |
396 let "R = reachable ?Ra ?A" = "?I3" |
396 let "R = reachable ?Ra ?A" = "?I3" |
397 let "R = reachable ?Rb ?B" = "?swI3" |
397 let "R = reachable ?Rb ?B" = "?swI3" |
398 have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" |
398 have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" |
399 proof (rule still_reachable_eq) |
399 proof (rule still_reachable_eq) |
400 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" |
400 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" |
401 by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
401 by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
402 next |
402 next |
403 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A" |
403 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A" |
404 by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
404 by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
405 next |
405 next |
406 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)" |
406 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)" |
407 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1) |
407 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1) |
408 next |
408 next |
409 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)" |
409 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)" |
410 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2) |
410 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2) |
411 qed |
411 qed |
412 with i3 |
412 with i3 |
413 have swI3: "?swI3" by (simp add:reachable_def) |
413 have swI3: "?swI3" by (simp add:reachable_def) |
414 moreover |
414 moreover |
415 |
415 |
416 -- "If it is reachable and not marked, it is still reachable using..." |
416 -- "If it is reachable and not marked, it is still reachable using..." |
417 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4 |
417 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4 |
418 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4 |
418 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?swI4 |
419 let ?T = "{t}" |
419 let ?T = "{t}" |
420 have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)" |
420 have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)" |
421 proof (rule still_reachable) |
421 proof (rule still_reachable) |
422 have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)" |
422 have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)" |
423 by (auto simp add:p_notin_stack_tl intro:fun_upd_other) |
423 by (auto simp add:p_notin_stack_tl intro:fun_upd_other) |
424 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
424 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
425 by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable) |
425 by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable) |
426 next |
426 next |
427 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))" |
427 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))" |
428 by (clarsimp simp:relS_def restr_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1) |
428 by (clarsimp simp:relS_def restr_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1) |
429 qed |
429 qed |
430 then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B" |
430 then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B" |
431 by blast |
431 by blast |
432 have ?swI4 |
432 have ?swI4 |
433 proof (rule allI, rule impI) |
433 proof (rule allI, rule impI) |
434 fix x |
434 fix x |
435 assume a: "x \<in> R \<and>\<not> m x" |
435 assume a: "x \<in> R \<and>\<not> m x" |
436 with i4 addr_p_eq stack_eq have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" |
436 with i4 addr_p_eq stack_eq have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" |
437 by (simp only:reachable_def, clarsimp) |
437 by (simp only:reachable_def, clarsimp) |
438 with ifB1 a |
438 with ifB1 a |
439 have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" |
439 have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" |
440 by (auto simp add:addrs_def) |
440 by (auto simp add:addrs_def) |
441 from inc exc subset show "x \<in> reachable ?Rb ?B" |
441 from inc exc subset show "x \<in> reachable ?Rb ?B" |
442 by (auto simp add:reachable_def) |
442 by (auto simp add:reachable_def) |
443 qed |
443 qed |
444 moreover |
444 moreover |
445 |
445 |
446 -- "If it is marked, then it is reachable" |
446 -- "If it is marked, then it is reachable" |
447 from i5 |
447 from i5 |
448 have "?swI5" . |
448 have "?swI5" . |
449 moreover |
449 moreover |
450 |
450 |
451 -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*} |
451 -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*} |
452 from i6 stack_eq |
452 from i6 stack_eq |
453 have "?swI6" |
453 have "?swI6" |
454 by clarsimp |
454 by clarsimp |
455 moreover |
455 moreover |
456 |
456 |
457 -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*} |
457 -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*} |
458 from stackDist i7 nifB2 |
458 from stackDist i7 nifB2 |
459 have "?swI7" |
459 have "?swI7" |
460 by (clarsimp simp:addr_p_eq stack_eq) |
460 by (clarsimp simp:addr_p_eq stack_eq) |
461 |
461 |
462 ultimately show ?thesis by auto |
462 ultimately show ?thesis by auto |
463 qed |
463 qed |
464 then have "\<exists>stack. ?swInv stack" by blast |
464 then have "\<exists>stack. ?swInv stack" by blast |
465 } |
465 } |
466 moreover |
466 moreover |
467 |
467 |
468 { |
468 { |
469 -- "Push arm" |
469 -- "Push arm" |
470 assume nifB1: "\<not>?ifB1" |
470 assume nifB1: "\<not>?ifB1" |
471 from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp |
471 from nifB1 whileB have tNotNull: "t \<noteq> Null" by clarsimp |
472 then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp |
472 then obtain addr_t where addr_t_eq: "t = Ref addr_t" by clarsimp |
473 with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp |
473 with i1 obtain new_stack where new_stack_eq: "new_stack = (addr t) # stack" by clarsimp |
474 from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp |
474 from tNotNull nifB1 have n_m_addr_t: "\<not> (t^.m)" by clarsimp |
475 with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast |
475 with i2 have t_notin_stack: "(addr t) \<notin> set stack" by blast |
476 let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack" |
476 let "?puI1\<and>?puI2\<and>?puI3\<and>?puI4\<and>?puI5\<and>?puI6\<and>?puI7" = "?puInv new_stack" |
477 have "?puInv new_stack" |
477 have "?puInv new_stack" |
478 proof - |
478 proof - |
479 |
479 |
480 -- {*List property is maintained:*} |
480 -- {*List property is maintained:*} |
481 from i1 t_notin_stack |
481 from i1 t_notin_stack |
482 have puI1: "?puI1" |
482 have puI1: "?puI1" |
483 by (simp add:addr_t_eq new_stack_eq, simp add:S_def) |
483 by (simp add:addr_t_eq new_stack_eq, simp add:S_def) |
484 moreover |
484 moreover |
485 |
485 |
486 -- {*Everything on the stack is marked:*} |
486 -- {*Everything on the stack is marked:*} |
487 from i2 |
487 from i2 |
488 have puI2: "?puI2" |
488 have puI2: "?puI2" |
489 by (simp add:new_stack_eq fun_upd_apply) |
489 by (simp add:new_stack_eq fun_upd_apply) |
490 moreover |
490 moreover |
491 |
491 |
492 -- {*Everything is still reachable:*} |
492 -- {*Everything is still reachable:*} |
493 let "R = reachable ?Ra ?A" = "?I3" |
493 let "R = reachable ?Ra ?A" = "?I3" |
494 let "R = reachable ?Rb ?B" = "?puI3" |
494 let "R = reachable ?Rb ?B" = "?puI3" |
495 have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" |
495 have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B" |
496 proof (rule still_reachable_eq) |
496 proof (rule still_reachable_eq) |
497 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" |
497 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" |
498 by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
498 by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
499 next |
499 next |
500 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A" |
500 show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A" |
501 by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
501 by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2]) |
502 next |
502 next |
503 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)" |
503 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)" |
504 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1) |
504 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1) |
505 next |
505 next |
506 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)" |
506 show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)" |
507 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2) |
507 by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2) |
508 qed |
508 qed |
509 with i3 |
509 with i3 |
510 have puI3: "?puI3" by (simp add:reachable_def) |
510 have puI3: "?puI3" by (simp add:reachable_def) |
511 moreover |
511 moreover |
512 |
512 |
513 -- "If it is reachable and not marked, it is still reachable using..." |
513 -- "If it is reachable and not marked, it is still reachable using..." |
514 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4 |
514 let "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Ra ?A" = ?I4 |
515 let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4 |
515 let "\<forall>x. x \<in> R \<and> \<not> ?new_m x \<longrightarrow> x \<in> reachable ?Rb ?B" = ?puI4 |
516 let ?T = "{t}" |
516 let ?T = "{t}" |
517 have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)" |
517 have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)" |
518 proof (rule still_reachable) |
518 proof (rule still_reachable) |
519 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
519 show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)" |
520 by (fastsimp simp:new_stack_eq addrs_def intro:self_reachable) |
520 by (fastsimp simp:new_stack_eq addrs_def intro:self_reachable) |
521 next |
521 next |
522 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))" |
522 show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))" |
523 by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) |
523 by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd) |
524 (fastsimp simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3) |
524 (fastsimp simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3) |
525 qed |
525 qed |
526 then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B" |
526 then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B" |
527 by blast |
527 by blast |
528 have ?puI4 |
528 have ?puI4 |
529 proof (rule allI, rule impI) |
529 proof (rule allI, rule impI) |
530 fix x |
530 fix x |
531 assume a: "x \<in> R \<and> \<not> ?new_m x" |
531 assume a: "x \<in> R \<and> \<not> ?new_m x" |
532 have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp |
532 have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp |
533 with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" |
533 with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A" |
534 by (fastsimp simp:addr_t_eq addrs_def reachable_def intro:self_reachable) |
534 by (fastsimp simp:addr_t_eq addrs_def reachable_def intro:self_reachable) |
535 have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" |
535 have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T" |
536 using xDisj a n_m_addr_t |
536 using xDisj a n_m_addr_t |
537 by (clarsimp simp add:addrs_def addr_t_eq) |
537 by (clarsimp simp add:addrs_def addr_t_eq) |
538 from inc exc subset show "x \<in> reachable ?Rb ?B" |
538 from inc exc subset show "x \<in> reachable ?Rb ?B" |
539 by (auto simp add:reachable_def) |
539 by (auto simp add:reachable_def) |
540 qed |
540 qed |
541 moreover |
541 moreover |
542 |
542 |
543 -- "If it is marked, then it is reachable" |
543 -- "If it is marked, then it is reachable" |
544 from i5 |
544 from i5 |
545 have "?puI5" |
545 have "?puI5" |
546 by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable) |
546 by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable) |
547 moreover |
547 moreover |
548 |
548 |
549 -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*} |
549 -- {*If it is not on the stack, then its @{term l} and @{term r} fields are unchanged*} |
550 from i6 |
550 from i6 |
551 have "?puI6" |
551 have "?puI6" |
552 by (simp add:new_stack_eq) |
552 by (simp add:new_stack_eq) |
553 moreover |
553 moreover |
554 |
554 |
555 -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*} |
555 -- {*If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed*} |
556 from stackDist i6 t_notin_stack i7 |
556 from stackDist i6 t_notin_stack i7 |
557 have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq) |
557 have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq) |
558 |
558 |
559 ultimately show ?thesis by auto |
559 ultimately show ?thesis by auto |
560 qed |
560 qed |
561 then have "\<exists>stack. ?puInv stack" by blast |
561 then have "\<exists>stack. ?puInv stack" by blast |
562 |
562 |
563 } |
563 } |
564 ultimately show ?thesis by blast |
564 ultimately show ?thesis by blast |
565 qed |
565 qed |
566 } |
566 } |
567 qed |
567 qed |
568 |
568 |
569 end |
569 end |