119 fun |
119 fun |
120 is_final :: "config \<Rightarrow> bool" |
120 is_final :: "config \<Rightarrow> bool" |
121 where |
121 where |
122 "is_final (s, l, r) = (s = 0)" |
122 "is_final (s, l, r) = (s = 0)" |
123 |
123 |
|
124 lemma is_final_steps: |
|
125 assumes "is_final (s, l, r)" |
|
126 shows "is_final (steps (s, l, r) p n)" |
|
127 using assms by (induct n) (auto) |
|
128 |
124 fun |
129 fun |
125 holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100) |
130 holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100) |
126 where |
131 where |
127 "P holds_for (s, l, r) = P (l, r)" |
132 "P holds_for (s, l, r) = P (l, r)" |
128 |
133 |
132 |
137 |
133 lemma steps_0 [simp]: |
138 lemma steps_0 [simp]: |
134 shows "steps (0, (l, r)) p n = (0, (l, r))" |
139 shows "steps (0, (l, r)) p n = (0, (l, r))" |
135 by (induct n) (simp_all) |
140 by (induct n) (simp_all) |
136 |
141 |
|
142 lemma is_final_holds[simp]: |
|
143 assumes "is_final c" |
|
144 shows "Q holds_for (steps c p n) = Q holds_for c" |
|
145 using assms |
|
146 apply(induct n) |
|
147 apply(case_tac [!] c) |
|
148 apply(auto) |
|
149 done |
|
150 |
137 type_synonym assert = "tape \<Rightarrow> bool" |
151 type_synonym assert = "tape \<Rightarrow> bool" |
138 |
152 |
139 definition assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
153 definition assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
140 where |
154 where |
141 "assert_imp P Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))" |
155 "assert_imp P Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))" |
142 |
156 |
|
157 lemma test: |
|
158 assumes "is_final (steps (1, (l, r)) p n1)" |
|
159 and "is_final (steps (1, (l, r)) p n2)" |
|
160 shows "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)" |
|
161 proof - |
|
162 obtain n3 where "n1 = n2 + n3 \<or> n2 = n1 + n3" |
|
163 by (metis le_iff_add nat_le_linear) |
|
164 with assms show "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)" |
|
165 by auto |
|
166 qed |
|
167 |
143 definition |
168 definition |
144 Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
169 Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
145 where |
170 where |
146 "{P} p {Q} \<equiv> |
171 "{P} p {Q} \<equiv> |
147 (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)))" |
172 (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)))" |
148 |
173 |
149 lemma HoareI: |
174 lemma HoareI: |
150 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)" |
175 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)" |
151 shows "{P} p {Q}" |
|
152 unfolding Hoare_def using assms by auto |
|
153 |
|
154 lemma HoareI2: |
|
155 assumes "\<And>l r n. P (l, r) \<and> is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)" |
|
156 shows "{P} p {Q}" |
176 shows "{P} p {Q}" |
157 unfolding Hoare_def using assms by auto |
177 unfolding Hoare_def using assms by auto |
158 |
178 |
159 text {* |
179 text {* |
160 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 |
180 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 |
171 and B_halt : "{P2} B {Q2}" |
191 and B_halt : "{P2} B {Q2}" |
172 shows "{P1} A |+| B {Q2}" |
192 shows "{P1} A |+| B {Q2}" |
173 proof(rule HoareI) |
193 proof(rule HoareI) |
174 fix a b |
194 fix a b |
175 assume h: "P1 (a, b)" |
195 assume h: "P1 (a, b)" |
176 hence "\<exists>n. let (s, tp') = steps (Suc 0, a, b) A n in s = 0 \<and> Q1 tp'" |
196 then have "\<exists>n. is_final (steps (1, a, b) A n) \<and> Q1 holds_for (steps (1, a, b) A n)" |
177 using A_halt unfolding hoare_def by simp |
197 using A_halt unfolding Hoare_def by simp |
178 from this obtain stp1 where "let (s, tp') = steps (Suc 0, a, b) A stp1 in s = 0 \<and> Q1 tp'" .. |
198 then obtain n1 where "is_final (steps (1, a, b) A n1) \<and> Q1 holds_for (steps (1, a, b) A stp1)" .. |
179 then show "\<exists>n. case steps (Suc 0, a, b) (A |+| B) n of (s, tp') \<Rightarrow> s = 0 \<and> Q2 tp'" |
199 then show "\<exists>n. is_final (steps (1, a, b) (A |+| B) n) \<and> Q2 holds_for (steps (1, a, b) (A |+| B) n)" |
180 proof(case_tac "steps (Suc 0, a, b) A stp1", simp, erule_tac conjE) |
200 proof(case_tac "steps (Suc 0, a, b) A stp1", simp, erule_tac conjE) |
181 fix aa ba c |
201 fix aa ba c |
182 assume g1: "Q1 (ba, c)" |
202 assume g1: "Q1 (ba, c)" |
183 and g2: "steps (Suc 0, a, b) A stp1 = (0, ba, c)" |
203 and g2: "steps (Suc 0, a, b) A stp1 = (0, ba, c)" |
184 hence "P2 (ba, c)" |
204 hence "P2 (ba, c)" |
185 using aimpb apply(simp add: assert_imp_def) |
205 using aimpb apply(simp add: assert_imp_def) |
186 done |
206 done |
187 hence "\<exists> stp. let (s, tp') = steps (Suc 0, ba, c) B stp in s = 0 \<and> Q2 tp'" |
207 hence "\<exists> stp. is_final (steps (Suc 0, ba, c) B stp) \<and> Q2 holds_for (steps (Suc 0, ba, c) B stp)" |
188 using B_halt unfolding hoare_def by simp |
208 using B_halt unfolding Hoare_def by simp |
189 from this obtain stp2 where "let (s, tp') = steps (Suc 0, ba, c) B stp2 in s = 0 \<and> Q2 tp'" .. |
209 from this obtain stp2 where |
|
210 "is_final (steps (Suc 0, ba, c) B stp2) \<and> Q2 holds_for (steps (Suc 0, ba, c) B stp2)" .. |
190 thus "?thesis" |
211 thus "?thesis" |
191 proof(case_tac "steps (Suc 0, ba, c) B stp2", simp, erule_tac conjE) |
212 proof(case_tac "steps (Suc 0, ba, c) B stp2", simp, erule_tac conjE) |
192 fix aa bb ca |
213 fix aa bb ca |
193 assume g3: " Q2 (bb, ca)" "steps (Suc 0, ba, c) B stp2 = (0, bb, ca)" |
214 assume g3: " Q2 (bb, ca)" "steps (Suc 0, ba, c) B stp2 = (0, bb, ca)" |
194 have "\<exists> stp. steps (Suc 0, a, b) (A |+| B) stp = (Suc (length A div 2), ba , c)" |
215 have "\<exists> stp. steps (Suc 0, a, b) (A |+| B) stp = (Suc (length A div 2), ba , c)" |