127 apply(cases a) |
129 apply(cases a) |
128 apply(cases b) |
130 apply(cases b) |
129 apply(auto) |
131 apply(auto) |
130 done |
132 done |
131 |
133 |
132 lemma ho_plus_rsp[quot_rsp]: |
134 lemma ho_plus_rsp[quotient_rsp]: |
133 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
135 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
134 by (simp) |
136 by (simp) |
135 |
137 |
136 ML {* val qty = @{typ "my_int"} *} |
138 ML {* val qty = @{typ "my_int"} *} |
137 ML {* val ty_name = "my_int" *} |
139 ML {* val ty_name = "my_int" *} |
138 ML {* val rsp_thms = @{thms ho_plus_rsp} *} |
140 ML {* val rsp_thms = @{thms ho_plus_rsp} *} |
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
141 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"; *} |
142 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
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] *} |
143 |
145 |
144 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
146 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
145 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} |
147 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} |
146 |
148 |
147 |
149 |
148 lemma "PLUS a b = PLUS b a" |
150 lemma "PLUS a b = PLUS b a" |
149 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
150 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
152 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
151 prefer 2 |
153 prefer 2 |
152 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
154 apply(tactic {* clean_tac @{context} 1 *}) |
153 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
155 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
154 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
156 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
155 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
156 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
158 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
157 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
159 apply(tactic {* inj_repabs_tac_intex @{context} 1*}) |
185 |
187 |
186 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
188 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
187 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
189 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
188 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
190 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
189 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
191 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
190 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
192 apply(tactic {* clean_tac @{context} 1 *}) |
191 done |
193 done |
192 |
194 |
193 lemma ho_tst: "foldl my_plus x [] = x" |
195 lemma ho_tst: "foldl my_plus x [] = x" |
194 apply simp |
196 apply simp |
195 done |
197 done |
232 assumes a: "QUOTIENT R1 abs1 rep1" |
234 assumes a: "QUOTIENT R1 abs1 rep1" |
233 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
235 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
234 apply (induct t) |
236 apply (induct t) |
235 by (simp_all add: QUOTIENT_ABS_REP[OF a]) |
237 by (simp_all add: QUOTIENT_ABS_REP[OF a]) |
236 |
238 |
237 lemma cons_rsp[quot_rsp]: |
239 lemma cons_rsp[quotient_rsp]: |
238 "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #" |
240 "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #" |
239 by simp |
241 by simp |
240 |
242 |
241 (* I believe it's true. *) |
243 (* I believe it's true. *) |
242 lemma foldl_rsp[quot_rsp]: |
244 lemma foldl_rsp[quotient_rsp]: |
243 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl" |
245 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl" |
244 apply (simp only: FUN_REL.simps) |
246 apply (simp only: FUN_REL.simps) |
245 apply (rule allI) |
247 apply (rule allI) |
246 apply (rule allI) |
248 apply (rule allI) |
247 apply (rule impI) |
249 apply (rule impI) |
252 apply (rule allI) |
254 apply (rule allI) |
253 apply (rule impI) |
255 apply (rule impI) |
254 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
256 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
255 sorry |
257 sorry |
256 |
258 |
257 lemma nil_listrel_rsp[quot_rsp]: |
259 lemma nil_listrel_rsp[quotient_rsp]: |
258 "(LIST_REL R) [] []" |
260 "(LIST_REL R) [] []" |
259 by simp |
261 by simp |
260 |
|
261 thm LAMBDA_PRS[no_vars] |
|
262 thm all_prs[no_vars] |
|
263 |
|
264 lemma test_all_prs: |
|
265 "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g" |
|
266 apply(drule all_prs) |
|
267 apply(simp) |
|
268 done |
|
269 |
|
270 lemma test: |
|
271 "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; |
|
272 (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f" |
|
273 apply - |
|
274 thm LAMBDA_PRS |
|
275 apply(drule LAMBDA_PRS) |
|
276 apply(assumption) |
|
277 apply(auto) |
|
278 done |
|
279 |
|
280 |
262 |
281 lemma "foldl PLUS x [] = x" |
263 lemma "foldl PLUS x [] = x" |
282 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
264 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
283 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
265 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
284 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
266 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
285 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
267 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
286 apply(simp only: nil_prs) |
268 apply(simp only: nil_prs) |
287 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
269 apply(tactic {* clean_tac @{context} 1 *}) |
288 done |
270 done |
289 |
271 |
290 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
272 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
291 sorry |
273 sorry |
292 |
274 |
294 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
276 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
295 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
277 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
296 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
278 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
297 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
279 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
298 apply(simp only: cons_prs[OF QUOTIENT_my_int]) |
280 apply(simp only: cons_prs[OF QUOTIENT_my_int]) |
299 apply(tactic {* clean_tac @{context} [quot] 1 *}) |
281 apply(tactic {* clean_tac @{context} 1 *}) |
300 done |
282 done |
301 |
283 |