57 val match: cterm * cterm -> |
57 val match: cterm * cterm -> |
58 ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
58 ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
59 val first_order_match: cterm * cterm -> |
59 val first_order_match: cterm * cterm -> |
60 ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
60 ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list |
61 (*theorems*) |
61 (*theorems*) |
62 val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a |
62 val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a |
63 val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a |
63 val fold_atomic_ctyps: {hyps: bool} -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a |
64 val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a |
64 val fold_atomic_cterms: {hyps: bool} -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a |
65 val terms_of_tpairs: (term * term) list -> term list |
65 val terms_of_tpairs: (term * term) list -> term list |
66 val full_prop_of: thm -> term |
66 val full_prop_of: thm -> term |
67 val theory_id: thm -> Context.theory_id |
67 val theory_id: thm -> Context.theory_id |
68 val theory_name: thm -> string |
68 val theory_name: thm -> string |
69 val maxidx_of: thm -> int |
69 val maxidx_of: thm -> int |
432 (*errors involving theorems*) |
432 (*errors involving theorems*) |
433 exception THM of string * int * thm list; |
433 exception THM of string * int * thm list; |
434 |
434 |
435 fun rep_thm (Thm (_, args)) = args; |
435 fun rep_thm (Thm (_, args)) = args; |
436 |
436 |
437 fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) = |
437 fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) = |
438 fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps; |
438 fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps; |
439 |
439 |
440 fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) = |
440 fun fold_atomic_ctyps h f (th as Thm (_, {cert, maxidx, shyps, ...})) = |
441 let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} |
441 let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} |
442 in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end; |
442 in (fold_terms h o fold_types o fold_atyps) (f o ctyp) th end; |
443 |
443 |
444 fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) = |
444 fun fold_atomic_cterms h f (th as Thm (_, {cert, maxidx, shyps, ...})) = |
445 let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in |
445 let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in |
446 (fold_terms o fold_aterms) |
446 (fold_terms h o fold_aterms) |
447 (fn t as Const (_, T) => f (cterm t T) |
447 (fn t as Const (_, T) => f (cterm t T) |
448 | t as Free (_, T) => f (cterm t T) |
448 | t as Free (_, T) => f (cterm t T) |
449 | t as Var (_, T) => f (cterm t T) |
449 | t as Var (_, T) => f (cterm t T) |
450 | _ => I) th |
450 | _ => I) th |
451 end; |
451 end; |
983 |
983 |
984 end; |
984 end; |
985 |
985 |
986 (*Dangling sort constraints of a thm*) |
986 (*Dangling sort constraints of a thm*) |
987 fun extra_shyps (th as Thm (_, {shyps, ...})) = |
987 fun extra_shyps (th as Thm (_, {shyps, ...})) = |
988 Sorts.subtract (fold_terms Sorts.insert_term th []) shyps; |
988 Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps; |
989 |
989 |
990 (*Remove extra sorts that are witnessed by type signature information*) |
990 (*Remove extra sorts that are witnessed by type signature information*) |
991 fun strip_shyps thm = |
991 fun strip_shyps thm = |
992 (case thm of |
992 (case thm of |
993 Thm (_, {shyps = [], ...}) => thm |
993 Thm (_, {shyps = [], ...}) => thm |
999 val minimize = Sorts.minimize_sort algebra; |
999 val minimize = Sorts.minimize_sort algebra; |
1000 val le = Sorts.sort_le algebra; |
1000 val le = Sorts.sort_le algebra; |
1001 fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); |
1001 fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); |
1002 fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)]; |
1002 fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)]; |
1003 |
1003 |
1004 val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; |
1004 val present = |
|
1005 (fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; |
1005 val extra = fold (Sorts.remove_sort o #2) present shyps; |
1006 val extra = fold (Sorts.remove_sort o #2) present shyps; |
1006 val witnessed = Sign.witness_sorts thy present extra; |
1007 val witnessed = Sign.witness_sorts thy present extra; |
1007 val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize); |
1008 val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize); |
1008 |
1009 |
1009 val extra' = |
1010 val extra' = |