equal
deleted
inserted
replaced
148 |
148 |
149 lemma "PLUS a b = PLUS b a" |
149 lemma "PLUS a b = PLUS b a" |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
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 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
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 *}) |
|
156 apply(simp add: id_def) |
154 apply(simp add: id_def) |
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
155 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*}) |
192 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)" |
193 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
191 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
194 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
192 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
195 apply(simp) |
193 apply(simp) |
196 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
194 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
197 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
195 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
198 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
|
199 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
|
200 done |
196 done |
201 |
197 |
202 lemma ho_tst: "foldl my_plus x [] = x" |
198 lemma ho_tst: "foldl my_plus x [] = x" |
203 apply simp |
199 apply simp |
204 done |
200 done |
215 lemma "foldl PLUS x [] = x" |
211 lemma "foldl PLUS x [] = x" |
216 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
212 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
217 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
213 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
218 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
214 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
219 apply(simp add: map_prs) |
215 apply(simp add: map_prs) |
220 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
221 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *} |
|
222 apply(simp only: map_prs) |
216 apply(simp only: map_prs) |
223 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
217 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
224 sorry |
218 sorry |
225 |
219 |
226 (* |
220 (* |
227 FIXME: All below is your construction code; mostly commented out as it |
221 FIXME: All below is your construction code; mostly commented out as it |
228 does not work. |
222 does not work. |
231 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
225 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
232 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
226 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
233 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
227 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
234 apply(simp) |
228 apply(simp) |
235 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
229 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
236 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
230 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
237 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
231 done |
238 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
232 |
239 done |
233 |
240 |
|
241 |
|