541 term CARD |
541 term CARD |
542 thm CARD_def |
542 thm CARD_def |
543 |
543 |
544 thm QUOTIENT_fset |
544 thm QUOTIENT_fset |
545 |
545 |
|
546 (* This code builds the interpretation from ML level, currently only |
|
547 for fset *) |
|
548 |
|
549 ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN |
|
550 simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def[symmetric]}) 1 THEN |
|
551 simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def[symmetric]}) 1) *} |
|
552 ML {* val mthdt = Method.Basic (fn _ => mthd) *} |
|
553 ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *} |
|
554 ML {* val exp_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true), |
|
555 Expression.Named [ |
|
556 ("R",@{term list_eq}), |
|
557 ("Abs",@{term Abs_fset}), |
|
558 ("Rep",@{term Rep_fset}) |
|
559 ]))] *} |
|
560 ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *} |
|
561 ML {* val eqn1i = (bindd, @{prop "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"}) *} |
|
562 ML {* val eqn2i = (bindd, @{prop "QUOT_TYPE.REP Rep_fset = REP_fset"}) *} |
|
563 setup {* fn thy => ProofContext.theory_of |
|
564 (bymt (Expression.interpretation (exp_i, []) [eqn2i,eqn1i] thy)) *} |
|
565 |
|
566 (* It is eqivalent to the below: |
|
567 |
|
568 interpretation QUOT_TYPE_fset_i: QUOT_TYPE list_eq Abs_fset Rep_fset |
|
569 where "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset" |
|
570 and "QUOT_TYPE.REP Rep_fset = REP_fset" |
|
571 unfolding ABS_fset_def REP_fset_def |
|
572 apply (rule QUOT_TYPE_fset) |
|
573 apply (simp only: ABS_fset_def[symmetric]) |
|
574 apply (simp only: REP_fset_def[symmetric]) |
|
575 done |
|
576 *) |
|
577 |
|
578 |
|
579 |
546 fun |
580 fun |
547 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _") |
581 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _") |
548 where |
582 where |
549 m1: "(x memb []) = False" |
583 m1: "(x memb []) = False" |
550 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))" |
584 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))" |
551 |
585 |
552 lemma mem_respects: |
586 lemma mem_respects: |
553 fixes z::"nat" |
587 fixes z |
554 assumes a: "list_eq x y" |
588 assumes a: "list_eq x y" |
555 shows "z memb x = z memb y" |
589 shows "(z memb x) = (z memb y)" |
556 using a |
590 using a |
557 apply(induct) |
591 apply(induct) |
558 apply(auto) |
592 apply(auto) |
559 done |
593 done |
560 |
594 |
561 |
595 |
562 local_setup {* |
596 definition "IN x xa \<equiv> x memb REP_fset xa" |
|
597 |
|
598 (*local_setup {* |
563 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
599 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
564 *} |
600 *}*) |
565 |
601 |
566 term membship |
602 term membship |
567 term IN |
603 term IN |
568 thm IN_def |
604 thm IN_def |
569 |
605 |
573 lemma yy: |
609 lemma yy: |
574 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
610 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
575 unfolding IN_def EMPTY_def |
611 unfolding IN_def EMPTY_def |
576 apply(rule_tac f="(op =) False" in arg_cong) |
612 apply(rule_tac f="(op =) False" in arg_cong) |
577 apply(rule mem_respects) |
613 apply(rule mem_respects) |
578 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
614 apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
579 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
|
580 apply(rule list_eq.intros) |
615 apply(rule list_eq.intros) |
581 done |
616 done |
582 |
617 |
583 lemma |
618 lemma |
584 shows "IN (x::nat) EMPTY = False" |
619 shows "IN (x::nat) EMPTY = False" |
607 using a |
642 using a |
608 apply(induct) |
643 apply(induct) |
609 apply(auto intro: list_eq.intros) |
644 apply(auto intro: list_eq.intros) |
610 apply(simp add: list_eq_sym) |
645 apply(simp add: list_eq_sym) |
611 done |
646 done |
612 |
|
613 (* This code builds the interpretation from ML level, currently only |
|
614 for fset *) |
|
615 |
|
616 ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN |
|
617 simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def[symmetric]}) 1 THEN |
|
618 simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def[symmetric]}) 1) *} |
|
619 ML {* val mthdt = Method.Basic (fn _ => mthd) *} |
|
620 ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *} |
|
621 ML {* val exp = [("QUOT_TYPE",(("QUOT_TYPE_fset_i", true), |
|
622 Expression.Named [ |
|
623 ("R","list_eq"), |
|
624 ("Abs","Abs_fset"), |
|
625 ("Rep","Rep_fset") |
|
626 ]))] *} |
|
627 ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *} |
|
628 ML {* val eqn1 = (bindd, "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset") *} |
|
629 ML {* val eqn2 = (bindd, "QUOT_TYPE.REP Rep_fset = REP_fset") *} |
|
630 setup {* fn thy => ProofContext.theory_of |
|
631 (bymt (Expression.interpretation_cmd (exp, []) [eqn2,eqn1] thy)) *} |
|
632 |
|
633 (* It is eqivalent to the below: |
|
634 |
|
635 interpretation QUOT_TYPE_fset_i: QUOT_TYPE list_eq Abs_fset Rep_fset |
|
636 where "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset" |
|
637 and "QUOT_TYPE.REP Rep_fset = REP_fset" |
|
638 unfolding ABS_fset_def REP_fset_def |
|
639 apply (rule QUOT_TYPE_fset) |
|
640 apply (simp only: ABS_fset_def[symmetric]) |
|
641 apply (simp only: REP_fset_def[symmetric]) |
|
642 done |
|
643 *) |
|
644 |
647 |
645 lemma yyy : |
648 lemma yyy : |
646 shows " |
649 shows " |
647 ( |
650 ( |
648 (UNION EMPTY s = s) & |
651 (UNION EMPTY s = s) & |
692 | build_aux (f $ a) = |
695 | build_aux (f $ a) = |
693 (if is_const f then mk_rep_abs (f $ (build_aux a)) |
696 (if is_const f then mk_rep_abs (f $ (build_aux a)) |
694 else ((build_aux f) $ (build_aux a))) |
697 else ((build_aux f) $ (build_aux a))) |
695 | build_aux x = |
698 | build_aux x = |
696 if is_const x then mk_rep_abs x else x |
699 if is_const x then mk_rep_abs x else x |
697 val concl = Thm.concl_of thm |
700 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
698 in |
701 in |
699 HOLogic.mk_eq ((build_aux concl), concl) |
702 HOLogic.mk_eq ((build_aux concl), concl) |
700 end *} |
703 end *} |
701 |
704 |
702 ML {* |
705 ML {* |
712 val goal = build_goal m1_novars consts mk_rep_abs |
715 val goal = build_goal m1_novars consts mk_rep_abs |
713 val cgoal = cterm_of @{theory} goal |
716 val cgoal = cterm_of @{theory} goal |
714 *} |
717 *} |
715 |
718 |
716 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
719 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
717 ML {* MetaSimplifier.rewrite false [emptyt] cgoal *} |
720 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
|
721 |
|
722 ML {* val in_t = (symmetric @{thm IN_def}) *} |
|
723 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *} |
|
724 |
|
725 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*) |
|
726 |
|
727 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
|
728 apply(rule_tac f="(op =)" in arg_cong2) |
|
729 unfolding IN_def EMPTY_def |
|
730 apply (rule_tac mem_respects) |
|
731 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
|
732 |
|
733 |