equal
deleted
inserted
replaced
149 |
149 |
150 lemma cheat: "P" sorry |
150 lemma cheat: "P" sorry |
151 |
151 |
152 lemma "PLUS a b = PLUS b a" |
152 lemma "PLUS a b = PLUS b a" |
153 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
153 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
154 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
154 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
155 prefer 2 |
155 prefer 2 |
156 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
156 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
157 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
157 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
158 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
158 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
189 apply (simp) |
189 apply (simp) |
190 done |
190 done |
191 |
191 |
192 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)" |
193 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
193 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
194 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
194 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
195 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
195 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
196 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
196 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
197 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
197 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
198 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
198 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
199 done |
199 done |
200 |
200 |
226 |> writeln |
226 |> writeln |
227 *} |
227 *} |
228 |
228 |
229 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
229 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
230 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
230 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
231 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) |
231 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
232 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
232 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
233 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
233 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
236 done |
236 done |