118 (cut_facts_tac prems 1), |
118 (cut_facts_tac prems 1), |
119 (nat_ind_tac "k" 1), |
119 (nat_ind_tac "k" 1), |
120 (Asm_simp_tac 1), |
120 (Asm_simp_tac 1), |
121 (strip_tac 1), |
121 (strip_tac 1), |
122 (simp_tac (!simpset addsimps [step_def2]) 1), |
122 (simp_tac (!simpset addsimps [step_def2]) 1), |
123 (res_inst_tac [("p","b`(iterate k1 (step`b`g) x)")] trE 1), |
123 (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1), |
124 (etac notE 1), |
124 (etac notE 1), |
125 (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1), |
125 (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1), |
126 (asm_simp_tac HOLCF_ss 1), |
126 (asm_simp_tac HOLCF_ss 1), |
127 (rtac mp 1), |
127 (rtac mp 1), |
128 (etac spec 1), |
128 (etac spec 1), |
129 (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] |
129 (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] |
130 addsimps [loop_lemma2] ) 1), |
130 addsimps [loop_lemma2] ) 1), |
131 (res_inst_tac [("s","iterate (Suc k1) (step`b`g) x"), |
131 (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"), |
132 ("t","g`(iterate k1 (step`b`g) x)")] ssubst 1), |
132 ("t","g`(iterate k (step`b`g) x)")] ssubst 1), |
133 (atac 2), |
133 (atac 2), |
134 (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1), |
134 (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1), |
135 (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] |
135 (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] |
136 addsimps [loop_lemma2] ) 1) |
136 addsimps [loop_lemma2] ) 1) |
137 ]); |
137 ]); |