1 theory turing_hoare |
1 theory turing_hoare |
2 imports turing_basic |
2 imports turing_basic |
3 begin |
3 begin |
|
4 |
|
5 declare step.simps[simp del] |
|
6 declare steps.simps[simp del] |
|
7 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
|
8 declare tm_wf.simps[simp del] |
|
9 |
4 |
10 |
5 type_synonym assert = "tape \<Rightarrow> bool" |
11 type_synonym assert = "tape \<Rightarrow> bool" |
6 |
12 |
7 definition |
13 definition |
8 assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
14 assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
64 where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)" |
70 where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)" |
65 using A_halt unfolding Hoare_def by auto |
71 using A_halt unfolding Hoare_def by auto |
66 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
72 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
67 by(case_tac "steps0 (1, l, r) A n1") (auto) |
73 by(case_tac "steps0 (1, l, r) A n1") (auto) |
68 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
74 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
69 using A_wf by(rule_tac t_merge_pre_halt_same) (auto) |
75 using A_wf by(rule_tac tm_comp_pre_halt_same) (auto) |
70 moreover |
76 moreover |
71 from c aimpb have "P2 holds_for (0, l', r')" |
77 from c aimpb have "P2 holds_for (0, l', r')" |
72 by (rule holds_for_imp) |
78 by (rule holds_for_imp) |
73 then have "P2 (l', r')" by auto |
79 then have "P2 (l', r')" by auto |
74 then obtain n2 |
80 then obtain n2 |
98 |
104 |
99 lemma Hoare_plus_unhalt: |
105 lemma Hoare_plus_unhalt: |
100 fixes A B :: tprog0 |
106 fixes A B :: tprog0 |
101 assumes aimpb: "Q1 \<mapsto> P2" |
107 assumes aimpb: "Q1 \<mapsto> P2" |
102 and A_wf : "tm_wf (A, 0)" |
108 and A_wf : "tm_wf (A, 0)" |
103 and B_wf : "tm_wf (B, 0)" |
109 and B_wf : "tm_wf (B, 0)" (* probably not needed *) |
104 and A_halt : "{P1} A {Q1}" |
110 and A_halt : "{P1} A {Q1}" |
105 and B_uhalt : "{P2} B" |
111 and B_uhalt : "{P2} B" |
106 shows "{P1} (A |+| B)" |
112 shows "{P1} (A |+| B)" |
107 proof(rule_tac Hoare_unhalt_I) |
113 proof(rule_tac Hoare_unhalt_I) |
108 fix l r |
114 fix l r |
111 using A_halt unfolding Hoare_def by auto |
117 using A_halt unfolding Hoare_def by auto |
112 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
118 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
113 by(case_tac "steps0 (1, l, r) A n1", auto) |
119 by(case_tac "steps0 (1, l, r) A n1", auto) |
114 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
120 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
115 using A_wf |
121 using A_wf |
116 by(rule_tac t_merge_pre_halt_same, auto) |
122 by(rule_tac tm_comp_pre_halt_same, auto) |
117 from c aimpb have "P2 holds_for (0, l', r')" |
123 from c aimpb have "P2 holds_for (0, l', r')" |
118 by(rule holds_for_imp) |
124 by(rule holds_for_imp) |
119 from this have "P2 (l', r')" by auto |
125 from this have "P2 (l', r')" by auto |
120 from this have e: "\<forall> n. \<not> is_final (steps0 (Suc 0, l', r') B n) " |
126 from this have e: "\<forall> n. \<not> is_final (steps0 (Suc 0, l', r') B n) " |
121 using B_uhalt unfolding Hoare_unhalt_def |
127 using B_uhalt unfolding Hoare_unhalt_def |