# HG changeset patch # User paulson # Date 1134484063 -3600 # Node ID 8352b1d3b6399cf6eea1524583a50dd4207dac05 # Parent ab1a710a68cee028a92f7b2044d7ff54fb218321 removal of functional reflexivity axioms diff -r ab1a710a68ce -r 8352b1d3b639 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Tue Dec 13 10:39:32 2005 +0100 +++ b/src/HOL/Hilbert_Choice.thy Tue Dec 13 15:27:43 2005 +0100 @@ -458,6 +458,7 @@ and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *} + and meson_not_refl_disj_D: "x ~= x | P ==> P" by fast+ diff -r ab1a710a68ce -r 8352b1d3b639 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Dec 13 10:39:32 2005 +0100 +++ b/src/HOL/Tools/meson.ML Tue Dec 13 15:27:43 2005 +0100 @@ -104,20 +104,69 @@ (*number of literals in a term*) val nliterals = length o literals; -(*to detect, and remove, tautologous clauses*) -fun taut_lits [] = false - | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; - -(*Include False as a literal: an occurrence of ~False is a tautology*) -fun is_taut th = taut_lits ((true, HOLogic.false_const) :: - literals (prop_of th)); - (*Generation of unique names -- maxidx cannot be relied upon to increase! Cannot rely on "variant", since variables might coincide when literals are joined to make a clause... 19 chooses "U" as the first variable name*) val name_ref = ref 19; + +(*** Tautology Checking ***) + +fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) = + signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) + | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits) + | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); + +fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); + +(*Literals like X=X are tautologous*) +fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u + | taut_poslit (Const("True",_)) = true + | taut_poslit _ = false; + +fun is_taut th = + let val (poslits,neglits) = signed_lits th + in exists taut_poslit poslits + orelse + exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits) + end; + + +(*** To remove trivial negated equality literals from clauses ***) + +(*They are typically functional reflexivity axioms and are the converses of + injectivity equivalences*) + +val not_refl_disj_D = thm"meson_not_refl_disj_D"; + +fun refl_clause_aux 0 th = th + | refl_clause_aux n th = +(debug ("refl_clause_aux " ^ Int.toString n ^ " " ^ string_of_thm th); + case HOLogic.dest_Trueprop (concl_of th) of + (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => + refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) + | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => + if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*) + (refl_clause_aux (n-1) (th RS not_refl_disj_D) (*delete*) + handle THM _ => refl_clause_aux (n-1) (th RS disj_comm)) (*ignore*) + else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) + | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) + | _ => (*not a disjunction*) th); + +fun notequal_lits_count (Const ("op |", _) $ P $ Q) = + notequal_lits_count P + notequal_lits_count Q + | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 + | notequal_lits_count _ = 0; + +(*Simplify a clause by applying reflexivity to its negated equality literals*) +fun refl_clause th = + let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) + in zero_var_indexes (refl_clause_aux neqs th) end; + + +(*** The basic CNF transformation ***) + (*Replaces universally quantified variables by FREE variables -- because assumptions may not contain scheme variables. Later, call "generalize". *) fun freeze_spec th = @@ -131,45 +180,48 @@ presumably to instantiate a Boolean variable.*) fun resop nf [prem] = resolve_tac (nf prem) 1; +val has_meta_conn = + exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]); + (*Conjunctive normal form, adding clauses from th in front of ths (for foldr). - Detects tautologies early, with "seen" holding the other literals of a clause. Strips universal quantifiers and breaks up conjunctions. Eliminates existential quantifiers using skoths: Skolemization theorems.*) fun cnf skoths (th,ths) = - let fun cnf_aux seen (th,ths) = - if taut_lits (literals(prop_of th) @ seen) - then ths (*tautology ignored*) - else if not (has_consts ["All","Ex","op &"] (prop_of th)) + let fun cnf_aux (th,ths) = + if has_meta_conn (prop_of th) then ths (*meta-level: ignore*) + else if not (has_consts ["All","Ex","op &"] (prop_of th)) then th::ths (*no work to do, terminate*) else case head_of (HOLogic.dest_Trueprop (concl_of th)) of Const ("op &", _) => (*conjunction*) - cnf_aux seen (th RS conjunct1, - cnf_aux seen (th RS conjunct2, ths)) + cnf_aux (th RS conjunct1, + cnf_aux (th RS conjunct2, ths)) | Const ("All", _) => (*universal quantifier*) - cnf_aux seen (freeze_spec th, ths) + cnf_aux (freeze_spec th, ths) | Const ("Ex", _) => (*existential quantifier: Insert Skolem functions*) - cnf_aux seen (tryres (th,skoths), ths) + cnf_aux (tryres (th,skoths), ths) | Const ("op |", _) => (*disjunction*) let val tac = - (METAHYPS (resop (cnf_nil seen)) 1) THEN + (METAHYPS (resop cnf_nil) 1) THEN (fn st' => st' |> METAHYPS - (resop (cnf_nil (literals (concl_of st') @ seen))) 1) + (resop cnf_nil) 1) in Seq.list_of (tac (th RS disj_forward)) @ ths end | _ => (*no work to do*) th::ths - and cnf_nil seen th = (cnf_aux seen (th,[])) + and cnf_nil th = (cnf_aux (th,[])) in name_ref := 19; (*It's safe to reset this in a top-level call to cnf*) (cnf skoths (th RS conjunct1, cnf skoths (th RS conjunct2, ths)) - handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)) + handle THM _ => (*not a conjunction*) cnf_aux (th, ths)) end; (*Convert all suitable free variables to schematic variables, but don't discharge assumptions.*) fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th)); -fun make_cnf skoths th = map generalize (cnf skoths (th, [])); +fun make_cnf skoths th = + filter (not o is_taut) + (map (refl_clause o generalize) (cnf skoths (th, []))); (**** Removal of duplicate literals ****) @@ -217,9 +269,7 @@ (*Sort clauses by number of literals*) fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); -(*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*) -fun sort_clauses ths = - sort (make_ord fewerlits) (List.filter (not o is_taut) ths); +fun sort_clauses ths = sort (make_ord fewerlits) ths; (*True if the given type contains bool anywhere*) fun has_bool (Type("bool",_)) = true @@ -239,9 +289,6 @@ exists_Const (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T)); -val has_meta_conn = - exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]); - (*Raises an exception if any Vars in the theorem mention type bool; they could cause make_horn to loop! Also rejects functions whose arguments are Booleans or other functions.*)