equal
deleted
inserted
replaced
569 else [] |
569 else [] |
570 |
570 |
571 (* postprocessing of eq and fv theorems *) |
571 (* postprocessing of eq and fv theorems *) |
572 |
572 |
573 val qeq_iffs' = qeq_iffs |
573 val qeq_iffs' = qeq_iffs |
574 |> map (simplify (HOL_basic_ss addsimps |
574 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
575 (@{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]} @ qfv_supp_thms))) |
575 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
576 |
576 |
577 val qsupp_constrs = qfv_defs |
577 val qsupp_constrs = qfv_defs |
578 |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms))) |
578 |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms))) |
|
579 |
|
580 val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp} |
|
581 val transform_thms = |
|
582 [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, |
|
583 @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, |
|
584 @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp}, |
|
585 @{thm fresh_def[symmetric]}] |
|
586 |
|
587 val qfresh_constrs = qsupp_constrs |
|
588 |> map (fn thm => thm RS transform_thm) |
|
589 |> map (simplify (HOL_basic_ss addsimps transform_thms)) |
|
590 |
579 |
591 |
580 (* noting the theorems *) |
592 (* noting the theorems *) |
581 |
593 |
582 (* generating the prefix for the theorem names *) |
594 (* generating the prefix for the theorem names *) |
583 val thms_name = |
595 val thms_name = |
597 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
609 ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) |
598 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
610 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
599 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
611 ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) |
600 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
612 ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) |
601 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
613 ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) |
|
614 ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs) |
602 in |
615 in |
603 (0, lthy9') |
616 (0, lthy9') |
604 end handle TEST ctxt => (0, ctxt) |
617 end handle TEST ctxt => (0, ctxt) |
605 *} |
618 *} |
606 |
619 |