107 val abstract_rule: string -> cterm -> thm -> thm |
107 val abstract_rule: string -> cterm -> thm -> thm |
108 val combination: thm -> thm -> thm |
108 val combination: thm -> thm -> thm |
109 val equal_intr: thm -> thm -> thm |
109 val equal_intr: thm -> thm -> thm |
110 val equal_elim: thm -> thm -> thm |
110 val equal_elim: thm -> thm -> thm |
111 val flexflex_rule: thm -> thm Seq.seq |
111 val flexflex_rule: thm -> thm Seq.seq |
|
112 val generalize: string list * string list -> int -> thm -> thm |
112 val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
113 val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
113 val trivial: cterm -> thm |
114 val trivial: cterm -> thm |
114 val class_triv: theory -> class -> thm |
115 val class_triv: theory -> class -> thm |
115 val unconstrainT: ctyp -> thm -> thm |
116 val unconstrainT: ctyp -> thm -> thm |
116 val varifyT: thm -> thm |
117 val varifyT: thm -> thm |
146 val proof_attributes: attribute list -> Context.proof * thm -> Context.proof * thm |
147 val proof_attributes: attribute list -> Context.proof * thm -> Context.proof * thm |
147 val no_attributes: 'a -> 'a * 'b list |
148 val no_attributes: 'a -> 'a * 'b list |
148 val simple_fact: 'a -> ('a * 'b list) list |
149 val simple_fact: 'a -> ('a * 'b list) list |
149 val terms_of_tpairs: (term * term) list -> term list |
150 val terms_of_tpairs: (term * term) list -> term list |
150 val maxidx_of: thm -> int |
151 val maxidx_of: thm -> int |
|
152 val maxidx_thm: thm -> int -> int |
151 val hyps_of: thm -> term list |
153 val hyps_of: thm -> term list |
152 val full_prop_of: thm -> term |
154 val full_prop_of: thm -> term |
153 val get_name_tags: thm -> string * tag list |
155 val get_name_tags: thm -> string * tag list |
154 val put_name_tags: string * tag list -> thm -> thm |
156 val put_name_tags: string * tag list -> thm -> thm |
155 val name_of_thm: thm -> string |
157 val name_of_thm: thm -> string |
445 |
447 |
446 fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref; |
448 fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref; |
447 val sign_of_thm = theory_of_thm; |
449 val sign_of_thm = theory_of_thm; |
448 |
450 |
449 fun maxidx_of (Thm {maxidx, ...}) = maxidx; |
451 fun maxidx_of (Thm {maxidx, ...}) = maxidx; |
|
452 fun maxidx_thm th i = Int.max (maxidx_of th, i); |
450 fun hyps_of (Thm {hyps, ...}) = hyps; |
453 fun hyps_of (Thm {hyps, ...}) = hyps; |
451 fun prop_of (Thm {prop, ...}) = prop; |
454 fun prop_of (Thm {prop, ...}) = prop; |
452 fun proof_of (Thm {der = (_, proof), ...}) = proof; |
455 fun proof_of (Thm {der = (_, proof), ...}) = proof; |
453 fun tpairs_of (Thm {tpairs, ...}) = tpairs; |
456 fun tpairs_of (Thm {tpairs, ...}) = tpairs; |
454 |
457 |
969 shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps, |
972 shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps, |
970 hyps = hyps, |
973 hyps = hyps, |
971 tpairs = tpairs', |
974 tpairs = tpairs', |
972 prop = prop'} |
975 prop = prop'} |
973 end); |
976 end); |
|
977 |
|
978 |
|
979 (*Generalization of fixed variables |
|
980 A |
|
981 -------------------- |
|
982 A[?'a/'a, ?x/x, ...] |
|
983 *) |
|
984 |
|
985 fun generalize ([], []) _ th = th |
|
986 | generalize (tfrees, frees) idx th = |
|
987 let |
|
988 val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = th; |
|
989 val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); |
|
990 |
|
991 val bad_type = if null tfrees then K false else |
|
992 Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false); |
|
993 fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x |
|
994 | bad_term (Var (_, T)) = bad_type T |
|
995 | bad_term (Const (_, T)) = bad_type T |
|
996 | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t |
|
997 | bad_term (t $ u) = bad_term t orelse bad_term u |
|
998 | bad_term (Bound _) = false; |
|
999 val _ = exists bad_term hyps andalso |
|
1000 raise THM ("generalize: variable free in assumptions", 0, [th]); |
|
1001 |
|
1002 val gen = Term.generalize (tfrees, frees) idx; |
|
1003 val prop' = gen prop; |
|
1004 val tpairs' = map (pairself gen) tpairs; |
|
1005 val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); |
|
1006 in |
|
1007 Thm { |
|
1008 thy_ref = thy_ref, |
|
1009 der = Pt.infer_derivs' (Pt.generalize (tfrees, frees) idx) der, |
|
1010 maxidx = maxidx', |
|
1011 shyps = shyps, |
|
1012 hyps = hyps, |
|
1013 tpairs = tpairs', |
|
1014 prop = prop'} |
|
1015 end; |
974 |
1016 |
975 |
1017 |
976 (*Instantiation of Vars |
1018 (*Instantiation of Vars |
977 A |
1019 A |
978 -------------------- |
1020 -------------------- |