864 in |
864 in |
865 Logic.mk_equals (build_aux ctxt concl2, concl2) |
865 Logic.mk_equals (build_aux ctxt concl2, concl2) |
866 end |
866 end |
867 *} |
867 *} |
868 |
868 |
869 ML {* |
|
870 fun build_goal' ctxt thm constructors qty mk_rep_abs = |
|
871 let |
|
872 fun is_const (Const (x, t)) = member (op =) constructors x |
|
873 | is_const _ = false |
|
874 |
|
875 fun maybe_mk_rep_abs t = |
|
876 let |
|
877 val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t) |
|
878 in |
|
879 if type_of t = qty then mk_rep_abs t else t |
|
880 end |
|
881 (* handle TYPE _ => t*) |
|
882 fun build_aux ctxt1 (Abs (x, T, t)) = |
|
883 let |
|
884 val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1; |
|
885 val v = Free (x', T); |
|
886 val t' = subst_bound (v, t); |
|
887 val rec_term = build_aux ctxt2 t'; |
|
888 in Term.lambda_name (x, v) rec_term end |
|
889 | build_aux ctxt1 (f $ a) = |
|
890 let |
|
891 val (f, args) = strip_comb (f $ a) |
|
892 val _ = writeln (Syntax.string_of_term ctxt f) |
|
893 in |
|
894 if is_const f then |
|
895 maybe_mk_rep_abs |
|
896 (list_comb (f, map maybe_mk_rep_abs (map (build_aux ctxt1) args))) |
|
897 else list_comb (build_aux ctxt1 f, map (build_aux ctxt1) args) |
|
898 end |
|
899 | build_aux _ x = |
|
900 if is_const x then maybe_mk_rep_abs x else x |
|
901 |
|
902 val concl2 = term_of (#prop (crep_thm thm)) |
|
903 in |
|
904 Logic.mk_equals (build_aux ctxt concl2, concl2) |
|
905 end *} |
|
906 |
|
907 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
869 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
908 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
870 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
909 |
871 |
910 ML {* |
872 ML {* |
911 fun dest_cbinop t = |
873 fun dest_cbinop t = |
1002 rtac @{thm card1_rsp}, |
964 rtac @{thm card1_rsp}, |
1003 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
965 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
1004 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
966 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
1005 DatatypeAux.cong_tac, |
967 DatatypeAux.cong_tac, |
1006 rtac @{thm ext}, |
968 rtac @{thm ext}, |
1007 rtac @{thm eq_reflection}, |
969 (* rtac @{thm eq_reflection},*) |
1008 CHANGED o (ObjectLogic.full_atomize_tac) |
970 CHANGED o (ObjectLogic.full_atomize_tac) |
1009 ]) |
971 ]) |
1010 *} |
972 *} |
1011 |
973 |
1012 ML {* |
974 ML {* |
1094 using list_eq.intros(4) by (simp only: zzz) |
1056 using list_eq.intros(4) by (simp only: zzz) |
1095 |
1057 |
1096 thm QUOT_TYPE_I_fset.REPS_same |
1058 thm QUOT_TYPE_I_fset.REPS_same |
1097 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
1059 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
1098 |
1060 |
1099 ML Drule.instantiate' |
|
1100 ML {* zzz'' *} |
|
1101 text {* |
|
1102 A variable export will still be necessary in the end, but this is already the final theorem. |
|
1103 *} |
|
1104 ML {* |
|
1105 Toplevel.program (fn () => |
|
1106 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1107 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
|
1108 ) |
|
1109 ) |
|
1110 *} |
|
1111 |
|
1112 |
1061 |
1113 thm list_eq.intros(5) |
1062 thm list_eq.intros(5) |
1114 ML {* |
1063 ML {* |
1115 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1064 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1116 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1065 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1181 |
1130 |
1182 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1131 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1183 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1132 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1184 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1133 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1185 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1134 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
|
1135 local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *} |
1186 |
1136 |
1187 thm m1_lift |
1137 thm m1_lift |
1188 thm leqi4_lift |
1138 thm leqi4_lift |
1189 thm leqi5_lift |
1139 thm leqi5_lift |
1190 thm m2_lift |
1140 thm m2_lift |
|
1141 thm card_suc |
|
1142 (* The above is not good, we lost the ABS in front of xs on the rhs, so can't be properly instantiated... *) |
1191 |
1143 |
1192 ML Drule.instantiate' |
1144 ML Drule.instantiate' |
1193 text {* |
1145 text {* |
1194 We lost the schematic variable again :(. |
1146 We lost the schematic variable again :(. |
1195 Another variable export will still be necessary... |
1147 Another variable export will still be necessary... |
1243 ML {* @{term "\<exists>x. P x"} *} |
1191 ML {* @{term "\<exists>x. P x"} *} |
1244 ML {* Thm.bicompose *} |
1192 ML {* Thm.bicompose *} |
1245 prove {* (Thm.term_of cgoal2) *} |
1193 prove {* (Thm.term_of cgoal2) *} |
1246 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1194 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1247 apply (tactic {* foo_tac' @{context} 1 *}) |
1195 apply (tactic {* foo_tac' @{context} 1 *}) |
1248 |
1196 done |
1249 |
1197 |
1250 (* |
1198 (* |
1251 datatype obj1 = |
1199 datatype obj1 = |
1252 OVAR1 "string" |
1200 OVAR1 "string" |
1253 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
1201 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
1254 | INVOKE1 "obj1 \<Rightarrow> string" |
1202 | INVOKE1 "obj1 \<Rightarrow> string" |
1255 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)" |
1203 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)" |
1256 *) |
1204 *) |
1257 |
|
1258 |
|
1259 yyes |
|