137 theorem add_homomorph_lb: |
137 theorem add_homomorph_lb: |
138 "{} \<turnstile> {\<lambda>s. s:s<This> \<ge> X \<and> s:s<Par> \<ge> Y} Meth(Nat,add) {\<lambda>s. s:s<Res> \<ge> X+Y}" |
138 "{} \<turnstile> {\<lambda>s. s:s<This> \<ge> X \<and> s:s<Par> \<ge> Y} Meth(Nat,add) {\<lambda>s. s:s<Res> \<ge> X+Y}" |
139 apply (rule hoare_ehoare.Meth) (* 1 *) |
139 apply (rule hoare_ehoare.Meth) (* 1 *) |
140 apply clarsimp |
140 apply clarsimp |
141 apply (rule_tac P'= "\<lambda>Z s. (s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z) \<and> D=Nat" and |
141 apply (rule_tac P'= "\<lambda>Z s. (s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z) \<and> D=Nat" and |
142 Q'= "\<lambda>Z s. s:s<Res> \<ge> fst Z+snd Z" in Conseq) |
142 Q'= "\<lambda>Z s. s:s<Res> \<ge> fst Z+snd Z" in AxSem.Conseq) |
143 prefer 2 |
143 prefer 2 |
144 apply (clarsimp simp add: init_locs_def init_vars_def) |
144 apply (clarsimp simp add: init_locs_def init_vars_def) |
145 apply rule |
145 apply rule |
146 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) |
146 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) |
147 apply (rule_tac P = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in Impl1) |
147 apply (rule_tac P = "\<lambda>Z Cm s. s:s<This> \<ge> fst Z \<and> s:s<Par> \<ge> snd Z" in AxSem.Impl1) |
148 apply (clarsimp simp add: body_def) (* 4 *) |
148 apply (clarsimp simp add: body_def) (* 4 *) |
149 apply (rename_tac n m) |
149 apply (rename_tac n m) |
150 apply (rule_tac Q = "\<lambda>v s. (s:s<This> \<ge> n \<and> s:s<Par> \<ge> m) \<and> |
150 apply (rule_tac Q = "\<lambda>v s. (s:s<This> \<ge> n \<and> s:s<Par> \<ge> m) \<and> |
151 (\<exists>a. s<This> = Addr a \<and> v = get_field s a pred)" in hoare_ehoare.Cond) |
151 (\<exists>a. s<This> = Addr a \<and> v = get_field s a pred)" in hoare_ehoare.Cond) |
152 apply (rule hoare_ehoare.FAcc) |
152 apply (rule hoare_ehoare.FAcc) |
173 prefer 2 |
173 prefer 2 |
174 apply clarsimp |
174 apply clarsimp |
175 apply (rule hoare_ehoare.Meth) (* 17 *) |
175 apply (rule hoare_ehoare.Meth) (* 17 *) |
176 apply clarsimp |
176 apply clarsimp |
177 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) |
177 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) |
178 apply (rule Conseq) |
178 apply (rule AxSem.Conseq) |
179 apply rule |
179 apply rule |
180 apply (rule hoare_ehoare.Asm) (* 20 *) |
180 apply (rule hoare_ehoare.Asm) (* 20 *) |
181 apply (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+) |
181 apply (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+) |
182 apply (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono) |
182 apply (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono) |
183 apply rule |
183 apply rule |
187 apply (rule hoare_ehoare.LAcc) |
187 apply (rule hoare_ehoare.LAcc) |
188 apply clarify |
188 apply clarify |
189 apply (rule hoare_ehoare.Meth) (* 24 *) |
189 apply (rule hoare_ehoare.Meth) (* 24 *) |
190 apply clarsimp |
190 apply clarsimp |
191 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) |
191 apply (case_tac "D = Nat", simp_all, rule_tac [2] cFalse) |
192 apply (rule Impl1) |
192 apply (rule AxSem.Impl1) |
193 apply (clarsimp simp add: body_def) |
193 apply (clarsimp simp add: body_def) |
194 apply (rule hoare_ehoare.Comp) (* 26 *) |
194 apply (rule hoare_ehoare.Comp) (* 26 *) |
195 prefer 2 |
195 prefer 2 |
196 apply (rule hoare_ehoare.FAss) |
196 apply (rule hoare_ehoare.FAss) |
197 prefer 2 |
197 prefer 2 |