equal
deleted
inserted
replaced
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
152 prefer 2 |
152 prefer 2 |
153 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
153 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
154 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
154 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
155 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
155 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
|
156 apply(simp add: id_def) |
|
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
|
158 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
156 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
159 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
160 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
158 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
161 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
159 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
162 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
160 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
163 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
187 done |
190 done |
188 |
191 |
189 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
192 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
190 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
193 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
191 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
194 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
|
195 apply(simp) |
192 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
196 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
193 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
197 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
194 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
198 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
195 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
199 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
196 done |
200 done |
225 *) |
229 *) |
226 |
230 |
227 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
231 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
228 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
232 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
229 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
233 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
|
234 apply(simp) |
230 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
235 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
231 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
236 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
232 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
237 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
233 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
238 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
234 done |
239 done |