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