|
1 theory turing_hoare |
|
2 imports turing_basic |
|
3 begin |
|
4 |
|
5 |
|
6 |
|
7 type_synonym assert = "tape \<Rightarrow> bool" |
|
8 |
|
9 definition |
|
10 assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
|
11 where |
|
12 "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)" |
|
13 |
|
14 |
|
15 |
|
16 fun |
|
17 holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100) |
|
18 where |
|
19 "P holds_for (s, l, r) = P (l, r)" |
|
20 |
|
21 lemma is_final_holds[simp]: |
|
22 assumes "is_final c" |
|
23 shows "Q holds_for (steps c (p, off) n) = Q holds_for c" |
|
24 using assms |
|
25 apply(induct n) |
|
26 apply(auto) |
|
27 apply(case_tac [!] c) |
|
28 apply(auto) |
|
29 done |
|
30 |
|
31 lemma holds_for_imp: |
|
32 assumes "P holds_for c" |
|
33 and "P \<mapsto> Q" |
|
34 shows "Q holds_for c" |
|
35 using assms unfolding assert_imp_def |
|
36 by (case_tac c) (auto) |
|
37 |
|
38 definition |
|
39 Hoare :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
|
40 where |
|
41 "{P} p {Q} \<equiv> |
|
42 (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)))" |
|
43 |
|
44 lemma HoareI: |
|
45 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)" |
|
46 shows "{P} p {Q}" |
|
47 unfolding Hoare_def using assms by auto |
|
48 |
|
49 |
|
50 text {* |
|
51 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 |
|
52 ----------------------------------- |
|
53 {P1} A |+| B {Q2} |
|
54 *} |
|
55 |
|
56 |
|
57 lemma Hoare_plus_halt: |
|
58 assumes aimpb: "Q1 \<mapsto> P2" |
|
59 and A_wf : "tm_wf (A, 0)" |
|
60 and B_wf : "tm_wf (B, 0)" |
|
61 and A_halt : "{P1} A {Q1}" |
|
62 and B_halt : "{P2} B {Q2}" |
|
63 shows "{P1} A |+| B {Q2}" |
|
64 proof(rule HoareI) |
|
65 fix l r |
|
66 assume h: "P1 (l, r)" |
|
67 then obtain n1 |
|
68 where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)" |
|
69 using A_halt unfolding Hoare_def by auto |
|
70 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
|
71 by(case_tac "steps0 (1, l, r) A n1") (auto) |
|
72 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
|
73 using A_wf by(rule_tac t_merge_pre_halt_same) (auto) |
|
74 moreover |
|
75 from c aimpb have "P2 holds_for (0, l', r')" |
|
76 by (rule holds_for_imp) |
|
77 then have "P2 (l', r')" by auto |
|
78 then obtain n2 |
|
79 where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)" |
|
80 using B_halt unfolding Hoare_def by auto |
|
81 then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" |
|
82 by (case_tac "steps0 (1, l', r') B n2", auto) |
|
83 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')" |
|
84 by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf) |
|
85 ultimately show |
|
86 "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)" |
|
87 using g |
|
88 apply(rule_tac x = "stpa + n2" in exI) |
|
89 apply(simp add: steps_add) |
|
90 done |
|
91 qed |
|
92 |
|
93 definition |
|
94 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50) |
|
95 where |
|
96 "{P} p \<equiv> |
|
97 (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))" |
|
98 |
|
99 lemma Hoare_unhalt_I: |
|
100 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)" |
|
101 shows "{P} p" |
|
102 unfolding Hoare_unhalt_def using assms by auto |
|
103 |
|
104 lemma Hoare_plus_unhalt: |
|
105 fixes A B :: tprog0 |
|
106 assumes aimpb: "Q1 \<mapsto> P2" |
|
107 and A_wf : "tm_wf (A, 0)" |
|
108 and B_wf : "tm_wf (B, 0)" |
|
109 and A_halt : "{P1} A {Q1}" |
|
110 and B_uhalt : "{P2} B" |
|
111 shows "{P1} (A |+| B)" |
|
112 proof(rule_tac Hoare_unhalt_I) |
|
113 fix l r |
|
114 assume h: "P1 (l, r)" |
|
115 then obtain n1 where a: "is_final (steps0 (1, l, r) A n1)" and b: "Q1 holds_for (steps0 (1, l, r) A n1)" |
|
116 using A_halt unfolding Hoare_def by auto |
|
117 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
|
118 by(case_tac "steps0 (1, l, r) A n1", auto) |
|
119 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
|
120 using A_wf |
|
121 by(rule_tac t_merge_pre_halt_same, auto) |
|
122 from c aimpb have "P2 holds_for (0, l', r')" |
|
123 by(rule holds_for_imp) |
|
124 from this have "P2 (l', r')" by auto |
|
125 from this have e: "\<forall> n. \<not> is_final (steps0 (Suc 0, l', r') B n) " |
|
126 using B_uhalt unfolding Hoare_unhalt_def |
|
127 by auto |
|
128 from e show "\<forall>n. \<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
129 proof(rule_tac allI, case_tac "n > stpa") |
|
130 fix n |
|
131 assume h2: "stpa < n" |
|
132 hence "\<not> is_final (steps0 (Suc 0, l', r') B (n - stpa))" |
|
133 using e |
|
134 apply(erule_tac x = "n - stpa" in allE) by simp |
|
135 then obtain s'' l'' r'' where f: "steps0 (Suc 0, l', r') B (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0" |
|
136 apply(case_tac "steps0 (Suc 0, l', r') B (n - stpa)", auto) |
|
137 done |
|
138 have k: "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - stpa) = (s''+ length A div 2, l'', r'') " |
|
139 using A_wf B_wf f g |
|
140 apply(drule_tac t_merge_second_same, auto) |
|
141 done |
|
142 show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
143 proof - |
|
144 have "\<not> is_final (steps0 (1, l, r) (A |+| B) (stpa + (n - stpa)))" |
|
145 using d k A_wf |
|
146 apply(simp only: steps_add d, simp add: tm_wf.simps) |
|
147 done |
|
148 thus "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
149 using h2 by simp |
|
150 qed |
|
151 next |
|
152 fix n |
|
153 assume h2: "\<not> stpa < n" |
|
154 with d show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
155 apply(auto) |
|
156 apply(subgoal_tac "\<exists> d. stpa = n + d", auto) |
|
157 apply(case_tac "(steps0 (Suc 0, l, r) (A |+| B) n)", simp) |
|
158 apply(rule_tac x = "stpa - n" in exI, simp) |
|
159 done |
|
160 qed |
|
161 qed |
|
162 |
|
163 lemma Hoare_weak: |
|
164 fixes p::tprog0 |
|
165 assumes a: "{P} p {Q}" |
|
166 and b: "P' \<mapsto> P" |
|
167 and c: "Q \<mapsto> Q'" |
|
168 shows "{P'} p {Q'}" |
|
169 using assms |
|
170 unfolding Hoare_def assert_imp_def |
|
171 by (blast intro: holds_for_imp[simplified assert_imp_def]) |
|
172 |
|
173 end |