72 | string_for_pattern (PApp (s, ps)) = |
72 | string_for_pattern (PApp (s, ps)) = |
73 if null ps then s else s ^ string_for_patterns ps |
73 if null ps then s else s ^ string_for_patterns ps |
74 and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" |
74 and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" |
75 |
75 |
76 (*Is the second type an instance of the first one?*) |
76 (*Is the second type an instance of the first one?*) |
77 fun match_pattern (PApp (a, T), PApp (b, U)) = |
77 fun match_pattern (PVar, _) = true |
78 a = b andalso match_patterns (T, U) |
78 | match_pattern (PApp _, PVar) = false |
79 | match_pattern (PVar, _) = true |
79 | match_pattern (PApp (s, ps), PApp (t, qs)) = |
80 | match_pattern (_, PVar) = false |
80 s = t andalso match_patterns (ps, qs) |
81 and match_patterns ([], []) = true |
81 and match_patterns (_, []) = true |
82 | match_patterns (T :: Ts, U :: Us) = |
82 | match_patterns ([], _) = false |
83 match_pattern (T, U) andalso match_patterns (Ts, Us) |
83 | match_patterns (p :: ps, q :: qs) = |
|
84 match_pattern (p, q) andalso match_patterns (ps, qs) |
84 |
85 |
85 (* Is there a unifiable constant? *) |
86 (* Is there a unifiable constant? *) |
86 fun pconst_mem f const_tab (s, ps) = |
87 fun pconst_mem f const_tab (s, ps) = |
87 exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s)) |
88 exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s)) |
88 |
89 |
106 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, |
107 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}, |
107 @{const_name "op ="}] |
108 @{const_name "op ="}] |
108 |
109 |
109 (* Add a pconstant to the table, but a [] entry means a standard |
110 (* Add a pconstant to the table, but a [] entry means a standard |
110 connective, which we ignore.*) |
111 connective, which we ignore.*) |
111 fun add_pconst_to_table also_skolem (c, Ts) = |
112 fun add_pconst_to_table also_skolem (c, ps) = |
112 if member (op =) boring_consts c orelse |
113 if member (op =) boring_consts c orelse |
113 (not also_skolem andalso String.isPrefix skolem_prefix c) then |
114 (not also_skolem andalso String.isPrefix skolem_prefix c) then |
114 I |
115 I |
115 else |
116 else |
116 Symtab.map_default (c, [Ts]) (fn Tss => insert (op =) Ts Tss) |
117 Symtab.map_default (c, [ps]) (insert (op =) ps) |
117 |
118 |
118 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) |
119 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) |
119 |
120 |
120 fun get_pconsts thy also_skolems pos ts = |
121 fun get_pconsts thy also_skolems pos ts = |
121 let |
122 let |
221 |
222 |
222 |
223 |
223 (**** Actual Filtering Code ****) |
224 (**** Actual Filtering Code ****) |
224 |
225 |
225 (*The frequency of a constant is the sum of those of all instances of its type.*) |
226 (*The frequency of a constant is the sum of those of all instances of its type.*) |
226 fun pconst_freq match const_tab (c, Ts) = |
227 fun pconst_freq match const_tab (c, ps) = |
227 CTtab.fold (fn (Ts', m) => match (Ts, Ts') ? Integer.add m) |
228 CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) |
228 (the (Symtab.lookup const_tab c)) 0 |
229 (the (Symtab.lookup const_tab c)) 0 |
229 |
230 |
230 |
231 |
231 (* A surprising number of theorems contain only a few significant constants. |
232 (* A surprising number of theorems contain only a few significant constants. |
232 These include all induction rules, and other general theorems. *) |
233 These include all induction rules, and other general theorems. *) |