1.1 --- a/src/HOL/Tools/meson.ML	Fri Aug 25 18:46:24 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Aug 25 18:47:36 2006 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4  sig
     1.5    val size_of_subgoals	: thm -> int
     1.6    val make_cnf		: thm list -> thm -> thm list
     1.7 +  val finish_cnf	: thm list -> thm list
     1.8    val make_nnf		: thm -> thm
     1.9    val make_nnf1		: thm -> thm
    1.10    val skolemize		: thm -> thm
    1.11 @@ -36,7 +37,6 @@
    1.12    val select_literal	: int -> thm -> thm
    1.13    val skolemize_tac	: int -> tactic
    1.14    val make_clauses_tac	: int -> tactic
    1.15 -  val check_is_fol_term : term -> term
    1.16  end
    1.17  
    1.18  
    1.19 @@ -66,13 +66,29 @@
    1.20  
    1.21  (**** Operators for forward proof ****)
    1.22  
    1.23 -(*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
    1.24 -fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
    1.25 +
    1.26 +(** First-order Resolution **)
    1.27 +
    1.28 +fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
    1.29 +fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    1.30 +
    1.31 +val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
    1.32 +
    1.33 +(*FIXME: currently does not "rename variables apart"*)
    1.34 +fun first_order_resolve thA thB =
    1.35 +  let val thy = theory_of_thm thA
    1.36 +      val tmA = concl_of thA
    1.37 +      fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
    1.38 +      val Const("==>",_) $ tmB $ _ = prop_of thB
    1.39 +      val (tyenv,tenv) = match tmB
    1.40 +      val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.41 +  in  thA RS (cterm_instantiate ct_pairs thB)  end
    1.42 +  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
    1.43  
    1.44  (*raises exception if no rules apply -- unlike RL*)
    1.45  fun tryres (th, rls) = 
    1.46    let fun tryall [] = raise THM("tryres", 0, th::rls)
    1.47 -        | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls)
    1.48 +        | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
    1.49    in  tryall rls  end;
    1.50    
    1.51  (*Permits forward proof from rules that discharge assumptions*)
    1.52 @@ -189,6 +205,11 @@
    1.53  
    1.54  val has_meta_conn = 
    1.55      exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
    1.56 +
    1.57 +fun apply_skolem_ths (th, rls) = 
    1.58 +  let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
    1.59 +        | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
    1.60 +  in  tryall rls  end;
    1.61    
    1.62  (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    1.63    Strips universal quantifiers and breaks up conjunctions.
    1.64 @@ -200,13 +221,12 @@
    1.65  	then th::ths (*no work to do, terminate*)
    1.66  	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
    1.67  	    Const ("op &", _) => (*conjunction*)
    1.68 -		cnf_aux (th RS conjunct1,
    1.69 -			      cnf_aux (th RS conjunct2, ths))
    1.70 +		cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
    1.71  	  | Const ("All", _) => (*universal quantifier*)
    1.72  	        cnf_aux (freeze_spec th,  ths)
    1.73  	  | Const ("Ex", _) => 
    1.74  	      (*existential quantifier: Insert Skolem functions*)
    1.75 -	      cnf_aux (tryres (th,skoths), ths)
    1.76 +	      cnf_aux (apply_skolem_ths (th,skoths), ths)
    1.77  	  | Const ("op |", _) => (*disjunction*)
    1.78  	      let val tac =
    1.79  		  (METAHYPS (resop cnf_nil) 1) THEN
    1.80 @@ -224,9 +244,10 @@
    1.81    but don't discharge assumptions.*)
    1.82  fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
    1.83  
    1.84 -fun make_cnf skoths th = 
    1.85 -  filter (not o is_taut) 
    1.86 -    (map (refl_clause o generalize) (cnf skoths (th, [])));
    1.87 +fun make_cnf skoths th = cnf skoths (th, []);
    1.88 +
    1.89 +(*Generalization, removal of redundant equalities, removal of tautologies.*)
    1.90 +fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
    1.91  
    1.92  
    1.93  (**** Removal of duplicate literals ****)
    1.94 @@ -303,13 +324,6 @@
    1.95  	 has_bool_arg_const t  orelse  
    1.96  	 has_meta_conn t);
    1.97  
    1.98 -(*FIXME: replace this by the boolean-valued version above!*)
    1.99 -fun check_is_fol_term t =
   1.100 -    if is_fol_term t then t else raise TERM("check_is_fol_term",[t]);
   1.101 -
   1.102 -fun check_is_fol th = (check_is_fol_term (prop_of th); th);
   1.103 -
   1.104 -
   1.105  (*Create a meta-level Horn clause*)
   1.106  fun make_horn crules th = make_horn crules (tryres(th,crules))
   1.107  			  handle THM _ => th;
   1.108 @@ -426,7 +440,6 @@
   1.109  fun make_clauses ths =
   1.110      (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
   1.111  
   1.112 -
   1.113  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   1.114  fun make_horns ths =
   1.115      name_thms "Horn#"
   1.116 @@ -461,7 +474,7 @@
   1.117  		      EVERY1 [skolemize_prems_tac negs,
   1.118  			      METAHYPS (cltac o make_clauses)]) 1,
   1.119              expand_defs_tac]) i st
   1.120 -  handle TERM _ => no_tac st;	(*probably from check_is_fol*)		      
   1.121 +  handle THM _ => no_tac st;	(*probably from make_meta_clause, not first-order*)		      
   1.122  
   1.123  (** Best-first search versions **)
   1.124  
   1.125 @@ -531,7 +544,9 @@
   1.126  
   1.127  (*Converting one clause*)
   1.128  fun make_meta_clause th = 
   1.129 -    negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
   1.130 +  if is_fol_term (prop_of th) 
   1.131 +  then negated_asm_of_head (make_horn resolution_clause_rules th)
   1.132 +  else raise THM("make_meta_clause", 0, [th]);
   1.133  
   1.134  fun make_meta_clauses ths =
   1.135      name_thms "MClause#"