1.1 --- a/src/HOL/Tools/meson.ML	Tue Oct 24 12:02:53 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Oct 26 10:48:35 2006 +0200
     1.3 @@ -312,9 +312,14 @@
     1.4  
     1.5  (**** Generation of contrapositives ****)
     1.6  
     1.7 +fun is_left (Const ("Trueprop", _) $ 
     1.8 +               (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
     1.9 +  | is_left _ = false;
    1.10 +               
    1.11  (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
    1.12 -fun assoc_right th = assoc_right (th RS disj_assoc)
    1.13 -	handle THM _ => th;
    1.14 +fun assoc_right th = 
    1.15 +  if is_left (prop_of th) then assoc_right (th RS disj_assoc)
    1.16 +  else th;
    1.17  
    1.18  (*Must check for negative literal first!*)
    1.19  val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
    1.20 @@ -349,18 +354,25 @@
    1.21      exists_Const
    1.22        (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
    1.23        
    1.24 -(*Raises an exception if any Vars in the theorem mention type bool; they
    1.25 -  could cause make_horn to loop! Also rejects functions whose arguments are 
    1.26 -  Booleans or other functions.*)
    1.27 +(*Raises an exception if any Vars in the theorem mention type bool. 
    1.28 +  Also rejects functions whose arguments are Booleans or other functions.*)
    1.29  fun is_fol_term t =
    1.30      not (exists (has_bool o fastype_of) (term_vars t)  orelse
    1.31  	 not (Term.is_first_order ["all","All","Ex"] t) orelse
    1.32  	 has_bool_arg_const t  orelse  
    1.33  	 has_meta_conn t);
    1.34  
    1.35 +fun rigid t = not (is_Var (head_of t));
    1.36 +
    1.37 +fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
    1.38 +  | ok4horn (Const ("Trueprop",_) $ t) = rigid t
    1.39 +  | ok4horn _ = false;
    1.40 +
    1.41  (*Create a meta-level Horn clause*)
    1.42 -fun make_horn crules th = make_horn crules (tryres(th,crules))
    1.43 -			  handle THM _ => th;
    1.44 +fun make_horn crules th = 
    1.45 +  if ok4horn (concl_of th) 
    1.46 +  then make_horn crules (tryres(th,crules)) handle THM _ => th
    1.47 +  else th;
    1.48  
    1.49  (*Generate Horn clauses for all contrapositives of a clause. The input, th,
    1.50    is a HOL disjunction.*)
    1.51 @@ -434,11 +446,18 @@
    1.52  val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
    1.53                 not_impD, not_iffD, not_allD, not_exD, not_notD];
    1.54  
    1.55 -fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
    1.56 +fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
    1.57 +  | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
    1.58 +  | ok4nnf _ = false;
    1.59 +
    1.60 +fun make_nnf1 th = 
    1.61 +  if ok4nnf (concl_of th) 
    1.62 +  then make_nnf1 (tryres(th, nnf_rls))
    1.63      handle THM _ =>
    1.64          forward_res make_nnf1
    1.65             (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
    1.66 -    handle THM _ => th;
    1.67 +    handle THM _ => th
    1.68 +  else th;
    1.69  
    1.70  (*The simplification removes defined quantifiers and occurrences of True and False. 
    1.71    nnf_ss also includes the one-point simprocs,
    1.72 @@ -455,7 +474,7 @@
    1.73  
    1.74  fun make_nnf th = case prems_of th of
    1.75      [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.76 -	     |> simplify nnf_ss  (*But this doesn't simplify premises...*)
    1.77 +	     |> simplify nnf_ss  
    1.78  	     |> make_nnf1
    1.79    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    1.80  
    1.81 @@ -587,10 +606,8 @@
    1.82  
    1.83  (*Converting one clause*)
    1.84  fun make_meta_clause th = 
    1.85 -  if is_fol_term (prop_of th) 
    1.86 -  then negated_asm_of_head (make_horn resolution_clause_rules th)
    1.87 -  else raise THM("make_meta_clause", 0, [th]);
    1.88 -
    1.89 +  negated_asm_of_head (make_horn resolution_clause_rules th);
    1.90 +  
    1.91  fun make_meta_clauses ths =
    1.92      name_thms "MClause#"
    1.93        (distinct Drule.eq_thm_prop (map make_meta_clause ths));