1.1 --- a/src/HOL/Tools/meson.ML	Thu Jun 15 17:50:30 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jun 15 17:50:47 2006 +0200
     1.3 @@ -123,7 +123,8 @@
     1.4    in  exists taut_poslit poslits
     1.5        orelse
     1.6        exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
     1.7 -  end;
     1.8 +  end
     1.9 +  handle TERM _ => false;	(*probably dest_Trueprop on a weird theorem*)		      
    1.10  
    1.11  
    1.12  (*** To remove trivial negated equality literals from clauses ***)
    1.13 @@ -154,11 +155,20 @@
    1.14  (*Simplify a clause by applying reflexivity to its negated equality literals*)
    1.15  fun refl_clause th = 
    1.16    let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
    1.17 -  in  zero_var_indexes (refl_clause_aux neqs th)  end;
    1.18 +  in  zero_var_indexes (refl_clause_aux neqs th)  end
    1.19 +  handle TERM _ => th;	(*probably dest_Trueprop on a weird theorem*)		      
    1.20  
    1.21  
    1.22  (*** The basic CNF transformation ***)
    1.23  
    1.24 +(*Estimate the number of clauses in order to detect infeasible theorems*)
    1.25 +fun nclauses (Const("Trueprop",_) $ t) = nclauses t
    1.26 +  | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u
    1.27 +  | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t
    1.28 +  | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t
    1.29 +  | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u
    1.30 +  | nclauses _ = 1; (* literal *)
    1.31 +
    1.32  (*Replaces universally quantified variables by FREE variables -- because
    1.33    assumptions may not contain scheme variables.  Later, call "generalize". *)
    1.34  fun freeze_spec th =
    1.35 @@ -179,7 +189,7 @@
    1.36    Eliminates existential quantifiers using skoths: Skolemization theorems.*)
    1.37  fun cnf skoths (th,ths) =
    1.38    let fun cnf_aux (th,ths) =
    1.39 -        if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
    1.40 +  	if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
    1.41          else if not (has_consts ["All","Ex","op &"] (prop_of th))  
    1.42  	then th::ths (*no work to do, terminate*)
    1.43  	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
    1.44 @@ -199,7 +209,9 @@
    1.45  	  | _ => (*no work to do*) th::ths 
    1.46        and cnf_nil th = cnf_aux (th,[])
    1.47    in 
    1.48 -    cnf_aux (th,ths)
    1.49 +    if nclauses (concl_of th) > 20 
    1.50 +    then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
    1.51 +    else cnf_aux (th,ths)
    1.52    end;
    1.53  
    1.54  (*Convert all suitable free variables to schematic variables, 
    1.55 @@ -379,15 +391,18 @@
    1.56    which are needed to avoid the various one-point theorems from generating junk clauses.*)
    1.57  val tag_True = thm "tag_True";
    1.58  val tag_False = thm "tag_False";
    1.59 -val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
    1.60 +val nnf_simps =
    1.61 +     [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True, 
    1.62 +      if_False, if_cancel, if_eq_cancel, cases_simp];
    1.63 +val nnf_extra_simps =
    1.64 +      thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
    1.65  
    1.66  val nnf_ss =
    1.67 -    HOL_basic_ss addsimps
    1.68 -     (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @
    1.69 -      thms"split_ifs" @ ex_simps @ all_simps @ simp_thms)
    1.70 -     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
    1.71 +    HOL_basic_ss addsimps nnf_extra_simps 
    1.72 +                 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
    1.73  
    1.74 -fun make_nnf th = th |> simplify nnf_ss
    1.75 +fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.76 +                     |> simplify nnf_ss  (*But this doesn't simplify premises...*)
    1.77                       |> make_nnf1
    1.78  
    1.79  (*Pull existential quantifiers to front. This accomplishes Skolemization for