equal
deleted
inserted
replaced
265 done |
265 done |
266 |
266 |
267 lemma hoare_lemma19: |
267 lemma hoare_lemma19: |
268 "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)" |
268 "(ALL k. (b1::'a->tr)$(iterate k$g$x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)" |
269 apply (rule flat_codom) |
269 apply (rule flat_codom) |
270 apply (rule_tac t = "x1" in iterate_0 [THEN subst]) |
270 apply (rule_tac t = "x" in iterate_0 [THEN subst]) |
271 apply (erule spec) |
271 apply (erule spec) |
272 done |
272 done |
273 |
273 |
274 lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU" |
274 lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU" |
275 apply (rule q_def [THEN eq_reflection, THEN def_fix_ind]) |
275 apply (rule q_def [THEN eq_reflection, THEN def_fix_ind]) |