137 val varifyT_global: thm -> thm |
137 val varifyT_global: thm -> thm |
138 val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm |
138 val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm |
139 val of_class: ctyp * class -> thm |
139 val of_class: ctyp * class -> thm |
140 val strip_shyps: thm -> thm |
140 val strip_shyps: thm -> thm |
141 val unconstrainT: thm -> thm |
141 val unconstrainT: thm -> thm |
142 val legacy_unconstrainT: ctyp -> thm -> thm |
|
143 val legacy_freezeT: thm -> thm |
142 val legacy_freezeT: thm -> thm |
144 val assumption: int -> thm -> thm Seq.seq |
143 val assumption: int -> thm -> thm Seq.seq |
145 val eq_assumption: int -> thm -> thm |
144 val eq_assumption: int -> thm -> thm |
146 val rotate_rule: int -> int -> thm -> thm |
145 val rotate_rule: int -> int -> thm -> thm |
147 val permute_prems: int -> int -> thm -> thm |
146 val permute_prems: int -> int -> thm -> thm |
1246 shyps = [[]], (*potentially redundant*) |
1245 shyps = [[]], (*potentially redundant*) |
1247 hyps = [], |
1246 hyps = [], |
1248 tpairs = [], |
1247 tpairs = [], |
1249 prop = prop'}) |
1248 prop = prop'}) |
1250 end; |
1249 end; |
1251 |
|
1252 fun legacy_unconstrainT |
|
1253 (Ctyp {thy_ref = thy_ref1, T, ...}) |
|
1254 (th as Thm (_, {thy_ref = thy_ref2, maxidx, shyps, hyps, tpairs, prop, ...})) = |
|
1255 let |
|
1256 val ((x, i), S) = Term.dest_TVar T handle TYPE _ => |
|
1257 raise THM ("unconstrainT: not a type variable", 0, [th]); |
|
1258 val T' = TVar ((x, i), []); |
|
1259 val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U)); |
|
1260 val constraints = Logic.mk_of_sort (T', S); |
|
1261 in |
|
1262 Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])), |
|
1263 {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), |
|
1264 tags = [], |
|
1265 maxidx = Int.max (maxidx, i), |
|
1266 shyps = Sorts.remove_sort S shyps, |
|
1267 hyps = hyps, |
|
1268 tpairs = map (pairself unconstrain) tpairs, |
|
1269 prop = Logic.list_implies (constraints, unconstrain prop)}) |
|
1270 end; |
|
1271 |
|
1272 |
1250 |
1273 (* Replace all TFrees not fixed or in the hyps by new TVars *) |
1251 (* Replace all TFrees not fixed or in the hyps by new TVars *) |
1274 fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = |
1252 fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = |
1275 let |
1253 let |
1276 val tfrees = fold Term.add_tfrees hyps fixed; |
1254 val tfrees = fold Term.add_tfrees hyps fixed; |