324 quotient_def |
324 quotient_def |
325 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
325 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
326 where |
326 where |
327 "fset_case \<equiv> list_case" |
327 "fset_case \<equiv> list_case" |
328 |
328 |
|
329 (* Probably not true without additional assumptions about the function *) |
329 lemma list_rec_rsp: |
330 lemma list_rec_rsp: |
330 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
331 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
331 apply (auto simp add: FUN_REL_EQ) |
332 apply (auto simp add: FUN_REL_EQ) |
|
333 apply (erule_tac list_eq.induct) |
|
334 apply (simp_all) |
332 sorry |
335 sorry |
333 |
336 |
334 lemma list_case_rsp: |
337 lemma list_case_rsp: |
335 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
338 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
336 apply (auto simp add: FUN_REL_EQ) |
339 apply (auto simp add: FUN_REL_EQ) |
357 ML {* val consts = lookup_quot_consts defs *} |
360 ML {* val consts = lookup_quot_consts defs *} |
358 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
361 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
359 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
362 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
360 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
363 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
361 |
364 |
362 |
365 thm list.recs(2) |
363 ML {* val t_a = atomize_thm @{thm list.recs(2)} *} |
366 ML {* val t_a = atomize_thm @{thm list.recs(2)} *} |
364 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
367 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
365 ML_prf {* fun tac ctxt = FIRST' [ |
368 ML_prf {* fun tac ctxt = FIRST' [ |
366 rtac rel_refl, |
369 rtac rel_refl, |
367 atac, |
370 atac, |
403 ML {* val aps = findaps rty (prop_of (t_a)) *} |
406 ML {* val aps = findaps rty (prop_of (t_a)) *} |
404 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
407 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
405 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
408 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 *} |
409 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *} |
407 ML {* t_t *} |
410 ML {* t_t *} |
408 ML {* val t_l0 = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *} |
|
409 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms) t_l0 *} |
|
410 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
411 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *} |
411 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
412 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
412 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *} |
413 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
|
414 ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_a *} |
|
415 ML {* val iitt = Drule.eta_contraction_rule (hd (tl lam_prs_thms)) *} |
|
416 ML {* val iitt = (hd (lam_prs_thms)) *} |
|
417 |
|
418 ML {* val t_l0 = repeat_eqsubst_thm @{context} [iitt] t_a *} |
|
419 ML {* val t_l0 = repeat_eqsubst_thm @{context} ([hd (tl lam_prs_thms)]) t_a *} |
|
420 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *} |
413 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
421 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
414 ML {* val t_id = simp_ids @{context} t_a *} |
422 ML t_l0 |
|
423 ML {* val t_id = simp_ids @{context} t_l0 *} |
415 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} |
424 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *} |
|
425 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_d *} |
|
426 |
416 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
427 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
417 ML {* ObjectLogic.rulify t_s *} |
428 ML {* ObjectLogic.rulify t_s *} |
418 |
429 |
419 ML {* |
430 ML {* |
420 fun lift_thm_fset_note name thm lthy = |
431 fun lift_thm_fset_note name thm lthy = |