347 |
347 |
348 |
348 |
349 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *} |
349 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *} |
350 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} |
350 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} |
351 |
351 |
352 |
352 lemma list_induct_part: |
353 |
353 assumes a: "P (x :: 'a list) ([] :: 'a list)" |
354 |
354 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
355 |
355 shows "P x l" |
|
356 apply (rule_tac P="P x" in list.induct) |
|
357 apply (rule a) |
|
358 apply (rule b) |
|
359 apply (assumption) |
|
360 done |
356 |
361 |
357 |
362 |
358 (* Construction site starts here *) |
363 (* Construction site starts here *) |
359 |
364 |
360 |
365 |
361 ML {* val consts = lookup_quot_consts defs *} |
366 ML {* val consts = lookup_quot_consts defs *} |
362 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
|
363 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
367 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
364 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
368 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
365 |
369 |
366 thm list.recs(2) |
370 thm list.recs(2) |
367 ML {* val t_a = atomize_thm @{thm list.recs(2)} *} |
371 ML {* val t_a = atomize_thm @{thm list_induct_part} *} |
368 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
372 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
369 ML_prf {* fun tac ctxt = FIRST' [ |
373 ML_prf {* fun tac ctxt = FIRST' [ |
370 rtac rel_refl, |
374 rtac rel_refl, |
371 atac, |
375 atac, |
372 rtac @{thm universal_twice}, |
376 rtac @{thm universal_twice}, |
405 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
409 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
406 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} |
410 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} |
407 ML {* t_t *} |
411 ML {* t_t *} |
408 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
412 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
409 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
413 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
410 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
414 ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_t *} |
411 ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_a *} |
415 ML app_prs_thms |
412 ML {* val iitt = Drule.eta_contraction_rule (hd (tl lam_prs_thms)) *} |
|
413 ML {* val iitt = (hd (lam_prs_thms)) *} |
|
414 |
|
415 ML {* val t_l0 = repeat_eqsubst_thm @{context} [iitt] t_a *} |
|
416 ML {* val t_l0 = repeat_eqsubst_thm @{context} ([hd (tl lam_prs_thms)]) t_a *} |
|
417 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *} |
416 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *} |
|
417 ML lam_prs_thms |
|
418 ML {* val t_id = simp_ids @{context} t_l *} |
|
419 thm INSERT_def |
418 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
420 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
419 ML t_l0 |
|
420 ML {* val t_id = simp_ids @{context} t_l0 *} |
|
421 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} |
421 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} |
422 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_d *} |
422 ML allthms |
423 |
423 thm FORALL_PRS |
424 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
424 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_d *} |
|
425 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_a *} |
425 ML {* ObjectLogic.rulify t_s *} |
426 ML {* ObjectLogic.rulify t_s *} |
|
427 |
|
428 ML {* Type.freeze *} |
|
429 |
|
430 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *} |
|
431 ML {* val vars = map Free (Term.add_frees gl []) *} |
|
432 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *} |
|
433 ML {* val gla = fold lambda_all vars gl *} |
|
434 ML {* val glf = Type.freeze gla *} |
|
435 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *} |
|
436 ML {* val allsym = map symmetric allthms *} |
|
437 ML {* val t_a = (snd o Thm.dest_equals o cprop_of) (MetaSimplifier.rewrite true allsym glac) *} |
426 |
438 |
427 ML {* |
439 ML {* |
428 fun lift_thm_fset_note name thm lthy = |
440 fun lift_thm_fset_note name thm lthy = |
429 let |
441 let |
430 val lifted_thm = lift_thm_fset lthy thm; |
442 val lifted_thm = lift_thm_fset lthy thm; |