equal
deleted
inserted
replaced
855 val rec_term = build_aux ctxt2 t'; |
855 val rec_term = build_aux ctxt2 t'; |
856 in Term.lambda_name (x, v) rec_term end |
856 in Term.lambda_name (x, v) rec_term end |
857 | _ => |
857 | _ => |
858 if is_constructor head then |
858 if is_constructor head then |
859 maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args')) |
859 maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args')) |
860 else list_comb (head, args')) |
860 else maybe_mk_rep_abs (list_comb (head, args'))) |
861 end; |
861 end; |
862 |
862 |
863 val concl2 = Thm.prop_of thm; |
863 val concl2 = Thm.prop_of thm; |
864 in |
864 in |
865 Logic.mk_equals (build_aux ctxt concl2, concl2) |
865 Logic.mk_equals (build_aux ctxt concl2, concl2) |
1038 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1038 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1039 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1039 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1040 *} |
1040 *} |
1041 |
1041 |
1042 (* It is the same, but we need a name for it. *) |
1042 (* It is the same, but we need a name for it. *) |
1043 prove {* Thm.term_of cgoal3 *} |
1043 prove zzz : {* Thm.term_of cgoal3 *} |
1044 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1045 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1046 done |
|
1047 lemma zzz : |
|
1048 "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs))) |
|
1049 \<equiv> Trueprop (a # a # xs \<approx> a # xs)" |
|
1050 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1044 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1051 apply (tactic {* foo_tac' @{context} 1 *}) |
1045 apply (tactic {* foo_tac' @{context} 1 *}) |
1052 done |
1046 done |
1053 |
1047 |
1054 lemma zzz' : |
1048 lemma zzz' : |
1137 thm m1_lift |
1131 thm m1_lift |
1138 thm leqi4_lift |
1132 thm leqi4_lift |
1139 thm leqi5_lift |
1133 thm leqi5_lift |
1140 thm m2_lift |
1134 thm m2_lift |
1141 thm card_suc |
1135 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... *) |
|
1143 |
|
1144 ML Drule.instantiate' |
|
1145 text {* |
|
1146 We lost the schematic variable again :(. |
|
1147 Another variable export will still be necessary... |
|
1148 *} |
|
1149 ML {* |
|
1150 Toplevel.program (fn () => |
|
1151 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1152 Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift} |
|
1153 ) |
|
1154 ) |
|
1155 *} |
|
1156 |
1136 |
1157 thm leqi4_lift |
1137 thm leqi4_lift |
1158 ML {* |
1138 ML {* |
1159 val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) [])) |
1139 val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) [])) |
1160 val (_, l) = dest_Type typ |
1140 val (_, l) = dest_Type typ |
1162 val v = Var (nam, t) |
1142 val v = Var (nam, t) |
1163 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
1143 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
1164 *} |
1144 *} |
1165 |
1145 |
1166 ML {* |
1146 ML {* |
1167 term_of (#prop (crep_thm @{thm sym})) |
|
1168 *} |
|
1169 |
|
1170 ML {* |
|
1171 Toplevel.program (fn () => |
1147 Toplevel.program (fn () => |
1172 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1148 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
1173 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1149 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
1174 ) |
1150 ) |
1175 ) |
1151 ) |
1176 *} |
1152 *} |
1177 |
1153 |
1178 ML {* MRS *} |
1154 thm card_suc |
|
1155 ML {* |
|
1156 val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) []))) |
|
1157 val (_, l) = dest_Type typ |
|
1158 val t = Type ("QuotMain.fset", l) |
|
1159 val v = Var (nam, t) |
|
1160 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
|
1161 *} |
|
1162 |
|
1163 ML {* |
|
1164 Toplevel.program (fn () => |
|
1165 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1166 Drule.instantiate' [] [SOME (cv)] @{thm card_suc} |
|
1167 ) |
|
1168 ) |
|
1169 *} |
|
1170 |
|
1171 |
|
1172 |
|
1173 |
|
1174 |
1179 thm card1_suc |
1175 thm card1_suc |
1180 |
1176 |
1181 ML {* |
1177 ML {* |
1182 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1178 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1183 *} |
1179 *} |
1188 val cgoal = cterm_of @{theory} goal |
1184 val cgoal = cterm_of @{theory} goal |
1189 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1185 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1190 *} |
1186 *} |
1191 ML {* @{term "\<exists>x. P x"} *} |
1187 ML {* @{term "\<exists>x. P x"} *} |
1192 ML {* Thm.bicompose *} |
1188 ML {* Thm.bicompose *} |
1193 prove {* (Thm.term_of cgoal2) *} |
1189 prove aaa: {* (Thm.term_of cgoal2) *} |
1194 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1190 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1195 apply (tactic {* foo_tac' @{context} 1 *}) |
1191 apply (tactic {* foo_tac' @{context} 1 *}) |
1196 done |
1192 done |
|
1193 |
|
1194 thm aaa |
1197 |
1195 |
1198 (* |
1196 (* |
1199 datatype obj1 = |
1197 datatype obj1 = |
1200 OVAR1 "string" |
1198 OVAR1 "string" |
1201 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
1199 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |