1.1 --- a/src/HOL/Tools/meson.ML	Sun Mar 25 15:15:07 2007 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Mon Mar 26 12:46:27 2007 +0200
     1.3 @@ -225,7 +225,7 @@
     1.4  fun too_many_clauses t = nclauses t >= !max_clauses;
     1.5  
     1.6  (*Replaces universally quantified variables by FREE variables -- because
     1.7 -  assumptions may not contain scheme variables.  Later, call "generalize". *)
     1.8 +  assumptions may not contain scheme variables.  Later, we call "generalize". *)
     1.9  fun freeze_spec th =
    1.10    let val newname = gensym "mes_"
    1.11        val spec' = read_instantiate [("x", newname)] spec
    1.12 @@ -233,7 +233,8 @@
    1.13  
    1.14  (*Used with METAHYPS below. There is one assumption, which gets bound to prem
    1.15    and then normalized via function nf. The normal form is given to resolve_tac,
    1.16 -  presumably to instantiate a Boolean variable.*)
    1.17 +  instantiate a Boolean variable created by resolution with disj_forward. Since
    1.18 +  (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
    1.19  fun resop nf [prem] = resolve_tac (nf prem) 1;
    1.20  
    1.21  (*Any need to extend this list with 
    1.22 @@ -245,7 +246,7 @@
    1.23    let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
    1.24          | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
    1.25    in  tryall rls  end;
    1.26 -  
    1.27 +
    1.28  (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
    1.29    Strips universal quantifiers and breaks up conjunctions.
    1.30    Eliminates existential quantifiers using skoths: Skolemization theorems.*)
    1.31 @@ -258,11 +259,13 @@
    1.32  	    Const ("op &", _) => (*conjunction*)
    1.33  		cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
    1.34  	  | Const ("All", _) => (*universal quantifier*)
    1.35 -	        cnf_aux (freeze_spec th,  ths)
    1.36 +	        cnf_aux (freeze_spec th, ths)
    1.37  	  | Const ("Ex", _) => 
    1.38  	      (*existential quantifier: Insert Skolem functions*)
    1.39  	      cnf_aux (apply_skolem_ths (th,skoths), ths)
    1.40 -	  | Const ("op |", _) => (*disjunction*)
    1.41 +	  | Const ("op |", _) => 
    1.42 +	      (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
    1.43 +	        all combinations of converting P, Q to CNF.*)
    1.44  	      let val tac =
    1.45  		  (METAHYPS (resop cnf_nil) 1) THEN
    1.46  		   (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
    1.47 @@ -275,9 +278,23 @@
    1.48      else cnf_aux (th,ths)
    1.49    end;
    1.50  
    1.51 +fun all_names (Const ("all", _) $ Abs(x,_,P)) = x :: all_names P
    1.52 +  | all_names _ = [];
    1.53 +
    1.54 +fun new_names n [] = []
    1.55 +  | new_names n (x::xs) = 
    1.56 +      if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs
    1.57 +      else new_names n xs;
    1.58 +
    1.59 +(*The gensym names are ugly, so don't let the user see them. When forall_elim_vars
    1.60 +  is called, it will ensure that no name clauses ensue.*)
    1.61 +fun nice_names th =
    1.62 +  let val old_names = all_names (prop_of th)
    1.63 +  in  Drule.rename_bvars (new_names 0 old_names) th  end;
    1.64 +
    1.65  (*Convert all suitable free variables to schematic variables, 
    1.66    but don't discharge assumptions.*)
    1.67 -fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th));
    1.68 +fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th)));
    1.69  
    1.70  fun make_cnf skoths th = cnf skoths (th, []);
    1.71