336 by blast |
336 by blast |
337 have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" |
337 have poI4: "\<forall>x. x \<in> R \<and> \<not> m x \<longrightarrow> x \<in> reachable ?Rb ?B" |
338 proof (rule allI, rule impI) |
338 proof (rule allI, rule impI) |
339 fix x |
339 fix x |
340 assume a: "x \<in> R \<and> \<not> m x" |
340 assume a: "x \<in> R \<and> \<not> m x" |
341 \<comment> \<open>First, a disjunction on @{term"p^.r"} used later in the proof\<close> |
341 \<comment> \<open>First, a disjunction on \<^term>\<open>p^.r\<close> used later in the proof\<close> |
342 have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 |
342 have pDisj:"p^.r = Null \<or> (p^.r \<noteq> Null \<and> p^.r^.m)" using poI1 poI2 |
343 by auto |
343 by auto |
344 \<comment> \<open>@{term x} belongs to the left hand side of @{thm[source] subset}:\<close> |
344 \<comment> \<open>\<^term>\<open>x\<close> belongs to the left hand side of @{thm[source] subset}:\<close> |
345 have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using a i4 by (simp only:reachable_def, clarsimp) |
345 have incl: "x \<in> ?Ra\<^sup>*``addrs ?A" using a i4 by (simp only:reachable_def, clarsimp) |
346 have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def) |
346 have excl: "x \<notin> ?Rb\<^sup>*`` addrs ?T" using pDisj ifB1 a by (auto simp add:addrs_def) |
347 \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close> |
347 \<comment> \<open>And therefore also belongs to the right hand side of @{thm[source]subset},\<close> |
348 \<comment> \<open>which corresponds to our goal.\<close> |
348 \<comment> \<open>which corresponds to our goal.\<close> |
349 from incl excl subset show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def) |
349 from incl excl subset show "x \<in> reachable ?Rb ?B" by (auto simp add:reachable_def) |
352 |
352 |
353 \<comment> \<open>If it is marked, then it is reachable\<close> |
353 \<comment> \<open>If it is marked, then it is reachable\<close> |
354 from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" . |
354 from i5 have poI5: "\<forall>x. m x \<longrightarrow> x \<in> R" . |
355 moreover |
355 moreover |
356 |
356 |
357 \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close> |
357 \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close> |
358 from i7 i6 ifB2 |
358 from i7 i6 ifB2 |
359 have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" |
359 have poI6: "\<forall>x. x \<notin> set stack_tl \<longrightarrow> (r(p \<rightarrow> t)) x = iR x \<and> l x = iL x" |
360 by(auto simp: addr_p_eq stack_eq fun_upd_apply) |
360 by(auto simp: addr_p_eq stack_eq fun_upd_apply) |
361 |
361 |
362 moreover |
362 moreover |
363 |
363 |
364 \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close> |
364 \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close> |
365 from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl" |
365 from p_notin_stack_tl i7 have poI7: "stkOk c l (r(p \<rightarrow> t)) iL iR p stack_tl" |
366 by (clarsimp simp:stack_eq addr_p_eq) |
366 by (clarsimp simp:stack_eq addr_p_eq) |
367 |
367 |
368 ultimately show "?popInv stack_tl" by simp |
368 ultimately show "?popInv stack_tl" by simp |
369 qed |
369 qed |
452 \<comment> \<open>If it is marked, then it is reachable\<close> |
452 \<comment> \<open>If it is marked, then it is reachable\<close> |
453 from i5 |
453 from i5 |
454 have "?swI5" . |
454 have "?swI5" . |
455 moreover |
455 moreover |
456 |
456 |
457 \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close> |
457 \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close> |
458 from i6 stack_eq |
458 from i6 stack_eq |
459 have "?swI6" |
459 have "?swI6" |
460 by clarsimp |
460 by clarsimp |
461 moreover |
461 moreover |
462 |
462 |
463 \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close> |
463 \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close> |
464 from stackDist i7 nifB2 |
464 from stackDist i7 nifB2 |
465 have "?swI7" |
465 have "?swI7" |
466 by (clarsimp simp:addr_p_eq stack_eq) |
466 by (clarsimp simp:addr_p_eq stack_eq) |
467 |
467 |
468 ultimately show ?thesis by auto |
468 ultimately show ?thesis by auto |
550 from i5 |
550 from i5 |
551 have "?puI5" |
551 have "?puI5" |
552 by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable) |
552 by (auto simp:addrs_def i3 reachable_def addr_t_eq fun_upd_apply intro:self_reachable) |
553 moreover |
553 moreover |
554 |
554 |
555 \<comment> \<open>If it is not on the stack, then its @{term l} and @{term r} fields are unchanged\<close> |
555 \<comment> \<open>If it is not on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields are unchanged\<close> |
556 from i6 |
556 from i6 |
557 have "?puI6" |
557 have "?puI6" |
558 by (simp add:new_stack_eq) |
558 by (simp add:new_stack_eq) |
559 moreover |
559 moreover |
560 |
560 |
561 \<comment> \<open>If it is on the stack, then its @{term l} and @{term r} fields can be reconstructed\<close> |
561 \<comment> \<open>If it is on the stack, then its \<^term>\<open>l\<close> and \<^term>\<open>r\<close> fields can be reconstructed\<close> |
562 from stackDist i6 t_notin_stack i7 |
562 from stackDist i6 t_notin_stack i7 |
563 have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq) |
563 have "?puI7" by (clarsimp simp:addr_t_eq new_stack_eq) |
564 |
564 |
565 ultimately show ?thesis by auto |
565 ultimately show ?thesis by auto |
566 qed |
566 qed |