|
1 theory Turing_Hoare |
|
2 imports Turing |
|
3 begin |
|
4 |
|
5 |
|
6 type_synonym assert = "tape \<Rightarrow> bool" |
|
7 |
|
8 definition |
|
9 assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
|
10 where |
|
11 "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)" |
|
12 |
|
13 lemma [intro, simp]: |
|
14 "P \<mapsto> P" |
|
15 unfolding assert_imp_def by simp |
|
16 |
|
17 fun |
|
18 holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100) |
|
19 where |
|
20 "P holds_for (s, l, r) = P (l, r)" |
|
21 |
|
22 lemma is_final_holds[simp]: |
|
23 assumes "is_final c" |
|
24 shows "Q holds_for (steps c p n) = Q holds_for c" |
|
25 using assms |
|
26 apply(induct n) |
|
27 apply(auto) |
|
28 apply(case_tac [!] c) |
|
29 apply(auto) |
|
30 done |
|
31 |
|
32 (* Hoare Rules *) |
|
33 |
|
34 (* halting case *) |
|
35 definition |
|
36 Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
|
37 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))" |
|
39 |
|
40 |
|
41 (* not halting case *) |
|
42 definition |
|
43 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50) |
|
44 where |
|
45 "{P} p \<up> \<equiv> \<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n)))" |
|
46 |
|
47 |
|
48 lemma Hoare_haltI: |
|
49 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)" |
|
50 shows "{P} p {Q}" |
|
51 unfolding Hoare_halt_def |
|
52 using assms by auto |
|
53 |
|
54 lemma Hoare_unhaltI: |
|
55 assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)" |
|
56 shows "{P} p \<up>" |
|
57 unfolding Hoare_unhalt_def |
|
58 using assms by auto |
|
59 |
|
60 |
|
61 |
|
62 |
|
63 text {* |
|
64 {P} A {Q} {Q} B {S} A well-formed |
|
65 ----------------------------------------- |
|
66 {P} A |+| B {S} |
|
67 *} |
|
68 |
|
69 |
|
70 lemma Hoare_plus_halt [case_names A_halt B_halt A_wf]: |
|
71 assumes A_halt : "{P} A {Q}" |
|
72 and B_halt : "{Q} B {S}" |
|
73 and A_wf : "tm_wf (A, 0)" |
|
74 shows "{P} A |+| B {S}" |
|
75 proof(rule Hoare_haltI) |
|
76 fix l r |
|
77 assume h: "P (l, r)" |
|
78 then obtain n1 l' r' |
|
79 where "is_final (steps0 (1, l, r) A n1)" |
|
80 and a1: "Q holds_for (steps0 (1, l, r) A n1)" |
|
81 and a2: "steps0 (1, l, r) A n1 = (0, l', r')" |
|
82 using A_halt unfolding Hoare_halt_def |
|
83 by (metis is_final_eq surj_pair) |
|
84 then obtain n2 |
|
85 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) |
|
87 moreover |
|
88 from a1 a2 have "Q (l', r')" by (simp) |
|
89 then obtain n3 l'' r'' |
|
90 where "is_final (steps0 (1, l', r') B n3)" |
|
91 and b1: "S holds_for (steps0 (1, l', r') B n3)" |
|
92 and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')" |
|
93 using B_halt unfolding Hoare_halt_def |
|
94 by (metis is_final_eq surj_pair) |
|
95 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) |
|
97 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)" |
|
99 using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) |
|
100 qed |
|
101 |
|
102 text {* |
|
103 {P} A {Q} {Q} B loops A well-formed |
|
104 ------------------------------------------ |
|
105 {P} A |+| B loops |
|
106 *} |
|
107 |
|
108 lemma Hoare_plus_unhalt [case_names A_halt B_unhalt A_wf]: |
|
109 assumes A_halt: "{P} A {Q}" |
|
110 and B_uhalt: "{Q} B \<up>" |
|
111 and A_wf : "tm_wf (A, 0)" |
|
112 shows "{P} (A |+| B) \<up>" |
|
113 proof(rule_tac Hoare_unhaltI) |
|
114 fix n l r |
|
115 assume h: "P (l, r)" |
|
116 then obtain n1 l' r' |
|
117 where a: "is_final (steps0 (1, l, r) A n1)" |
|
118 and b: "Q holds_for (steps0 (1, l, r) A n1)" |
|
119 and c: "steps0 (1, l, r) A n1 = (0, l', r')" |
|
120 using A_halt unfolding Hoare_halt_def |
|
121 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')" |
|
123 using A_wf by (rule_tac tm_comp_pre_halt_same) |
|
124 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
125 proof(cases "n2 \<le> n") |
|
126 case True |
|
127 from b c have "Q (l', r')" by simp |
|
128 then have "\<forall> n. \<not> is_final (steps0 (1, l', r') B n) " |
|
129 using B_uhalt unfolding Hoare_unhalt_def by simp |
|
130 then have "\<not> is_final (steps0 (1, l', r') B (n - n2))" by auto |
|
131 then obtain s'' l'' r'' |
|
132 where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" |
|
133 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'')" |
|
135 using A_wf by (auto dest: tm_comp_second_same simp del: tm_wf.simps) |
|
136 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) |
|
138 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
139 using `n2 \<le> n` by simp |
|
140 next |
|
141 case False |
|
142 then obtain n3 where "n = n2 - n3" |
|
143 by (metis diff_le_self le_imp_diff_is_add nat_add_commute nat_le_linear) |
|
144 moreover |
|
145 with eq show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
146 by (simp add: not_is_final[where ?n1.0="n2"]) |
|
147 qed |
|
148 qed |
|
149 |
|
150 lemma Hoare_consequence: |
|
151 assumes "P' \<mapsto> P" "{P} p {Q}" "Q \<mapsto> Q'" |
|
152 shows "{P'} p {Q'}" |
|
153 using assms |
|
154 unfolding Hoare_halt_def assert_imp_def |
|
155 by (metis holds_for.simps surj_pair) |
|
156 |
|
157 |
|
158 |
|
159 end |