322 ML {* lift_thm_fset @{context} @{thm m1} *} |
322 ML {* lift_thm_fset @{context} @{thm m1} *} |
323 ML {* lift_thm_fset @{context} @{thm m2} *} |
323 ML {* lift_thm_fset @{context} @{thm m2} *} |
324 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
324 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
325 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
325 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
326 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
326 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
327 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*) |
327 ML {* lift_thm_fset @{context} @{thm map_append} *} |
328 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
328 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
329 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
329 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
330 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
330 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
331 |
331 |
332 term list_rec |
332 term list_rec |
333 |
333 |
334 quotient_def |
334 quotient_def |
335 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
335 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
336 where |
336 where |
337 "fset_rec \<equiv> list_rec" |
337 "fset_rec \<equiv> list_rec" |
|
338 |
|
339 (* ML {* Toplevel.program (fn () => lift_thm_fset @{context} @{thm list.recs(2)}) *} *) |
338 |
340 |
339 thm list.recs(2) |
341 thm list.recs(2) |
340 thm list.cases |
342 thm list.cases |
341 |
343 |
342 |
344 |
348 ML {* val defs_sym = add_lower_defs @{context} defs *} |
350 ML {* val defs_sym = add_lower_defs @{context} defs *} |
349 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
351 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
350 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
352 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
351 |
353 |
352 |
354 |
353 ML {* val t_a = atomize_thm @{thm map_append} *} |
355 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 |
354 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
371 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
355 ML_prf {* fun tac ctxt = FIRST' [ |
372 ML_prf {* fun tac ctxt = FIRST' [ |
356 rtac rel_refl, |
373 rtac rel_refl, |
357 atac, |
374 atac, |
358 rtac @{thm universal_twice}, |
375 rtac @{thm universal_twice}, |
367 ]; *} |
384 ]; *} |
368 apply (atomize(full)) |
385 apply (atomize(full)) |
369 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
386 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
370 done*) |
387 done*) |
371 |
388 |
372 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
389 ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *} |
373 ML {* |
390 ML {* |
374 val rt = build_repabs_term @{context} t_r consts rty qty |
391 val rt = build_repabs_term @{context} t_r consts rty qty |
375 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
392 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
376 *} |
393 *} |
377 |
394 |
380 |
397 |
381 prove rg |
398 prove rg |
382 apply(atomize(full)) |
399 apply(atomize(full)) |
383 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
400 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
384 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
401 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 |
385 done |
407 done |
386 ML {* val t_t = |
408 ML {* val t_t = |
387 Toplevel.program (fn () => |
409 Toplevel.program (fn () => |
388 repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
410 repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
389 ) |
411 ) |
391 |
413 |
392 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
414 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
393 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
415 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
394 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
416 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
395 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
417 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
396 ML {* val app_prs_thms = map Thm.freezeT app_prs_thms *} |
418 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} |
397 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *} |
419 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *} |
398 ML {* val (alls, exs) = findallex rty qty (prop_of t_a); *} |
420 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
399 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
421 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
400 ML {* val allthmsv = map Thm.varifyT allthms *} |
422 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *} |
401 ML {* val t_a = MetaSimplifier.rewrite_rule (allthmsv) t_l *} |
|
402 ML {* val defs_sym = add_lower_defs @{context} defs *} |
423 ML {* val defs_sym = add_lower_defs @{context} defs *} |
403 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} |
424 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} |
404 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
425 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
405 ML {* ObjectLogic.rulify t_s *} |
426 ML {* ObjectLogic.rulify t_s *} |
406 |
427 |