equal
deleted
inserted
replaced
147 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
147 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
148 |
148 |
149 |
149 |
150 lemma "PLUS a b = PLUS b a" |
150 lemma "PLUS a b = PLUS b a" |
151 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
152 apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) |
152 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
153 prefer 2 |
153 prefer 2 |
154 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
154 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
155 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
155 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
156 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
156 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
157 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
157 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
187 apply (simp) |
187 apply (simp) |
188 done |
188 done |
189 |
189 |
190 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
190 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
191 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
191 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
192 apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) |
192 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
193 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
193 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
194 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
194 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
195 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
195 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
196 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
196 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
197 done |
197 done |
198 |
198 |
224 |> writeln |
224 |> writeln |
225 *} |
225 *} |
226 |
226 |
227 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
227 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
228 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
228 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
229 apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) |
229 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
230 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
230 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
231 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
231 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) *} |
232 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 *}) |
233 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
234 done |
234 done |