equal
deleted
inserted
replaced
102 apply (simp (no_asm_simp)) |
102 apply (simp (no_asm_simp)) |
103 apply (intro strip) |
103 apply (intro strip) |
104 apply (simp (no_asm) add: step_def2) |
104 apply (simp (no_asm) add: step_def2) |
105 apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE) |
105 apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE) |
106 apply (erule notE) |
106 apply (erule notE) |
107 apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [thm "step_def2"]) 1 *}) |
107 apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [@{thm step_def2}]) 1 *}) |
108 apply (tactic "asm_simp_tac HOLCF_ss 1") |
108 apply (tactic "asm_simp_tac HOLCF_ss 1") |
109 apply (rule mp) |
109 apply (rule mp) |
110 apply (erule spec) |
110 apply (erule spec) |
111 apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [thm "iterate_Suc"] |
111 apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}] |
112 addsimps [thm "loop_lemma2"]) 1 *}) |
112 addsimps [@{thm loop_lemma2}]) 1 *}) |
113 apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x" |
113 apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x" |
114 and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst) |
114 and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst) |
115 prefer 2 apply (assumption) |
115 prefer 2 apply (assumption) |
116 apply (simp add: step_def2) |
116 apply (simp add: step_def2) |
117 apply (drule (1) loop_lemma2, simp) |
117 apply (drule (1) loop_lemma2, simp) |