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)" |
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}" |
34 shows "{P} p {Q}" |
35 unfolding Hoare_def |
35 unfolding Hoare_def |
36 using assms by auto |
36 using assms by auto |
37 |
37 |
38 lemma Hoare_unhalt_I: |
38 lemma Hoare_unhaltI: |
39 assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)" |
39 assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)" |
40 shows "{P} p \<up>" |
40 shows "{P} p \<up>" |
41 unfolding Hoare_unhalt_def |
41 unfolding Hoare_unhalt_def |
42 using assms by auto |
42 using assms by auto |
43 |
43 |
90 ultimately show |
90 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)" |
91 "\<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) |
92 using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) |
93 qed |
93 qed |
94 |
94 |
|
95 lemma Hoare_plus_halt_simple [case_names A_halt B_halt A_wf]: |
|
96 assumes A_halt : "{P1} A {P2}" |
|
97 and B_halt : "{P2} B {P3}" |
|
98 and A_wf : "tm_wf (A, 0)" |
|
99 shows "{P1} A |+| B {P3}" |
|
100 by (rule Hoare_plus_halt[OF A_halt B_halt _ A_wf]) |
|
101 (simp add: assert_imp_def) |
|
102 |
|
103 |
95 |
104 |
96 text {* |
105 text {* |
97 {P1} A {Q1} {P2} B loops Q1 \<mapsto> P2 A well-formed |
106 {P1} A {Q1} {P2} B loops Q1 \<mapsto> P2 A well-formed |
98 ------------------------------------------------------ |
107 ------------------------------------------------------ |
99 {P1} A |+| B loops |
108 {P1} A |+| B loops |
100 *} |
109 *} |
101 |
110 |
102 |
|
103 |
|
104 |
|
105 lemma Hoare_plus_unhalt: |
111 lemma Hoare_plus_unhalt: |
106 assumes A_halt: "{P1} A {Q1}" |
112 assumes A_halt: "{P1} A {Q1}" |
107 and B_uhalt: "{P2} B \<up>" |
113 and B_uhalt: "{P2} B \<up>" |
108 and a_imp: "Q1 \<mapsto> P2" |
114 and a_imp: "Q1 \<mapsto> P2" |
109 and A_wf : "tm_wf (A, 0)" |
115 and A_wf : "tm_wf (A, 0)" |
110 shows "{P1} (A |+| B) \<up>" |
116 shows "{P1} (A |+| B) \<up>" |
111 proof(rule_tac Hoare_unhalt_I) |
117 proof(rule_tac Hoare_unhaltI) |
112 fix n l r |
118 fix n l r |
113 assume h: "P1 (l, r)" |
119 assume h: "P1 (l, r)" |
114 then obtain n1 l' r' |
120 then obtain n1 l' r' |
115 where a: "is_final (steps0 (1, l, r) A n1)" |
121 where a: "is_final (steps0 (1, l, r) A n1)" |
116 and b: "Q1 holds_for (steps0 (1, l, r) A n1)" |
122 and b: "Q1 holds_for (steps0 (1, l, r) A n1)" |
143 with eq show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
149 with eq show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
144 by (simp add: not_is_final[where ?n1.0="n2"]) |
150 by (simp add: not_is_final[where ?n1.0="n2"]) |
145 qed |
151 qed |
146 qed |
152 qed |
147 |
153 |
|
154 lemma Hoare_plus_unhalt_simple [case_names A_halt B_unhalt A_wf]: |
|
155 assumes A_halt: "{P1} A {P2}" |
|
156 and B_uhalt: "{P2} B \<up>" |
|
157 and A_wf : "tm_wf (A, 0)" |
|
158 shows "{P1} (A |+| B) \<up>" |
|
159 by (rule Hoare_plus_unhalt[OF A_halt B_uhalt _ A_wf]) |
|
160 (simp add: assert_imp_def) |
|
161 |
|
162 |
148 lemma Hoare_weak: |
163 lemma Hoare_weak: |
149 assumes a: "{P} p {Q}" |
164 assumes a: "{P} p {Q}" |
150 and b: "P' \<mapsto> P" |
165 and b: "P' \<mapsto> P" |
151 and c: "Q \<mapsto> Q'" |
166 and c: "Q \<mapsto> Q'" |
152 shows "{P'} p {Q'}" |
167 shows "{P'} p {Q'}" |