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