105 ultimately |
105 ultimately |
106 show ?case by blast |
106 show ?case by blast |
107 next |
107 next |
108 case WhileFalse |
108 case WhileFalse |
109 thus ?case by (auto simp: bequiv_up_to_def) |
109 thus ?case by (auto simp: bequiv_up_to_def) |
110 qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+ |
110 qed (fastforce simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+ |
111 |
111 |
112 lemma bequiv_context_subst: |
112 lemma bequiv_context_subst: |
113 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)" |
113 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)" |
114 by (auto simp: bequiv_up_to_def) |
114 by (auto simp: bequiv_up_to_def) |
115 |
115 |
126 done |
126 done |
127 |
127 |
128 lemma equiv_up_to_while_weak: |
128 lemma equiv_up_to_while_weak: |
129 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> |
129 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> |
130 P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'" |
130 P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'" |
131 by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken |
131 by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken |
132 simp: hoare_valid_def) |
132 simp: hoare_valid_def) |
133 |
133 |
134 lemma equiv_up_to_if: |
134 lemma equiv_up_to_if: |
135 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow> |
135 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow> |
136 P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'" |
136 P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'" |
137 by (auto simp: bequiv_up_to_def equiv_up_to_def) |
137 by (auto simp: bequiv_up_to_def equiv_up_to_def) |
138 |
138 |
139 lemma equiv_up_to_if_weak: |
139 lemma equiv_up_to_if_weak: |
140 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow> |
140 "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow> |
141 P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'" |
141 P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'" |
142 by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken) |
142 by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken) |
143 |
143 |
144 lemma equiv_up_to_if_True [intro!]: |
144 lemma equiv_up_to_if_True [intro!]: |
145 "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1" |
145 "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1" |
146 by (auto simp: equiv_up_to_def) |
146 by (auto simp: equiv_up_to_def) |
147 |
147 |