equal
deleted
inserted
replaced
827 val consts = [@{const_name "Nil"}, @{const_name "append"}, |
827 val consts = [@{const_name "Nil"}, @{const_name "append"}, |
828 @{const_name "Cons"}, @{const_name "membship"}, |
828 @{const_name "Cons"}, @{const_name "membship"}, |
829 @{const_name "card1"}] |
829 @{const_name "card1"}] |
830 *} |
830 *} |
831 |
831 |
|
832 ML {* val qty = @{typ "'a fset"} *} |
|
833 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *} |
|
834 ML {* val fall = Const(@{const_name all}, tt) *} |
|
835 |
832 ML {* |
836 ML {* |
833 fun build_goal ctxt thm constructors rty qty mk_rep mk_abs = |
837 fun build_goal ctxt thm constructors rty qty mk_rep mk_abs = |
834 let |
838 let |
835 fun mk_rep_abs x = mk_rep (mk_abs x); |
839 fun mk_rep_abs x = mk_rep (mk_abs x); |
836 |
840 |
841 let |
845 let |
842 val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t) |
846 val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t) |
843 in |
847 in |
844 if fastype_of t = rty then mk_rep_abs t else t |
848 if fastype_of t = rty then mk_rep_abs t else t |
845 end; |
849 end; |
|
850 |
|
851 fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty |
|
852 | is_all _ = false; |
846 |
853 |
847 fun build_aux ctxt1 tm = |
854 fun build_aux ctxt1 tm = |
848 let |
855 let |
849 val (head, args) = Term.strip_comb tm; |
856 val (head, args) = Term.strip_comb tm; |
850 val args' = map (build_aux ctxt1) args; |
857 val args' = map (build_aux ctxt1) args; |
865 val v = Free (x', T); |
872 val v = Free (x', T); |
866 val t' = subst_bound (v, t); |
873 val t' = subst_bound (v, t); |
867 val rec_term = build_aux ctxt2 t'; |
874 val rec_term = build_aux ctxt2 t'; |
868 in Term.lambda_name (x, v) rec_term end |
875 in Term.lambda_name (x, v) rec_term end |
869 | _ => |
876 | _ => |
870 if is_constructor head then |
877 if is_all head then (* I assume that we never lift 'prop' since it is not of sort type *) |
|
878 list_comb (fall, args') |
|
879 else if is_constructor head then |
871 maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args')) |
880 maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args')) |
872 else maybe_mk_rep_abs (list_comb (head, args'))) |
881 else |
|
882 maybe_mk_rep_abs (list_comb (head, args')) |
|
883 ) |
873 end; |
884 end; |
874 |
885 |
875 val concl2 = Thm.prop_of thm; |
886 val concl2 = Thm.prop_of thm; |
876 in |
887 in |
877 Logic.mk_equals (build_aux ctxt concl2, concl2) |
888 Logic.mk_equals (build_aux ctxt concl2, concl2) |
1093 val goal = |
1104 val goal = |
1094 Toplevel.program (fn () => |
1105 Toplevel.program (fn () => |
1095 build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1106 build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1096 ) |
1107 ) |
1097 *} |
1108 *} |
1098 term all |
|
1099 ML {* |
1109 ML {* |
1100 val cgoal = |
1110 val cgoal = |
1101 Toplevel.program (fn () => |
1111 Toplevel.program (fn () => |
1102 cterm_of @{theory} goal |
1112 cterm_of @{theory} goal |
1103 ) |
1113 ) |
1140 |
1150 |
1141 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1151 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1142 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1152 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1143 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1153 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1144 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1154 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1145 local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *} |
1155 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
1146 |
1156 |
1147 thm m1_lift |
1157 thm m1_lift |
1148 thm leqi4_lift |
1158 thm leqi4_lift |
1149 thm leqi5_lift |
1159 thm leqi5_lift |
1150 thm m2_lift |
1160 thm m2_lift |
1151 thm card_suc |
1161 (*thm card_suc*) |
1152 |
1162 |
1153 thm leqi4_lift |
1163 thm leqi4_lift |
1154 ML {* |
1164 ML {* |
1155 val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) [])) |
1165 val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) [])) |
1156 val (_, l) = dest_Type typ |
1166 val (_, l) = dest_Type typ |
1165 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1175 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1166 ) |
1176 ) |
1167 ) |
1177 ) |
1168 *} |
1178 *} |
1169 |
1179 |
|
1180 (* |
1170 thm card_suc |
1181 thm card_suc |
1171 ML {* |
1182 ML {* |
1172 val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) []))) |
1183 val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) []))) |
1173 val (_, l) = dest_Type typ |
1184 val (_, l) = dest_Type typ |
1174 val t = Type ("QuotMain.fset", l) |
1185 val t = Type ("QuotMain.fset", l) |
1181 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1192 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1182 Drule.instantiate' [] [SOME (cv)] @{thm card_suc} |
1193 Drule.instantiate' [] [SOME (cv)] @{thm card_suc} |
1183 ) |
1194 ) |
1184 ) |
1195 ) |
1185 *} |
1196 *} |
1186 |
1197 *) |
1187 |
1198 |
1188 |
1199 |
1189 |
1200 |
1190 |
1201 |
1191 thm card1_suc |
1202 thm card1_suc |
1194 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1205 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1195 *} |
1206 *} |
1196 ML {* |
1207 ML {* |
1197 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1208 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1198 *} |
1209 *} |
1199 ML {* |
1210 ML {* term_of @{cpat "all"} *} |
1200 val cgoal = cterm_of @{theory} goal |
1211 ML {* |
|
1212 val cgoal = |
|
1213 Toplevel.program (fn () => |
|
1214 cterm_of @{theory} goal |
|
1215 ); |
1201 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1216 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1202 *} |
1217 *} |
1203 ML {* @{term "\<exists>x. P x"} *} |
1218 ML {* @{term "\<exists>x. P x"} *} |
1204 ML {* Thm.bicompose *} |
1219 ML {* Thm.bicompose *} |
1205 prove aaa: {* (Thm.term_of cgoal2) *} |
1220 prove aaa: {* (Thm.term_of cgoal2) *} |