equal
deleted
inserted
replaced
51 apply(auto) |
51 apply(auto) |
52 done |
52 done |
53 |
53 |
54 |
54 |
55 text {* |
55 text {* |
56 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A, B well-formed |
56 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A well-formed |
57 ------------------------------------------------------ |
57 --------------------------------------------------- |
58 {P1} A |+| B {Q2} |
58 {P1} A |+| B {Q2} |
59 *} |
59 *} |
60 |
60 |
61 |
61 |
62 lemma Hoare_plus_halt: |
62 lemma Hoare_plus_halt: |
63 assumes a_imp: "Q1 \<mapsto> P2" |
63 assumes A_halt : "{P1} A {Q1}" |
|
64 and B_halt : "{P2} B {Q2}" |
|
65 and a_imp: "Q1 \<mapsto> P2" |
64 and A_wf : "tm_wf (A, 0)" |
66 and A_wf : "tm_wf (A, 0)" |
65 and A_halt : "{P1} A {Q1}" |
|
66 and B_halt : "{P2} B {Q2}" |
|
67 shows "{P1} A |+| B {Q2}" |
67 shows "{P1} A |+| B {Q2}" |
68 proof(rule HoareI) |
68 proof(rule HoareI) |
69 fix l r |
69 fix l r |
70 assume h: "P1 (l, r)" |
70 assume h: "P1 (l, r)" |
71 then obtain n1 l' r' |
71 then obtain n1 l' r' |
101 |
101 |
102 |
102 |
103 |
103 |
104 |
104 |
105 lemma Hoare_plus_unhalt: |
105 lemma Hoare_plus_unhalt: |
106 assumes a_imp: "Q1 \<mapsto> P2" |
106 assumes A_halt: "{P1} A {Q1}" |
|
107 and B_uhalt: "{P2} B \<up>" |
|
108 and a_imp: "Q1 \<mapsto> P2" |
107 and A_wf : "tm_wf (A, 0)" |
109 and A_wf : "tm_wf (A, 0)" |
108 and A_halt : "{P1} A {Q1}" |
|
109 and B_uhalt : "{P2} B \<up>" |
|
110 shows "{P1} (A |+| B) \<up>" |
110 shows "{P1} (A |+| B) \<up>" |
111 proof(rule_tac Hoare_unhalt_I) |
111 proof(rule_tac Hoare_unhalt_I) |
112 fix n l r |
112 fix n l r |
113 assume h: "P1 (l, r)" |
113 assume h: "P1 (l, r)" |
114 then obtain n1 l' r' |
114 then obtain n1 l' r' |
153 using assms |
153 using assms |
154 unfolding Hoare_def assert_imp_def |
154 unfolding Hoare_def assert_imp_def |
155 by (metis holds_for.simps surj_pair) |
155 by (metis holds_for.simps surj_pair) |
156 |
156 |
157 |
157 |
158 declare tm_comp.simps [simp del] |
|
159 declare adjust.simps[simp del] |
|
160 declare shift.simps[simp del] |
|
161 declare tm_wf.simps[simp del] |
|
162 declare step.simps[simp del] |
|
163 declare steps.simps[simp del] |
|
164 |
|
165 |
|
166 |
158 |
167 end |
159 end |