49 |
49 |
50 |
50 |
51 (*Are any of the constants in "bs" present in the term?*) |
51 (*Are any of the constants in "bs" present in the term?*) |
52 fun has_consts bs = |
52 fun has_consts bs = |
53 let fun has (Const(a,_)) = a mem bs |
53 let fun has (Const(a,_)) = a mem bs |
|
54 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false |
|
55 (*ignore constants within @-terms*) |
54 | has (f$u) = has f orelse has u |
56 | has (f$u) = has f orelse has u |
55 | has (Abs(_,_,t)) = has t |
57 | has (Abs(_,_,t)) = has t |
56 | has _ = false |
58 | has _ = false |
57 in has end; |
59 in has end; |
58 |
60 |
92 fun resop nf [prem] = resolve_tac (nf prem) 1; |
94 fun resop nf [prem] = resolve_tac (nf prem) 1; |
93 |
95 |
94 (*Conjunctive normal form, detecting tautologies early. |
96 (*Conjunctive normal form, detecting tautologies early. |
95 Strips universal quantifiers and breaks up conjunctions. *) |
97 Strips universal quantifiers and breaks up conjunctions. *) |
96 fun cnf_aux seen (th,ths) = |
98 fun cnf_aux seen (th,ths) = |
97 if taut_lits (literals(prop_of th) @ seen) then ths |
99 if taut_lits (literals(prop_of th) @ seen) |
98 else if not (has_consts ["All","op &"] (prop_of th)) then th::ths |
100 then ths (*tautology ignored*) |
|
101 else if not (has_consts ["All","op &"] (prop_of th)) |
|
102 then th::ths (*no work to do, terminate*) |
99 else (*conjunction?*) |
103 else (*conjunction?*) |
100 cnf_aux seen (th RS conjunct1, |
104 cnf_aux seen (th RS conjunct1, |
101 cnf_aux seen (th RS conjunct2, ths)) |
105 cnf_aux seen (th RS conjunct2, ths)) |
102 handle THM _ => (*universal quant?*) |
106 handle THM _ => (*universal quant?*) |
103 cnf_aux seen (freeze_spec th, ths) |
107 cnf_aux seen (freeze_spec th, ths) |