equal
deleted
inserted
replaced
9 (*modifying terms*) |
9 (*modifying terms*) |
10 val as_meta_eq: cterm -> cterm |
10 val as_meta_eq: cterm -> cterm |
11 |
11 |
12 (*theorem nets*) |
12 (*theorem nets*) |
13 val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net |
13 val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net |
14 val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net -> |
14 val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list |
15 cterm -> 'a option |
|
16 val net_instance: thm Net.net -> cterm -> thm option |
15 val net_instance: thm Net.net -> cterm -> thm option |
17 |
16 |
18 (*proof combinators*) |
17 (*proof combinators*) |
19 val under_assumption: (thm -> thm) -> cterm -> thm |
18 val under_assumption: (thm -> thm) -> cterm -> thm |
20 val with_conv: conv -> (cterm -> thm) -> cterm -> thm |
19 val with_conv: conv -> (cterm -> thm) -> cterm -> thm |
66 local |
65 local |
67 fun instances_from_net match f net ct = |
66 fun instances_from_net match f net ct = |
68 let |
67 let |
69 val lookup = if match then Net.match_term else Net.unify_term |
68 val lookup = if match then Net.match_term else Net.unify_term |
70 val xthms = lookup net (Thm.term_of ct) |
69 val xthms = lookup net (Thm.term_of ct) |
71 fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms |
70 fun select ct = map_filter (f (maybe_instantiate ct)) xthms |
72 fun first_of' f ct = |
71 fun select' ct = |
73 let val thm = Thm.trivial ct |
72 let val thm = Thm.trivial ct |
74 in get_first (f (try (fn rule => rule COMP thm))) xthms end |
73 in map_filter (f (try (fn rule => rule COMP thm))) xthms end |
75 in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end |
74 in (case select ct of [] => select' ct | xthms' => xthms') end |
76 in |
75 in |
77 |
76 |
78 fun net_instance' f = instances_from_net false f |
77 val net_instances = |
79 |
78 instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm)) |
80 val net_instance = instances_from_net true I |
79 |
|
80 val net_instance = try hd oo instances_from_net true I |
81 |
81 |
82 end |
82 end |
83 |
83 |
84 |
84 |
85 |
85 |