equal
deleted
inserted
replaced
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
141 ML {* val consts = lookup_quot_consts defs *} |
141 ML {* val consts = lookup_quot_consts defs *} |
142 |
142 |
143 ML {* |
143 ML {* |
144 fun lift_tac_fset lthy t = |
144 fun lift_tac_fset lthy t = |
145 lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs |
145 lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs |
146 *} |
146 *} |
147 |
147 |
148 lemma "PLUS a b = PLUS b a" |
148 lemma "PLUS a b = PLUS b a" |
149 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
149 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
150 |
150 |
164 apply simp |
164 apply simp |
165 done |
165 done |
166 |
166 |
167 lemma "foldl PLUS x [] = x" |
167 lemma "foldl PLUS x [] = x" |
168 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) |
168 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) |
169 prefer 3 |
|
170 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
|
171 sorry |
169 sorry |
172 |
170 |
173 (* |
171 (* |
174 FIXME: All below is your construction code; mostly commented out as it |
172 FIXME: All below is your construction code; mostly commented out as it |
175 does not work. |
173 does not work. |