13 fun |
13 fun |
14 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) |
15 where |
15 where |
16 "P holds_for (s, l, r) = P (l, r)" |
16 "P holds_for (s, l, r) = P (l, r)" |
17 |
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_unhaltI: |
|
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 |
|
44 lemma is_final_holds[simp]: |
18 lemma is_final_holds[simp]: |
45 assumes "is_final c" |
19 assumes "is_final c" |
46 shows "Q holds_for (steps c p n) = Q holds_for c" |
20 shows "Q holds_for (steps c p n) = Q holds_for c" |
47 using assms |
21 using assms |
48 apply(induct n) |
22 apply(induct n) |
49 apply(auto) |
23 apply(auto) |
50 apply(case_tac [!] c) |
24 apply(case_tac [!] c) |
51 apply(auto) |
25 apply(auto) |
52 done |
26 done |
53 |
27 |
|
28 (* Hoare Rules *) |
|
29 |
|
30 (* halting case *) |
|
31 definition |
|
32 Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50) |
|
33 where |
|
34 "{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))" |
|
35 |
|
36 (* not halting case *) |
|
37 definition |
|
38 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50) |
|
39 where |
|
40 "{P} p \<up> \<equiv> \<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n)))" |
|
41 |
|
42 |
|
43 lemma Hoare_haltI: |
|
44 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)" |
|
45 shows "{P} p {Q}" |
|
46 unfolding Hoare_halt_def |
|
47 using assms by auto |
|
48 |
|
49 lemma Hoare_unhaltI: |
|
50 assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)" |
|
51 shows "{P} p \<up>" |
|
52 unfolding Hoare_unhalt_def |
|
53 using assms by auto |
|
54 |
|
55 |
|
56 |
54 |
57 |
55 text {* |
58 text {* |
56 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A well-formed |
59 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A well-formed |
57 --------------------------------------------------- |
60 --------------------------------------------------- |
58 {P1} A |+| B {Q2} |
61 {P1} A |+| B {Q2} |
59 *} |
62 *} |
60 |
63 |
61 |
64 |
62 lemma Hoare_plus_halt: |
65 lemma Hoare_plus_halt [case_names A_halt B_halt Imp A_wf]: |
63 assumes A_halt : "{P1} A {Q1}" |
66 assumes A_halt : "{P1} A {Q1}" |
64 and B_halt : "{P2} B {Q2}" |
67 and B_halt : "{P2} B {Q2}" |
65 and a_imp: "Q1 \<mapsto> P2" |
68 and a_imp: "Q1 \<mapsto> P2" |
66 and A_wf : "tm_wf (A, 0)" |
69 and A_wf : "tm_wf (A, 0)" |
67 shows "{P1} A |+| B {Q2}" |
70 shows "{P1} A |+| B {Q2}" |
68 proof(rule HoareI) |
71 proof(rule Hoare_haltI) |
69 fix l r |
72 fix l r |
70 assume h: "P1 (l, r)" |
73 assume h: "P1 (l, r)" |
71 then obtain n1 l' r' |
74 then obtain n1 l' r' |
72 where "is_final (steps0 (1, l, r) A n1)" |
75 where "is_final (steps0 (1, l, r) A n1)" |
73 and a1: "Q1 holds_for (steps0 (1, l, r) A n1)" |
76 and a1: "Q1 holds_for (steps0 (1, l, r) A n1)" |
74 and a2: "steps0 (1, l, r) A n1 = (0, l', r')" |
77 and a2: "steps0 (1, l, r) A n1 = (0, l', r')" |
75 using A_halt unfolding Hoare_def |
78 using A_halt unfolding Hoare_halt_def |
76 by (metis is_final_eq surj_pair) |
79 by (metis is_final_eq surj_pair) |
77 then obtain n2 |
80 then obtain n2 |
78 where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" |
81 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) |
82 using A_wf by (rule_tac tm_comp_pre_halt_same) |
80 moreover |
83 moreover |
81 from a1 a2 a_imp have "P2 (l', r')" by (simp add: assert_imp_def) |
84 from a1 a2 a_imp have "P2 (l', r')" by (simp add: assert_imp_def) |
82 then obtain n3 l'' r'' |
85 then obtain n3 l'' r'' |
83 where "is_final (steps0 (1, l', r') B n3)" |
86 where "is_final (steps0 (1, l', r') B n3)" |
84 and b1: "Q2 holds_for (steps0 (1, l', r') B n3)" |
87 and b1: "Q2 holds_for (steps0 (1, l', r') B n3)" |
85 and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')" |
88 and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')" |
86 using B_halt unfolding Hoare_def |
89 using B_halt unfolding Hoare_halt_def |
87 by (metis is_final_eq surj_pair) |
90 by (metis is_final_eq surj_pair) |
88 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n3 = (0, l'', r'')" |
91 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n3 = (0, l'', r'')" |
89 using A_wf by (rule_tac t_merge_second_halt_same) |
92 using A_wf by (rule_tac tm_comp_second_halt_same) |
90 ultimately show |
93 ultimately show |
91 "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)" |
94 "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)" |
92 using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) |
95 using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) |
93 qed |
96 qed |
94 |
97 |
119 assume h: "P1 (l, r)" |
122 assume h: "P1 (l, r)" |
120 then obtain n1 l' r' |
123 then obtain n1 l' r' |
121 where a: "is_final (steps0 (1, l, r) A n1)" |
124 where a: "is_final (steps0 (1, l, r) A n1)" |
122 and b: "Q1 holds_for (steps0 (1, l, r) A n1)" |
125 and b: "Q1 holds_for (steps0 (1, l, r) A n1)" |
123 and c: "steps0 (1, l, r) A n1 = (0, l', r')" |
126 and c: "steps0 (1, l, r) A n1 = (0, l', r')" |
124 using A_halt unfolding Hoare_def |
127 using A_halt unfolding Hoare_halt_def |
125 by (metis is_final_eq surj_pair) |
128 by (metis is_final_eq surj_pair) |
126 then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" |
129 then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" |
127 using A_wf by (rule_tac tm_comp_pre_halt_same) |
130 using A_wf by (rule_tac tm_comp_pre_halt_same) |
128 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
131 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
129 proof(cases "n2 \<le> n") |
132 proof(cases "n2 \<le> n") |
134 then have "\<not> is_final (steps0 (Suc 0, l', r') B (n - n2))" by auto |
137 then have "\<not> is_final (steps0 (Suc 0, l', r') B (n - n2))" by auto |
135 then obtain s'' l'' r'' |
138 then obtain s'' l'' r'' |
136 where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" |
139 where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" |
137 and "\<not> is_final (s'', l'', r'')" by (metis surj_pair) |
140 and "\<not> is_final (s'', l'', r'')" by (metis surj_pair) |
138 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" |
141 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" |
139 using A_wf by (auto dest: t_merge_second_same simp del: tm_wf.simps) |
142 using A_wf by (auto dest: tm_comp_second_same simp del: tm_wf.simps) |
140 then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" |
143 then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" |
141 using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) |
144 using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) |
142 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
145 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
143 using `n2 \<le> n` by simp |
146 using `n2 \<le> n` by simp |
144 next |
147 next |