133 by (simp) |
133 by (simp) |
134 |
134 |
135 ML {* val qty = @{typ "my_int"} *} |
135 ML {* val qty = @{typ "my_int"} *} |
136 ML {* val ty_name = "my_int" *} |
136 ML {* val ty_name = "my_int" *} |
137 ML {* val rsp_thms = @{thms ho_plus_rsp} *} |
137 ML {* val rsp_thms = @{thms ho_plus_rsp} *} |
138 ML {* val defs = @{thms PLUS_def} *} |
|
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
138 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
139 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
141 ML {* val consts = lookup_quot_consts defs *} |
140 |
142 |
141 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] *} |
143 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] defs *} |
|
144 |
142 |
145 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
143 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
144 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
147 |
145 |
148 |
146 |
149 lemma "PLUS a b = PLUS b a" |
147 lemma "PLUS a b = PLUS b a" |
150 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
148 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
149 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
152 prefer 2 |
150 prefer 2 |
153 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
151 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
154 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
152 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
155 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
153 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
156 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
154 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
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*}) |
186 |
184 |
187 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
185 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
188 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
186 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
189 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
187 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
190 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
188 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
191 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
189 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
192 done |
190 done |
193 |
191 |
194 lemma ho_tst: "foldl my_plus x [] = x" |
192 lemma ho_tst: "foldl my_plus x [] = x" |
195 apply simp |
193 apply simp |
196 done |
194 done |
283 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
281 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
284 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
282 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
285 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
283 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
286 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
284 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
287 apply(simp only: nil_prs) |
285 apply(simp only: nil_prs) |
288 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
286 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
289 done |
287 done |
290 |
288 |
291 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
289 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
292 sorry |
290 sorry |
293 |
291 |
295 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
293 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
296 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
294 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
297 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
295 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
298 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
296 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
299 apply(simp only: cons_prs[OF QUOTIENT_my_int]) |
297 apply(simp only: cons_prs[OF QUOTIENT_my_int]) |
300 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
298 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
301 done |
299 done |
302 |
300 |