112 val flexflex_rule: thm -> thm Seq.seq |
112 val flexflex_rule: thm -> thm Seq.seq |
113 val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
113 val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
114 val trivial: cterm -> thm |
114 val trivial: cterm -> thm |
115 val class_triv: theory -> class -> thm |
115 val class_triv: theory -> class -> thm |
116 val varifyT: thm -> thm |
116 val varifyT: thm -> thm |
117 val varifyT': (string * sort) list -> thm -> thm * ((string * sort) * indexname) list |
117 val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm |
118 val freezeT: thm -> thm |
118 val freezeT: thm -> thm |
119 val dest_state: thm * int -> (term * term) list * term list * term * term |
119 val dest_state: thm * int -> (term * term) list * term list * term * term |
120 val lift_rule: cterm -> thm -> thm |
120 val lift_rule: cterm -> thm -> thm |
121 val incr_indexes: int -> thm -> thm |
121 val incr_indexes: int -> thm -> thm |
122 val assumption: int -> thm -> thm Seq.seq |
122 val assumption: int -> thm -> thm Seq.seq |
1072 val tfrees = foldr add_term_tfrees fixed hyps; |
1072 val tfrees = foldr add_term_tfrees fixed hyps; |
1073 val prop1 = attach_tpairs tpairs prop; |
1073 val prop1 = attach_tpairs tpairs prop; |
1074 val (prop2, al) = Type.varify (prop1, tfrees); |
1074 val (prop2, al) = Type.varify (prop1, tfrees); |
1075 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); |
1075 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); |
1076 in |
1076 in |
1077 (Thm {thy_ref = thy_ref, |
1077 (al, Thm {thy_ref = thy_ref, |
1078 der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, |
1078 der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, |
1079 maxidx = Int.max (0, maxidx), |
1079 maxidx = Int.max (0, maxidx), |
1080 shyps = shyps, |
1080 shyps = shyps, |
1081 hyps = hyps, |
1081 hyps = hyps, |
1082 tpairs = rev (map Logic.dest_equals ts), |
1082 tpairs = rev (map Logic.dest_equals ts), |
1083 prop = prop3}, al) |
1083 prop = prop3}) |
1084 end; |
1084 end; |
1085 |
1085 |
1086 val varifyT = #1 o varifyT' []; |
1086 val varifyT = #2 o varifyT' []; |
1087 |
1087 |
1088 (* Replace all TVars by new TFrees *) |
1088 (* Replace all TVars by new TFrees *) |
1089 fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
1089 fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
1090 let |
1090 let |
1091 val prop1 = attach_tpairs tpairs prop; |
1091 val prop1 = attach_tpairs tpairs prop; |