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