equal
deleted
inserted
replaced
1 (* Title: thys/Turing_Hoare.thy |
1 (* Title: thys/Turing_Hoare.thy |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 header {* Hoare Rules for TMs *} |
5 chapter {* Hoare Rules for TMs *} |
6 |
6 |
7 theory Turing_Hoare |
7 theory Turing_Hoare |
8 imports Turing |
8 imports Turing |
9 begin |
9 begin |
10 |
10 |
143 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)" |
144 using `n2 \<le> n` by simp |
144 using `n2 \<le> n` by simp |
145 next |
145 next |
146 case False |
146 case False |
147 then obtain n3 where "n = n2 - n3" |
147 then obtain n3 where "n = n2 - n3" |
148 by (metis diff_le_self le_imp_diff_is_add nat_add_commute nat_le_linear) |
148 using diff_le_self le_imp_diff_is_add nat_le_linear |
|
149 add.commute by metis |
149 moreover |
150 moreover |
150 with eq show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
151 with eq show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
151 by (simp add: not_is_final[where ?n1.0="n2"]) |
152 by (simp add: not_is_final[where ?n1.0="n2"]) |
152 qed |
153 qed |
153 qed |
154 qed |