34 (* halting case *) |
40 (* halting case *) |
35 definition |
41 definition |
36 Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
42 Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
37 where |
43 where |
38 "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))" |
44 "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))" |
39 |
|
40 |
45 |
41 (* not halting case *) |
46 (* not halting case *) |
42 definition |
47 definition |
43 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50) |
48 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50) |
44 where |
49 where |
81 and a2: "steps0 (1, l, r) A n1 = (0, l', r')" |
86 and a2: "steps0 (1, l, r) A n1 = (0, l', r')" |
82 using A_halt unfolding Hoare_halt_def |
87 using A_halt unfolding Hoare_halt_def |
83 by (metis is_final_eq surj_pair) |
88 by (metis is_final_eq surj_pair) |
84 then obtain n2 |
89 then obtain n2 |
85 where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" |
90 where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" |
86 using A_wf by (rule_tac tm_comp_pre_halt_same) |
91 using A_wf by (rule_tac tm_comp_next) |
87 moreover |
92 moreover |
88 from a1 a2 have "Q (l', r')" by (simp) |
93 from a1 a2 have "Q (l', r')" by (simp) |
89 then obtain n3 l'' r'' |
94 then obtain n3 l'' r'' |
90 where "is_final (steps0 (1, l', r') B n3)" |
95 where "is_final (steps0 (1, l', r') B n3)" |
91 and b1: "S holds_for (steps0 (1, l', r') B n3)" |
96 and b1: "S holds_for (steps0 (1, l', r') B n3)" |
92 and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')" |
97 and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')" |
93 using B_halt unfolding Hoare_halt_def |
98 using B_halt unfolding Hoare_halt_def |
94 by (metis is_final_eq surj_pair) |
99 by (metis is_final_eq surj_pair) |
95 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n3 = (0, l'', r'')" |
100 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n3 = (0, l'', r'')" |
96 using A_wf by (rule_tac tm_comp_second_halt_same) |
101 using A_wf by (rule_tac tm_comp_final) |
97 ultimately show |
102 ultimately show |
98 "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> S holds_for (steps0 (1, l, r) (A |+| B) n)" |
103 "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> S holds_for (steps0 (1, l, r) (A |+| B) n)" |
99 using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) |
104 using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) |
100 qed |
105 qed |
101 |
106 |
118 and b: "Q holds_for (steps0 (1, l, r) A n1)" |
123 and b: "Q holds_for (steps0 (1, l, r) A n1)" |
119 and c: "steps0 (1, l, r) A n1 = (0, l', r')" |
124 and c: "steps0 (1, l, r) A n1 = (0, l', r')" |
120 using A_halt unfolding Hoare_halt_def |
125 using A_halt unfolding Hoare_halt_def |
121 by (metis is_final_eq surj_pair) |
126 by (metis is_final_eq surj_pair) |
122 then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" |
127 then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" |
123 using A_wf by (rule_tac tm_comp_pre_halt_same) |
128 using A_wf by (rule_tac tm_comp_next) |
124 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
129 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
125 proof(cases "n2 \<le> n") |
130 proof(cases "n2 \<le> n") |
126 case True |
131 case True |
127 from b c have "Q (l', r')" by simp |
132 from b c have "Q (l', r')" by simp |
128 then have "\<forall> n. \<not> is_final (steps0 (1, l', r') B n) " |
133 then have "\<forall> n. \<not> is_final (steps0 (1, l', r') B n) " |
130 then have "\<not> is_final (steps0 (1, l', r') B (n - n2))" by auto |
135 then have "\<not> is_final (steps0 (1, l', r') B (n - n2))" by auto |
131 then obtain s'' l'' r'' |
136 then obtain s'' l'' r'' |
132 where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" |
137 where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" |
133 and "\<not> is_final (s'', l'', r'')" by (metis surj_pair) |
138 and "\<not> is_final (s'', l'', r'')" by (metis surj_pair) |
134 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" |
139 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" |
135 using A_wf by (auto dest: tm_comp_second_same simp del: tm_wf.simps) |
140 using A_wf by (auto dest: tm_comp_second simp del: tm_wf.simps) |
136 then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" |
141 then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" |
137 using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) |
142 using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) |
138 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
143 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
139 using `n2 \<le> n` by simp |
144 using `n2 \<le> n` by simp |
140 next |
145 next |