702 |
702 |
703 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
703 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
704 trm == new_trm |
704 trm == new_trm |
705 *) |
705 *) |
706 |
706 |
|
707 text {* Assumes that the given theorem is atomized *} |
707 ML {* |
708 ML {* |
708 fun build_regularize_goal thm rty rel lthy = |
709 fun build_regularize_goal thm rty rel lthy = |
709 Logic.mk_implies |
710 Logic.mk_implies |
710 ((prop_of thm), |
711 ((prop_of thm), |
711 (regularise (prop_of thm) rty rel lthy)) |
712 (regularise (prop_of thm) rty rel lthy)) |
712 *} |
713 *} |
713 |
714 |
714 section {* RepAbs injection *} |
715 section {* RepAbs injection *} |
715 |
|
716 |
716 |
717 ML {* |
717 ML {* |
718 fun build_repabs_term lthy thm constructors rty qty = |
718 fun build_repabs_term lthy thm constructors rty qty = |
719 let |
719 let |
720 fun mk_rep tm = |
720 fun mk_rep tm = |
771 in |
771 in |
772 build_aux lthy (Thm.prop_of thm) |
772 build_aux lthy (Thm.prop_of thm) |
773 end |
773 end |
774 *} |
774 *} |
775 |
775 |
|
776 text {* Assumes that it is given a regularized theorem *} |
776 ML {* |
777 ML {* |
777 fun build_repabs_goal ctxt thm cons rty qty = |
778 fun build_repabs_goal ctxt thm cons rty qty = |
778 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) |
779 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) |
779 *} |
780 *} |
780 |
781 |
781 |
782 |
782 |
|
783 |
|
784 |
|
785 section {* finite set example *} |
783 section {* finite set example *} |
786 |
784 |
787 print_syntax |
|
788 inductive |
785 inductive |
789 list_eq (infix "\<approx>" 50) |
786 list_eq (infix "\<approx>" 50) |
790 where |
787 where |
791 "a#b#xs \<approx> b#a#xs" |
788 "a#b#xs \<approx> b#a#xs" |
792 | "[] \<approx> []" |
789 | "[] \<approx> []" |
1039 apply (simp add: yyy) |
1036 apply (simp add: yyy) |
1040 apply (simp add: QUOT_TYPE_I_fset.thm10) |
1037 apply (simp add: QUOT_TYPE_I_fset.thm10) |
1041 done |
1038 done |
1042 |
1039 |
1043 ML {* |
1040 ML {* |
1044 fun mk_rep x = @{term REP_fset} $ x; |
|
1045 fun mk_abs x = @{term ABS_fset} $ x; |
|
1046 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
1041 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
1047 @{const_name "membship"}, @{const_name "card1"}, |
1042 @{const_name "membship"}, @{const_name "card1"}, |
1048 @{const_name "append"}, @{const_name "fold1"}]; |
1043 @{const_name "append"}, @{const_name "fold1"}]; |
1049 *} |
1044 *} |
1050 |
1045 |
1051 ML {* val tm = @{term "x :: 'a list"} *} |
|
1052 ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *} |
|
1053 ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *} |
|
1054 |
|
1055 ML {* val qty = @{typ "'a fset"} *} |
|
1056 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *} |
|
1057 ML {* val fall = Const(@{const_name all}, dummyT) *} |
|
1058 |
|
1059 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
1046 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
1060 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
1047 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
1061 |
|
1062 |
|
1063 |
1048 |
1064 ML {* |
1049 ML {* |
1065 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1050 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1066 *} |
1051 *} |
1067 |
1052 |