equal
deleted
inserted
replaced
908 val (bop, lhs) = Thm.dest_comb t2; |
908 val (bop, lhs) = Thm.dest_comb t2; |
909 in |
909 in |
910 (bop, (lhs, rhs)) |
910 (bop, (lhs, rhs)) |
911 end |
911 end |
912 *} |
912 *} |
|
913 |
913 ML {* |
914 ML {* |
914 fun dest_ceq t = |
915 fun dest_ceq t = |
915 let |
916 let |
916 val (bop, pair) = dest_cbinop t; |
917 val (bop, pair) = dest_cbinop t; |
917 val (bop_s, _) = Term.dest_Const (Thm.term_of bop); |
918 val (bop_s, _) = Term.dest_Const (Thm.term_of bop); |
1159 Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift} |
1160 Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift} |
1160 ) |
1161 ) |
1161 ) |
1162 ) |
1162 *} |
1163 *} |
1163 |
1164 |
|
1165 thm leqi4_lift |
|
1166 ML {* |
|
1167 val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) [])) |
|
1168 val (_, l) = dest_Type typ |
|
1169 val t = Type ("QuotMain.fset", l) |
|
1170 val v = Var (nam, t) |
|
1171 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
|
1172 *} |
|
1173 |
|
1174 ML {* |
|
1175 term_of (#prop (crep_thm @{thm sym})) |
|
1176 *} |
|
1177 |
|
1178 ML {* |
|
1179 Toplevel.program (fn () => |
|
1180 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1181 Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift} |
|
1182 ) |
|
1183 ) |
|
1184 *} |
|
1185 |
|
1186 |
1164 |
1187 |
1165 |
1188 |
1166 |
1189 |
1167 ML {* MRS *} |
1190 ML {* MRS *} |
1168 thm card1_suc |
1191 thm card1_suc |
1176 ML {* |
1199 ML {* |
1177 val cgoal = cterm_of @{theory} goal |
1200 val cgoal = cterm_of @{theory} goal |
1178 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1201 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1179 *} |
1202 *} |
1180 ML {* @{term "\<exists>x. P x"} *} |
1203 ML {* @{term "\<exists>x. P x"} *} |
|
1204 ML {* Thm.bicompose *} |
1181 prove {* (Thm.term_of cgoal2) *} |
1205 prove {* (Thm.term_of cgoal2) *} |
1182 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1206 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1183 apply (tactic {* foo_tac' @{context} 1 *}) |
1207 apply (tactic {* foo_tac' @{context} 1 *}) |
1184 done |
|
1185 |
1208 |
1186 |
1209 |
1187 (* |
1210 (* |
1188 datatype obj1 = |
1211 datatype obj1 = |
1189 OVAR1 "string" |
1212 OVAR1 "string" |