884 val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm); |
884 val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm); |
885 val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm); |
885 val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm); |
886 val concl2 = Logic.list_implies (prems, concl) |
886 val concl2 = Logic.list_implies (prems, concl) |
887 (* val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*) |
887 (* val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*) |
888 in |
888 in |
889 HOLogic.mk_eq ((build_aux concl2), concl2) |
889 Logic.mk_equals ( (build_aux concl2), concl2) |
890 end *} |
890 end *} |
891 |
891 |
892 ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *} |
892 ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *} |
893 ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *} |
893 ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *} |
894 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
894 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
963 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
963 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
964 foo_tac |
964 foo_tac |
965 ]) |
965 ]) |
966 *} |
966 *} |
967 |
967 |
968 thm m1 |
|
969 |
|
970 ML {* |
968 ML {* |
971 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
969 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
972 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
970 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
973 val cgoal = cterm_of @{theory} goal |
971 val cgoal = cterm_of @{theory} goal |
974 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
972 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
975 *} |
973 *} |
976 |
974 |
977 notation ( output) "prop" ("#_" [1000] 1000) |
975 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
978 |
976 notation ( output) "Trueprop" ("#_" [1000] 1000) |
979 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
977 |
|
978 lemma tp: |
|
979 shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)" |
|
980 by auto |
|
981 |
|
982 prove {* (Thm.term_of cgoal2) *} |
|
983 apply (rule tp) |
|
984 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
980 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
985 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 ="]) |
|
985 apply (tactic {* foo_tac' @{context} 1 *}) |
986 apply (tactic {* foo_tac' @{context} 1 *}) |
986 apply (tactic {* foo_tac' @{context} 1 *}) |
987 done |
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 |
|
991 |
988 |
992 thm length_append (* Not true but worth checking that the goal is correct *) |
989 thm length_append (* Not true but worth checking that the goal is correct *) |
993 ML {* |
990 ML {* |
994 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
991 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
995 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
992 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
996 val cgoal = cterm_of @{theory} goal |
993 val cgoal = cterm_of @{theory} goal |
997 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
994 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
998 *} |
995 *} |
999 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
996 prove {* Thm.term_of cgoal2 *} |
|
997 apply (rule tp) |
|
998 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
1000 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
999 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1001 (* apply (tactic {* foo_tac' @{context} 1 *})*) |
1000 apply (tactic {* foo_tac' @{context} 1 *}) |
1002 sorry |
1001 sorry |
1003 |
1002 |
1004 thm m2 |
1003 thm m2 |
1005 ML {* |
1004 ML {* |
1006 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
1005 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
1007 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1006 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1008 val cgoal = cterm_of @{theory} goal |
1007 val cgoal = cterm_of @{theory} goal |
1009 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1008 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1010 *} |
1009 *} |
1011 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
1010 prove {* Thm.term_of cgoal2 *} |
|
1011 apply (rule tp) |
|
1012 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
1012 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1013 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1013 (* apply (tactic {* foo_tac' @{context} 1 *}) |
1014 apply (tactic {* foo_tac' @{context} 1 *}) |
1014 done *) sorry |
1015 done |
1015 |
1016 |
1016 thm list_eq.intros(4) |
1017 thm list_eq.intros(4) |
1017 ML {* |
1018 ML {* |
1018 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
1019 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)})) |
1019 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1020 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1021 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1022 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1022 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1023 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1023 *} |
1024 *} |
1024 |
1025 |
1025 (* It is the same, but we need a name for it. *) |
1026 (* It is the same, but we need a name for it. *) |
1026 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
1027 prove {* Thm.term_of cgoal3 *} |
|
1028 apply (rule tp) |
|
1029 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
1027 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1030 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1028 apply (tactic {* foo_tac' @{context} 1 *}) |
1031 apply (tactic {* foo_tac' @{context} 1 *}) |
1029 sorry |
1032 done |
1030 lemma zzz : |
1033 lemma zzz : |
1031 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
1034 "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
1032 = (a # a # xs \<approx> a # xs)" |
1035 \<equiv> Trueprop (a # a # xs \<approx> a # xs)" |
|
1036 apply (rule tp) |
|
1037 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
1033 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1038 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1034 apply (tactic {* foo_tac' @{context} 1 *}) |
1039 apply (tactic {* foo_tac' @{context} 1 *}) |
1035 done |
1040 done |
1036 |
1041 |
1037 lemma zzz' : |
1042 lemma zzz' : |
1052 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
1057 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
1053 ) |
1058 ) |
1054 ) |
1059 ) |
1055 *} |
1060 *} |
1056 |
1061 |
1057 thm sym |
1062 |
1058 ML {* |
1063 thm list_eq.intros(5) |
1059 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm sym})) |
1064 ML {* |
|
1065 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
1060 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1066 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1061 *} |
1067 *} |
1062 ML {* |
1068 ML {* |
1063 val cgoal = |
1069 val cgoal = |
1064 Toplevel.program (fn () => |
1070 Toplevel.program (fn () => |
1065 cterm_of @{theory} goal |
1071 cterm_of @{theory} goal |
1066 ) |
1072 ) |
1067 *} |
1073 *} |
1068 |
|
1069 |
|
1070 thm list_eq.intros(5) |
|
1071 ML {* |
|
1072 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
|
1073 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
1074 *} |
|
1075 ML {* |
|
1076 val cgoal = |
|
1077 Toplevel.program (fn () => |
|
1078 cterm_of @{theory} goal |
|
1079 ) |
|
1080 *} |
|
1081 ML {* |
1074 ML {* |
1082 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1075 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1083 *} |
1076 *} |
1084 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
1077 prove {* Thm.term_of cgoal2 *} |
|
1078 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
1079 apply (rule tp) |
|
1080 apply (tactic {* ObjectLogic.full_atomize_tac 1 *}) |
1085 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1081 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1086 apply (tactic {* foo_tac' @{context} 1 *}) |
1082 apply (tactic {* foo_tac' @{context} 1 *}) |
1087 done |
1083 done |
1088 |
|
1089 |
1084 |
1090 thm list.induct |
1085 thm list.induct |
1091 ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *} |
1086 ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *} |
1092 |
1087 |
1093 ML {* |
1088 ML {* |