270 using a |
268 using a |
271 apply (induct) |
269 apply (induct) |
272 apply(auto intro: list_eq.intros) |
270 apply(auto intro: list_eq.intros) |
273 done |
271 done |
274 |
272 |
275 lemma fun_rel_id: |
|
276 "(op = ===> op =) \<equiv> op =" |
|
277 apply (rule eq_reflection) |
|
278 apply (rule ext) |
|
279 apply (rule ext) |
|
280 apply (simp) |
|
281 apply (auto) |
|
282 apply (rule ext) |
|
283 apply (simp) |
|
284 done |
|
285 |
|
286 lemma ho_map_rsp: |
273 lemma ho_map_rsp: |
287 "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map" |
274 "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map" |
288 by (simp add: fun_rel_id map_rsp) |
275 by (simp add: FUN_REL_EQ map_rsp) |
289 |
276 |
290 lemma map_append : |
277 lemma map_append : |
291 "(map f (a @ b)) \<approx> |
278 "(map f (a @ b)) \<approx> |
292 (map f a) @ (map f b)" |
279 (map f a) @ (map f b)" |
293 by simp (rule list_eq_refl) |
280 by simp (rule list_eq_refl) |
294 |
281 |
295 lemma op_eq_twice: "(op = ===> op =) = (op =)" |
|
296 apply (rule ext) |
|
297 apply (rule ext) |
|
298 apply (simp add: FUN_REL.simps) |
|
299 apply auto |
|
300 apply (rule ext) |
|
301 apply simp |
|
302 done |
|
303 |
|
304 |
|
305 |
|
306 lemma ho_fold_rsp: |
282 lemma ho_fold_rsp: |
307 "((op = ===> op = ===> op =) ===> (op = ===> op =) ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
283 "((op = ===> op = ===> op =) ===> (op = ===> op =) ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
308 apply (auto simp add: op_eq_twice) |
284 apply (auto simp add: FUN_REL_EQ) |
309 sorry |
285 sorry |
310 |
286 |
311 print_quotients |
287 print_quotients |
312 |
288 |
313 |
289 |
327 ML {* lift_thm_fset @{context} @{thm map_append} *} |
303 ML {* lift_thm_fset @{context} @{thm map_append} *} |
328 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
304 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
329 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
305 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
330 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
306 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
331 |
307 |
332 term list_rec |
|
333 |
|
334 quotient_def |
308 quotient_def |
335 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
309 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
336 where |
310 where |
337 "fset_rec \<equiv> list_rec" |
311 "fset_rec \<equiv> list_rec" |
338 |
312 |
339 (* ML {* Toplevel.program (fn () => lift_thm_fset @{context} @{thm list.recs(2)}) *} *) |
313 quotient_def |
340 |
314 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
341 thm list.recs(2) |
315 where |
342 thm list.cases |
316 "fset_case \<equiv> list_case" |
343 |
317 |
344 |
318 lemma list_rec_rsp: |
345 |
319 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
346 |
320 apply (auto simp add: FUN_REL_EQ) |
|
321 sorry |
|
322 |
|
323 lemma list_case_rsp: |
|
324 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
|
325 apply (auto simp add: FUN_REL_EQ) |
|
326 sorry |
|
327 |
|
328 |
|
329 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
|
330 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
|
331 |
|
332 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
|
333 |
|
334 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *} |
|
335 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} |
|
336 |
|
337 |
|
338 |
|
339 |
|
340 |
|
341 |
|
342 |
|
343 (* Construction site starts here *) |
347 |
344 |
348 |
345 |
349 ML {* val consts = lookup_quot_consts defs *} |
346 ML {* val consts = lookup_quot_consts defs *} |
350 ML {* val defs_sym = add_lower_defs @{context} defs *} |
347 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
351 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
348 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
352 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
349 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
353 |
350 |
354 |
351 |
355 ML {* val t_a = atomize_thm @{thm list.recs(2)} *} |
352 ML {* val t_a = atomize_thm @{thm list.recs(2)} *} |
356 ML {* val p_a = cprop_of t_a *} |
|
357 ML {* val pp = (snd o Thm.dest_abs NONE o snd o Thm.dest_comb o snd o Thm.dest_comb) p_a *} |
|
358 ML {* needs_lift @{typ "'a list"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} *} |
|
359 ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} |
|
360 |
|
361 |
|
362 ML {* val tt = (my_reg @{context} (@{term list_eq}) ( @{typ "'a list"}) (term_of pp)) *} |
|
363 ML {* val (_, [R, _]) = strip_comb tt *} |
|
364 ML {* val (_, [R]) = strip_comb R *} |
|
365 ML {* val (f, [R1, R2]) = strip_comb R *} |
|
366 ML {* val (f, [R1, R2]) = strip_comb R2 *} |
|
367 ML {* val (f, [R1, R2]) = strip_comb R2 *} |
|
368 |
|
369 ML {* cterm_of @{theory} R2 *} |
|
370 |
|
371 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
353 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
372 ML_prf {* fun tac ctxt = FIRST' [ |
354 ML_prf {* fun tac ctxt = FIRST' [ |
373 rtac rel_refl, |
355 rtac rel_refl, |
374 atac, |
356 atac, |
375 rtac @{thm universal_twice}, |
357 rtac @{thm universal_twice}, |
383 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
365 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
384 ]; *} |
366 ]; *} |
385 apply (atomize(full)) |
367 apply (atomize(full)) |
386 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
368 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
387 done*) |
369 done*) |
388 |
|
389 ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *} |
370 ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *} |
390 ML {* |
371 ML {* |
391 val rt = build_repabs_term @{context} t_r consts rty qty |
372 val rt = build_repabs_term @{context} t_r consts rty qty |
392 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
373 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
393 *} |
374 *} |
397 |
378 |
398 prove rg |
379 prove rg |
399 apply(atomize(full)) |
380 apply(atomize(full)) |
400 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
381 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
401 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
382 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
402 |
|
403 "(op = ===> (op = ===> op \<approx> ===> op = ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
|
404 "QUOTIENT op = (id ---> id) (id ---> id)" |
|
405 "(op = ===> op \<approx> ===> op =) x y" |
|
406 |
383 |
407 done |
384 done |
408 ML {* val t_t = |
385 ML {* val t_t = |
409 Toplevel.program (fn () => |
386 Toplevel.program (fn () => |
410 repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
387 repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
411 ) |
388 ) |
412 *} |
389 *} |
413 |
390 |
414 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
391 ML {* val abs = findabs rty (prop_of (t_a)) *} |
415 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
392 ML {* val aps = findaps rty (prop_of (t_a)) *} |
416 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
393 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
417 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
394 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
418 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} |
395 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} |
419 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *} |
396 ML {* t_t *} |
|
397 ML {* val t_l0 = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *} |
|
398 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms) t_l0 *} |
420 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
399 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
421 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
400 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
422 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *} |
401 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *} |
423 ML {* val defs_sym = add_lower_defs @{context} defs *} |
402 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
424 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} |
403 ML {* val t_id = simp_ids @{context} t_a *} |
|
404 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} |
425 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
405 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
426 ML {* ObjectLogic.rulify t_s *} |
406 ML {* ObjectLogic.rulify t_s *} |
427 |
407 |
428 ML {* |
408 ML {* |
429 fun lift_thm_fset_note name thm lthy = |
409 fun lift_thm_fset_note name thm lthy = |