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