857 ML {* |
857 ML {* |
858 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
858 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
859 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}] |
859 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}] |
860 *} |
860 *} |
861 |
861 |
|
862 ML lambda |
|
863 |
862 ML {* |
864 ML {* |
863 fun build_goal thm constructors lifted_type mk_rep_abs = |
865 fun build_goal thm constructors lifted_type mk_rep_abs = |
864 let |
866 let |
865 fun is_const (Const (x, t)) = x mem constructors |
867 fun is_const (Const (x, t)) = x mem constructors |
866 | is_const _ = false |
868 | is_const _ = false |
868 let |
870 let |
869 val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) |
871 val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) |
870 in |
872 in |
871 if type_of t = lifted_type then mk_rep_abs t else t |
873 if type_of t = lifted_type then mk_rep_abs t else t |
872 end |
874 end |
873 handle TYPE _ => t |
875 (* handle TYPE _ => t*) |
874 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
876 fun build_aux (Abs (s, t, tr)) = |
|
877 let |
|
878 val [(fresh_s, _)] = Variable.variant_frees @{context} [] [(s, ())]; |
|
879 val newv = Free (fresh_s, t); |
|
880 val str = subst_bound (newv, tr); |
|
881 val rec_term = build_aux str; |
|
882 val bound_term = lambda newv rec_term |
|
883 in |
|
884 bound_term |
|
885 end |
875 | build_aux (f $ a) = |
886 | build_aux (f $ a) = |
876 let |
887 let |
877 val (f, args) = strip_comb (f $ a) |
888 val (f, args) = strip_comb (f $ a) |
878 val _ = writeln (Syntax.string_of_term @{context} f) |
889 val _ = writeln (Syntax.string_of_term @{context} f) |
879 in |
890 in |
917 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
928 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
918 ) |
929 ) |
919 *} |
930 *} |
920 |
931 |
921 ML {* |
932 ML {* |
922 fun foo_conv t = |
933 fun split_binop_conv t = |
923 let |
934 let |
|
935 val _ = tracing (Syntax.string_of_term @{context} (term_of t)) |
924 val (lhs, rhs) = dest_ceq t; |
936 val (lhs, rhs) = dest_ceq t; |
925 val (bop, _) = dest_cbinop lhs; |
937 val (bop, _) = dest_cbinop lhs; |
926 val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
938 val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
927 val [cmT, crT] = Thm.dest_ctyp cr2; |
939 val [cmT, crT] = Thm.dest_ctyp cr2; |
928 in |
940 in |
929 Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2} |
941 Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2} |
930 end |
942 end |
931 *} |
943 *} |
932 |
944 |
933 ML {* |
945 ML {* |
934 fun foo_tac n thm = |
946 fun split_arg_conv t = |
|
947 let |
|
948 val (lhs, rhs) = dest_ceq t; |
|
949 val (lop, larg) = Thm.dest_comb lhs; |
|
950 val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
|
951 in |
|
952 Drule.instantiate' [SOME caT,SOME crT] [NONE,NONE,SOME lop] @{thm arg_cong} |
|
953 end |
|
954 *} |
|
955 |
|
956 ML {* |
|
957 fun split_binop_tac n thm = |
935 let |
958 let |
936 val concl = Thm.cprem_of thm n; |
959 val concl = Thm.cprem_of thm n; |
937 val (_, cconcl) = Thm.dest_comb concl; |
960 val (_, cconcl) = Thm.dest_comb concl; |
938 val rewr = foo_conv cconcl; |
961 val rewr = split_binop_conv cconcl; |
939 (* val _ = tracing (Display.string_of_thm @{context} rewr) |
962 in |
940 val _ = tracing (Display.string_of_thm @{context} thm)*) |
963 rtac rewr n thm |
|
964 end |
|
965 handle CTERM _ => Seq.empty |
|
966 *} |
|
967 |
|
968 ML {* |
|
969 fun split_arg_tac n thm = |
|
970 let |
|
971 val concl = Thm.cprem_of thm n; |
|
972 val (_, cconcl) = Thm.dest_comb concl; |
|
973 val rewr = split_arg_conv cconcl; |
941 in |
974 in |
942 rtac rewr n thm |
975 rtac rewr n thm |
943 end |
976 end |
944 handle CTERM _ => Seq.empty |
977 handle CTERM _ => Seq.empty |
945 *} |
978 *} |
958 rtac @{thm cons_preserves}, |
991 rtac @{thm cons_preserves}, |
959 rtac @{thm mem_respects}, |
992 rtac @{thm mem_respects}, |
960 rtac @{thm card1_rsp}, |
993 rtac @{thm card1_rsp}, |
961 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
994 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
962 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
995 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
963 foo_tac, |
996 DatatypeAux.cong_tac, |
|
997 rtac @{thm ext}, |
|
998 (* rtac @{thm eq_reflection}*) |
964 CHANGED o (ObjectLogic.full_atomize_tac) |
999 CHANGED o (ObjectLogic.full_atomize_tac) |
965 ]) |
1000 ]) |
966 *} |
1001 *} |
967 |
1002 |
968 ML {* |
1003 ML {* |
1077 build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1111 build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1078 ) |
1112 ) |
1079 *} |
1113 *} |
1080 ML {* |
1114 ML {* |
1081 val cgoal = cterm_of @{theory} goal |
1115 val cgoal = cterm_of @{theory} goal |
|
1116 *} |
|
1117 ML {* |
1082 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1118 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1083 *} |
1119 *} |
1084 ML fset_defs_sym |
1120 |
1085 prove {* (Thm.term_of cgoal2) *} |
1121 prove {* (Thm.term_of cgoal2) *} |
1086 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1122 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1087 apply (tactic {* foo_tac' @{context} 1 *}) |
1123 apply (tactic {* foo_tac' @{context} 1 *}) |
1088 apply (rule_tac f = "P" in arg_cong) |
|
1089 sorry |
1124 sorry |
1090 |
1125 |
1091 thm card1_suc |
1126 thm card1_suc |
1092 |
1127 |
1093 ML {* |
1128 ML {* |
1098 *} |
1133 *} |
1099 ML {* |
1134 ML {* |
1100 val cgoal = cterm_of @{theory} goal |
1135 val cgoal = cterm_of @{theory} goal |
1101 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1136 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1102 *} |
1137 *} |
|
1138 ML {* @{term "\<exists>x. P x"} *} |
1103 prove {* (Thm.term_of cgoal2) *} |
1139 prove {* (Thm.term_of cgoal2) *} |
1104 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1140 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1105 apply (tactic {* foo_tac' @{context} 1 *}) |
1141 apply (tactic {* foo_tac' @{context} 1 *}) |
1106 |
1142 done |
1107 |
1143 |
1108 |
1144 |
1109 (* |
1145 (* |
1110 datatype obj1 = |
1146 datatype obj1 = |
1111 OVAR1 "string" |
1147 OVAR1 "string" |