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