634 assumes a: "list_eq x y" |
624 assumes a: "list_eq x y" |
635 shows "(z memb x) = (z memb y)" |
625 shows "(z memb x) = (z memb y)" |
636 using a by induct auto |
626 using a by induct auto |
637 |
627 |
638 |
628 |
|
629 fun |
|
630 card1 :: "'a list \<Rightarrow> nat" |
|
631 where |
|
632 card1_nil: "(card1 []) = 0" |
|
633 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
|
634 |
|
635 local_setup {* |
|
636 make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
637 *} |
|
638 |
|
639 term card1 |
|
640 term card |
|
641 thm card_def |
|
642 |
|
643 (* text {* |
|
644 Maybe make_const_def should require a theorem that says that the particular lifted function |
|
645 respects the relation. With it such a definition would be impossible: |
|
646 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
647 *} *) |
|
648 |
|
649 lemma card1_rsp: |
|
650 fixes a b :: "'a list" |
|
651 assumes e: "a \<approx> b" |
|
652 shows "card1 a = card1 b" |
|
653 using e apply induct |
|
654 apply (simp_all add:mem_respects) |
|
655 done |
|
656 |
|
657 lemma card1_0: |
|
658 fixes a :: "'a list" |
|
659 shows "(card1 a = 0) = (a = [])" |
|
660 apply (induct a) |
|
661 apply (simp) |
|
662 apply (simp_all) |
|
663 apply meson |
|
664 apply (simp_all) |
|
665 done |
|
666 |
|
667 lemma not_mem_card1: |
|
668 fixes x :: "'a" |
|
669 fixes xs :: "'a list" |
|
670 shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)" |
|
671 by simp |
|
672 |
|
673 |
|
674 lemma mem_cons: |
|
675 fixes x :: "'a" |
|
676 fixes xs :: "'a list" |
|
677 assumes a : "x memb xs" |
|
678 shows "x # xs \<approx> xs" |
|
679 using a apply (induct xs) |
|
680 apply (simp_all) |
|
681 apply (meson) |
|
682 apply (simp_all add: list_eq.intros(4)) |
|
683 proof - |
|
684 fix a :: "'a" |
|
685 fix xs :: "'a list" |
|
686 assume a1 : "x # xs \<approx> xs" |
|
687 assume a2 : "x memb xs" |
|
688 have a3 : "x # a # xs \<approx> a # x # xs" using list_eq.intros(1)[of "x"] by blast |
|
689 have a4 : "a # x # xs \<approx> a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp |
|
690 then show "x # a # xs \<approx> a # xs" using a3 list_eq.intros(6) by blast |
|
691 qed |
|
692 |
|
693 lemma card1_suc: |
|
694 fixes xs :: "'a list" |
|
695 fixes n :: "nat" |
|
696 assumes c: "card1 xs = Suc n" |
|
697 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)" |
|
698 using c apply (induct xs) |
|
699 apply (simp) |
|
700 (* apply (rule allI)*) |
|
701 proof - |
|
702 fix a :: "'a" |
|
703 fix xs :: "'a list" |
|
704 fix n :: "nat" |
|
705 assume a1: "card1 xs = Suc n \<Longrightarrow> \<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys" |
|
706 assume a2: "card1 (a # xs) = Suc n" |
|
707 from a1 a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" |
|
708 apply - |
|
709 apply (rule True_or_False [of "a memb xs", THEN disjE]) |
|
710 apply (simp_all add: card1_cons if_True simp_thms) |
|
711 proof - |
|
712 assume a1: "\<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys" |
|
713 assume a2: "card1 xs = Suc n" |
|
714 assume a3: "a memb xs" |
|
715 from a1 obtain b ys where a5: "\<not> b memb ys \<and> xs \<approx> b # ys" by blast |
|
716 from a2 a3 a5 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" |
|
717 apply - |
|
718 apply (rule_tac x = "b" in exI) |
|
719 apply (rule_tac x = "ys" in exI) |
|
720 apply (simp_all) |
|
721 proof - |
|
722 assume a1: "a memb xs" |
|
723 assume a2: "\<not> b memb ys \<and> xs \<approx> b # ys" |
|
724 then have a3: "xs \<approx> b # ys" by simp |
|
725 have "a # xs \<approx> xs" using a1 mem_cons[of "a" "xs"] by simp |
|
726 then show "a # xs \<approx> b # ys" using a3 list_eq.intros(6) by blast |
|
727 qed |
|
728 next |
|
729 assume a2: "\<not> a memb xs" |
|
730 from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" |
|
731 apply - |
|
732 apply (rule_tac x = "a" in exI) |
|
733 apply (rule_tac x = "xs" in exI) |
|
734 apply (simp) |
|
735 apply (rule list_eq_sym) |
|
736 done |
|
737 qed |
|
738 qed |
|
739 |
639 lemma cons_preserves: |
740 lemma cons_preserves: |
640 fixes z |
741 fixes z |
641 assumes a: "xs \<approx> ys" |
742 assumes a: "xs \<approx> ys" |
642 shows "(z # xs) \<approx> (z # ys)" |
743 shows "(z # xs) \<approx> (z # ys)" |
643 using a by (rule QuotMain.list_eq.intros(5)) |
744 using a by (rule QuotMain.list_eq.intros(5)) |
644 |
745 |
645 (* cu: what does unlam do? *) |
746 |
646 ML {* |
747 text {* |
647 fun unlam_def orig_ctxt ctxt t = |
748 unlam_def converts a definition theorem given as 'a = \lambda x. \lambda y. f (x y)' |
|
749 to a theorem 'a x y = f (x, y)'. These are needed to rewrite right-to-left. |
|
750 *} |
|
751 |
|
752 ML {* |
|
753 fun unlam_def_aux orig_ctxt ctxt t = |
648 let val rhs = Thm.rhs_of t in |
754 let val rhs = Thm.rhs_of t in |
649 (case try (Thm.dest_abs NONE) rhs of |
755 (case try (Thm.dest_abs NONE) rhs of |
650 SOME (v, vt) => |
756 SOME (v, vt) => |
651 let |
757 let |
652 val (vname, vt) = Term.dest_Free (Thm.term_of v) |
758 val (vname, vt) = Term.dest_Free (Thm.term_of v) |
653 val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt |
759 val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt |
654 val nv = Free(vnname, vt) |
760 val nv = Free(vnname, vt) |
655 val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv) |
761 val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv) |
656 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
762 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
657 in unlam_def orig_ctxt ctxt tnorm end |
763 in unlam_def_aux orig_ctxt ctxt tnorm end |
658 | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) |
764 | NONE => singleton (ProofContext.export ctxt orig_ctxt) t) |
659 end |
765 end; |
|
766 |
|
767 fun unlam_def ctxt t = unlam_def_aux ctxt ctxt t |
660 *} |
768 *} |
661 |
769 |
662 local_setup {* |
770 local_setup {* |
663 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
771 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
664 *} |
772 *} |
665 |
773 |
666 term membship |
774 term membship |
667 term IN |
775 term IN |
668 thm IN_def |
776 thm IN_def |
669 ML {* unlam_def @{context} @{context} @{thm IN_def} *} |
777 ML {* unlam_def @{context} @{thm IN_def} *} |
670 |
778 |
671 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
779 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
672 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
780 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
673 |
781 |
674 lemma yy: |
782 lemma yy: |
771 (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) |
879 (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) |
772 else list_comb ((build_aux f), (map build_aux args))) |
880 else list_comb ((build_aux f), (map build_aux args))) |
773 end |
881 end |
774 | build_aux x = |
882 | build_aux x = |
775 if is_const x then maybe_mk_rep_abs x else x |
883 if is_const x then maybe_mk_rep_abs x else x |
776 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
884 val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm); |
|
885 val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm); |
|
886 val concl2 = Logic.list_implies (prems, concl) |
|
887 (* val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*) |
777 in |
888 in |
778 HOLogic.mk_eq ((build_aux concl), concl) |
889 HOLogic.mk_eq ((build_aux concl2), concl2) |
779 end *} |
890 end *} |
780 |
891 |
781 ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *} |
892 ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *} |
782 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *} |
893 ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *} |
783 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
894 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
784 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
895 ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *} |
785 ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *} |
896 ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *} |
786 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def CARD_def INSERT_def} *} |
897 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
787 ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *} |
898 ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *} |
788 |
899 |
789 ML {* |
900 ML {* |
790 fun dest_cbinop t = |
901 fun dest_cbinop t = |
791 let |
902 let |
861 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
972 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
862 val cgoal = cterm_of @{theory} goal |
973 val cgoal = cterm_of @{theory} goal |
863 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
974 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
864 *} |
975 *} |
865 |
976 |
|
977 notation ( output) "prop" ("#_" [1000] 1000) |
|
978 |
866 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
979 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
867 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
980 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
981 apply (tactic {* print_tac "" *}) |
|
982 thm arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="] |
|
983 (* apply (rule arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="])*) |
|
984 apply (subst arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="]) |
868 apply (tactic {* foo_tac' @{context} 1 *}) |
985 apply (tactic {* foo_tac' @{context} 1 *}) |
869 done |
986 apply (tactic {* foo_tac' @{context} 1 *}) |
870 |
987 thm arg_cong2 [of "x memb []" "x memb []" False False "op ="] |
|
988 (*apply (rule arg_cong2 [of "x memb []" "x memb []" False False "op ="]) |
|
989 done *) |
|
990 sorry |
871 |
991 |
872 thm length_append (* Not true but worth checking that the goal is correct *) |
992 thm length_append (* Not true but worth checking that the goal is correct *) |
873 ML {* |
993 ML {* |
874 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
994 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
875 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
995 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
876 val cgoal = cterm_of @{theory} goal |
996 val cgoal = cterm_of @{theory} goal |
877 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
997 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
878 *} |
998 *} |
879 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
999 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
880 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1000 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
881 apply (tactic {* foo_tac' @{context} 1 *}) |
1001 (* apply (tactic {* foo_tac' @{context} 1 *})*) |
882 sorry |
1002 sorry |
883 |
1003 |
884 thm m2 |
1004 thm m2 |
885 ML {* |
1005 ML {* |
886 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
1006 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
901 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1021 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
902 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1022 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
903 *} |
1023 *} |
904 |
1024 |
905 (* It is the same, but we need a name for it. *) |
1025 (* It is the same, but we need a name for it. *) |
906 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry |
1026 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
|
1027 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1028 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1029 sorry |
907 lemma zzz : |
1030 lemma zzz : |
908 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
1031 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
909 = (a # a # xs \<approx> a # xs)" |
1032 = (a # a # xs \<approx> a # xs)" |
910 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1033 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
911 apply (tactic {* foo_tac' @{context} 1 *}) |
1034 apply (tactic {* foo_tac' @{context} 1 *}) |
929 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
1052 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
930 ) |
1053 ) |
931 ) |
1054 ) |
932 *} |
1055 *} |
933 |
1056 |
|
1057 thm sym |
|
1058 ML {* |
|
1059 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm sym})) |
|
1060 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
1061 *} |
|
1062 ML {* |
|
1063 val cgoal = |
|
1064 Toplevel.program (fn () => |
|
1065 cterm_of @{theory} goal |
|
1066 ) |
|
1067 *} |
|
1068 |
|
1069 |
934 thm list_eq.intros(5) |
1070 thm list_eq.intros(5) |
935 ML {* |
1071 ML {* |
936 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
1072 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
937 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1073 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
938 val cgoal = cterm_of @{theory} goal |
1074 *} |
|
1075 ML {* |
|
1076 val cgoal = |
|
1077 Toplevel.program (fn () => |
|
1078 cterm_of @{theory} goal |
|
1079 ) |
|
1080 *} |
|
1081 ML {* |
939 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1082 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
940 *} |
1083 *} |
941 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
1084 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
942 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1085 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
943 apply (tactic {* foo_tac' @{context} 1 *}) |
1086 apply (tactic {* foo_tac' @{context} 1 *}) |
944 done |
1087 done |
|
1088 |
|
1089 |
|
1090 thm list.induct |
|
1091 ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *} |
|
1092 |
|
1093 ML {* |
|
1094 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct})) |
|
1095 *} |
|
1096 ML {* |
|
1097 val goal = |
|
1098 Toplevel.program (fn () => |
|
1099 build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
1100 ) |
|
1101 *} |
|
1102 ML {* |
|
1103 val cgoal = cterm_of @{theory} goal |
|
1104 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
1105 *} |
|
1106 |
|
1107 |
|
1108 thm card1_suc |
|
1109 |
|
1110 ML {* |
|
1111 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc})) |
|
1112 *} |
|
1113 ML {* |
|
1114 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
1115 *} |
|
1116 ML {* |
|
1117 val cgoal = cterm_of @{theory} goal |
|
1118 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
1119 *} |
|
1120 |
|
1121 |
945 |
1122 |
946 (* |
1123 (* |
947 datatype obj1 = |
1124 datatype obj1 = |
948 OVAR1 "string" |
1125 OVAR1 "string" |
949 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
1126 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |