move MESON files together
authorblanchet
Mon Oct 04 21:37:42 2010 +0200 (2010-10-04)
changeset 399401f01c9b2b76b
parent 39939 6e9aff5ee9b5
child 39941 02fcd9cd1eac
move MESON files together
src/HOL/IsaMakefile
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Sledgehammer/meson_clausify.ML
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Oct 04 20:55:55 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Oct 04 21:37:42 2010 +0200
     1.3 @@ -201,6 +201,8 @@
     1.4    Tools/inductive_realizer.ML \
     1.5    Tools/inductive_set.ML \
     1.6    Tools/lin_arith.ML \
     1.7 +  Tools/Meson/meson.ML \
     1.8 +  Tools/Meson/meson_clausify.ML \
     1.9    Tools/nat_arith.ML \
    1.10    Tools/primrec.ML \
    1.11    Tools/prop_logic.ML \
    1.12 @@ -275,7 +277,6 @@
    1.13    Tools/int_arith.ML \
    1.14    Tools/groebner.ML \
    1.15    Tools/list_code.ML \
    1.16 -  Tools/meson.ML \
    1.17    Tools/nat_numeral_simprocs.ML \
    1.18    Tools/Nitpick/kodkod.ML \
    1.19    Tools/Nitpick/kodkod_sat.ML \
    1.20 @@ -315,7 +316,6 @@
    1.21    Tools/recdef.ML \
    1.22    Tools/record.ML \
    1.23    Tools/semiring_normalizer.ML \
    1.24 -  Tools/Sledgehammer/meson_clausify.ML \
    1.25    Tools/Sledgehammer/metis_reconstruct.ML \
    1.26    Tools/Sledgehammer/metis_translate.ML \
    1.27    Tools/Sledgehammer/metis_tactics.ML \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Oct 04 21:37:42 2010 +0200
     2.3 @@ -0,0 +1,712 @@
     2.4 +(*  Title:      HOL/Tools/meson.ML
     2.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.6 +
     2.7 +The MESON resolution proof procedure for HOL.
     2.8 +When making clauses, avoids using the rewriter -- instead uses RS recursively.
     2.9 +*)
    2.10 +
    2.11 +signature MESON =
    2.12 +sig
    2.13 +  val trace: bool Unsynchronized.ref
    2.14 +  val term_pair_of: indexname * (typ * 'a) -> term * 'a
    2.15 +  val size_of_subgoals: thm -> int
    2.16 +  val has_too_many_clauses: Proof.context -> term -> bool
    2.17 +  val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    2.18 +  val finish_cnf: thm list -> thm list
    2.19 +  val presimplify: thm -> thm
    2.20 +  val make_nnf: Proof.context -> thm -> thm
    2.21 +  val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm
    2.22 +  val skolemize : Proof.context -> thm -> thm
    2.23 +  val is_fol_term: theory -> term -> bool
    2.24 +  val make_clauses_unsorted: thm list -> thm list
    2.25 +  val make_clauses: thm list -> thm list
    2.26 +  val make_horns: thm list -> thm list
    2.27 +  val best_prolog_tac: (thm -> int) -> thm list -> tactic
    2.28 +  val depth_prolog_tac: thm list -> tactic
    2.29 +  val gocls: thm list -> thm list
    2.30 +  val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
    2.31 +  val MESON:
    2.32 +    tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
    2.33 +    -> int -> tactic
    2.34 +  val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
    2.35 +  val safe_best_meson_tac: Proof.context -> int -> tactic
    2.36 +  val depth_meson_tac: Proof.context -> int -> tactic
    2.37 +  val prolog_step_tac': thm list -> int -> tactic
    2.38 +  val iter_deepen_prolog_tac: thm list -> tactic
    2.39 +  val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
    2.40 +  val make_meta_clause: thm -> thm
    2.41 +  val make_meta_clauses: thm list -> thm list
    2.42 +  val meson_tac: Proof.context -> thm list -> int -> tactic
    2.43 +  val setup: theory -> theory
    2.44 +end
    2.45 +
    2.46 +structure Meson : MESON =
    2.47 +struct
    2.48 +
    2.49 +val trace = Unsynchronized.ref false;
    2.50 +fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    2.51 +
    2.52 +val max_clauses_default = 60;
    2.53 +val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default);
    2.54 +
    2.55 +(*No known example (on 1-5-2007) needs even thirty*)
    2.56 +val iter_deepen_limit = 50;
    2.57 +
    2.58 +val disj_forward = @{thm disj_forward};
    2.59 +val disj_forward2 = @{thm disj_forward2};
    2.60 +val make_pos_rule = @{thm make_pos_rule};
    2.61 +val make_pos_rule' = @{thm make_pos_rule'};
    2.62 +val make_pos_goal = @{thm make_pos_goal};
    2.63 +val make_neg_rule = @{thm make_neg_rule};
    2.64 +val make_neg_rule' = @{thm make_neg_rule'};
    2.65 +val make_neg_goal = @{thm make_neg_goal};
    2.66 +val conj_forward = @{thm conj_forward};
    2.67 +val all_forward = @{thm all_forward};
    2.68 +val ex_forward = @{thm ex_forward};
    2.69 +
    2.70 +val not_conjD = @{thm meson_not_conjD};
    2.71 +val not_disjD = @{thm meson_not_disjD};
    2.72 +val not_notD = @{thm meson_not_notD};
    2.73 +val not_allD = @{thm meson_not_allD};
    2.74 +val not_exD = @{thm meson_not_exD};
    2.75 +val imp_to_disjD = @{thm meson_imp_to_disjD};
    2.76 +val not_impD = @{thm meson_not_impD};
    2.77 +val iff_to_disjD = @{thm meson_iff_to_disjD};
    2.78 +val not_iffD = @{thm meson_not_iffD};
    2.79 +val conj_exD1 = @{thm meson_conj_exD1};
    2.80 +val conj_exD2 = @{thm meson_conj_exD2};
    2.81 +val disj_exD = @{thm meson_disj_exD};
    2.82 +val disj_exD1 = @{thm meson_disj_exD1};
    2.83 +val disj_exD2 = @{thm meson_disj_exD2};
    2.84 +val disj_assoc = @{thm meson_disj_assoc};
    2.85 +val disj_comm = @{thm meson_disj_comm};
    2.86 +val disj_FalseD1 = @{thm meson_disj_FalseD1};
    2.87 +val disj_FalseD2 = @{thm meson_disj_FalseD2};
    2.88 +
    2.89 +
    2.90 +(**** Operators for forward proof ****)
    2.91 +
    2.92 +
    2.93 +(** First-order Resolution **)
    2.94 +
    2.95 +fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    2.96 +
    2.97 +(*FIXME: currently does not "rename variables apart"*)
    2.98 +fun first_order_resolve thA thB =
    2.99 +  (case
   2.100 +    try (fn () =>
   2.101 +      let val thy = theory_of_thm thA
   2.102 +          val tmA = concl_of thA
   2.103 +          val Const("==>",_) $ tmB $ _ = prop_of thB
   2.104 +          val tenv =
   2.105 +            Pattern.first_order_match thy (tmB, tmA)
   2.106 +                                          (Vartab.empty, Vartab.empty) |> snd
   2.107 +          val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
   2.108 +      in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
   2.109 +    SOME th => th
   2.110 +  | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
   2.111 +
   2.112 +(* Applying "choice" swaps the bound variable names. We tweak
   2.113 +   "Thm.rename_boundvars"'s input to get the desired names. *)
   2.114 +fun fix_bounds (_ $ (Const (@{const_name Ex}, _)
   2.115 +                     $ Abs (_, _, Const (@{const_name All}, _) $ _)))
   2.116 +               (t0 $ (Const (@{const_name All}, T1)
   2.117 +                      $ Abs (a1, T1', Const (@{const_name Ex}, T2)
   2.118 +                                      $ Abs (a2, T2', t')))) =
   2.119 +    t0 $ (Const (@{const_name All}, T1)
   2.120 +          $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t')))
   2.121 +  | fix_bounds _ t = t
   2.122 +
   2.123 +(* Hack to make it less likely that we lose our precious bound variable names in
   2.124 +   "rename_bvs_RS" below, because of a clash. *)
   2.125 +val protect_prefix = "_"
   2.126 +
   2.127 +fun protect_bounds (t $ u) = protect_bounds t $ protect_bounds u
   2.128 +  | protect_bounds (Abs (s, T, t')) =
   2.129 +    Abs (protect_prefix ^ s, T, protect_bounds t')
   2.130 +  | protect_bounds t = t
   2.131 +
   2.132 +(* Forward proof while preserving bound variables names*)
   2.133 +fun rename_bvs_RS th rl =
   2.134 +  let
   2.135 +    val t = concl_of th
   2.136 +    val r = concl_of rl
   2.137 +    val th' = th RS Thm.rename_boundvars r (protect_bounds r) rl
   2.138 +    val t' = concl_of th'
   2.139 +  in Thm.rename_boundvars t' (fix_bounds t' t) th' end
   2.140 +
   2.141 +(*raises exception if no rules apply*)
   2.142 +fun tryres (th, rls) =
   2.143 +  let fun tryall [] = raise THM("tryres", 0, th::rls)
   2.144 +        | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
   2.145 +  in  tryall rls  end;
   2.146 +
   2.147 +(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
   2.148 +  e.g. from conj_forward, should have the form
   2.149 +    "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
   2.150 +  and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
   2.151 +fun forward_res ctxt nf st =
   2.152 +  let fun forward_tacf [prem] = rtac (nf prem) 1
   2.153 +        | forward_tacf prems =
   2.154 +            error (cat_lines
   2.155 +              ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
   2.156 +                Display.string_of_thm ctxt st ::
   2.157 +                "Premises:" :: map (Display.string_of_thm ctxt) prems))
   2.158 +  in
   2.159 +    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
   2.160 +    of SOME(th,_) => th
   2.161 +     | NONE => raise THM("forward_res", 0, [st])
   2.162 +  end;
   2.163 +
   2.164 +(*Are any of the logical connectives in "bs" present in the term?*)
   2.165 +fun has_conns bs =
   2.166 +  let fun has (Const _) = false
   2.167 +        | has (Const(@{const_name Trueprop},_) $ p) = has p
   2.168 +        | has (Const(@{const_name Not},_) $ p) = has p
   2.169 +        | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
   2.170 +        | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
   2.171 +        | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
   2.172 +        | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
   2.173 +        | has _ = false
   2.174 +  in  has  end;
   2.175 +
   2.176 +
   2.177 +(**** Clause handling ****)
   2.178 +
   2.179 +fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
   2.180 +  | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
   2.181 +  | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
   2.182 +  | literals P = [(true,P)];
   2.183 +
   2.184 +(*number of literals in a term*)
   2.185 +val nliterals = length o literals;
   2.186 +
   2.187 +
   2.188 +(*** Tautology Checking ***)
   2.189 +
   2.190 +fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
   2.191 +      signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   2.192 +  | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
   2.193 +  | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
   2.194 +
   2.195 +fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
   2.196 +
   2.197 +(*Literals like X=X are tautologous*)
   2.198 +fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
   2.199 +  | taut_poslit (Const(@{const_name True},_)) = true
   2.200 +  | taut_poslit _ = false;
   2.201 +
   2.202 +fun is_taut th =
   2.203 +  let val (poslits,neglits) = signed_lits th
   2.204 +  in  exists taut_poslit poslits
   2.205 +      orelse
   2.206 +      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
   2.207 +  end
   2.208 +  handle TERM _ => false;       (*probably dest_Trueprop on a weird theorem*)
   2.209 +
   2.210 +
   2.211 +(*** To remove trivial negated equality literals from clauses ***)
   2.212 +
   2.213 +(*They are typically functional reflexivity axioms and are the converses of
   2.214 +  injectivity equivalences*)
   2.215 +
   2.216 +val not_refl_disj_D = @{thm meson_not_refl_disj_D};
   2.217 +
   2.218 +(*Is either term a Var that does not properly occur in the other term?*)
   2.219 +fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
   2.220 +  | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
   2.221 +  | eliminable _ = false;
   2.222 +
   2.223 +fun refl_clause_aux 0 th = th
   2.224 +  | refl_clause_aux n th =
   2.225 +       case HOLogic.dest_Trueprop (concl_of th) of
   2.226 +          (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
   2.227 +            refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
   2.228 +        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
   2.229 +            if eliminable(t,u)
   2.230 +            then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
   2.231 +            else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
   2.232 +        | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   2.233 +        | _ => (*not a disjunction*) th;
   2.234 +
   2.235 +fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
   2.236 +      notequal_lits_count P + notequal_lits_count Q
   2.237 +  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
   2.238 +  | notequal_lits_count _ = 0;
   2.239 +
   2.240 +(*Simplify a clause by applying reflexivity to its negated equality literals*)
   2.241 +fun refl_clause th =
   2.242 +  let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
   2.243 +  in  zero_var_indexes (refl_clause_aux neqs th)  end
   2.244 +  handle TERM _ => th;  (*probably dest_Trueprop on a weird theorem*)
   2.245 +
   2.246 +
   2.247 +(*** Removal of duplicate literals ***)
   2.248 +
   2.249 +(*Forward proof, passing extra assumptions as theorems to the tactic*)
   2.250 +fun forward_res2 nf hyps st =
   2.251 +  case Seq.pull
   2.252 +        (REPEAT
   2.253 +         (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   2.254 +         st)
   2.255 +  of SOME(th,_) => th
   2.256 +   | NONE => raise THM("forward_res2", 0, [st]);
   2.257 +
   2.258 +(*Remove duplicates in P|Q by assuming ~P in Q
   2.259 +  rls (initially []) accumulates assumptions of the form P==>False*)
   2.260 +fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
   2.261 +    handle THM _ => tryres(th,rls)
   2.262 +    handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2),
   2.263 +                           [disj_FalseD1, disj_FalseD2, asm_rl])
   2.264 +    handle THM _ => th;
   2.265 +
   2.266 +(*Remove duplicate literals, if there are any*)
   2.267 +fun nodups ctxt th =
   2.268 +  if has_duplicates (op =) (literals (prop_of th))
   2.269 +    then nodups_aux ctxt [] th
   2.270 +    else th;
   2.271 +
   2.272 +
   2.273 +(*** The basic CNF transformation ***)
   2.274 +
   2.275 +fun estimated_num_clauses bound t =
   2.276 + let
   2.277 +  fun sum x y = if x < bound andalso y < bound then x+y else bound
   2.278 +  fun prod x y = if x < bound andalso y < bound then x*y else bound
   2.279 +  
   2.280 +  (*Estimate the number of clauses in order to detect infeasible theorems*)
   2.281 +  fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
   2.282 +    | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
   2.283 +    | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
   2.284 +        if b then sum (signed_nclauses b t) (signed_nclauses b u)
   2.285 +             else prod (signed_nclauses b t) (signed_nclauses b u)
   2.286 +    | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
   2.287 +        if b then prod (signed_nclauses b t) (signed_nclauses b u)
   2.288 +             else sum (signed_nclauses b t) (signed_nclauses b u)
   2.289 +    | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
   2.290 +        if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
   2.291 +             else sum (signed_nclauses (not b) t) (signed_nclauses b u)
   2.292 +    | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
   2.293 +        if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
   2.294 +            if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
   2.295 +                          (prod (signed_nclauses (not b) u) (signed_nclauses b t))
   2.296 +                 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
   2.297 +                          (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
   2.298 +        else 1
   2.299 +    | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
   2.300 +    | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
   2.301 +    | signed_nclauses _ _ = 1; (* literal *)
   2.302 + in signed_nclauses true t end
   2.303 +
   2.304 +fun has_too_many_clauses ctxt t =
   2.305 +  let val max_cl = Config.get ctxt max_clauses in
   2.306 +    estimated_num_clauses (max_cl + 1) t > max_cl
   2.307 +  end
   2.308 +
   2.309 +(*Replaces universally quantified variables by FREE variables -- because
   2.310 +  assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
   2.311 +local  
   2.312 +  val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
   2.313 +  val spec_varT = #T (Thm.rep_cterm spec_var);
   2.314 +  fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
   2.315 +in  
   2.316 +  fun freeze_spec th ctxt =
   2.317 +    let
   2.318 +      val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
   2.319 +      val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
   2.320 +      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
   2.321 +    in (th RS spec', ctxt') end
   2.322 +end;
   2.323 +
   2.324 +(*Used with METAHYPS below. There is one assumption, which gets bound to prem
   2.325 +  and then normalized via function nf. The normal form is given to resolve_tac,
   2.326 +  instantiate a Boolean variable created by resolution with disj_forward. Since
   2.327 +  (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
   2.328 +fun resop nf [prem] = resolve_tac (nf prem) 1;
   2.329 +
   2.330 +(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
   2.331 +   and "Pure.term"? *)
   2.332 +val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
   2.333 +
   2.334 +fun apply_skolem_theorem (th, rls) =
   2.335 +  let
   2.336 +    fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
   2.337 +      | tryall (rl :: rls) =
   2.338 +        first_order_resolve th rl handle THM _ => tryall rls
   2.339 +  in tryall rls end
   2.340 +
   2.341 +(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
   2.342 +   Strips universal quantifiers and breaks up conjunctions.
   2.343 +   Eliminates existential quantifiers using Skolemization theorems. *)
   2.344 +fun cnf old_skolem_ths ctxt (th, ths) =
   2.345 +  let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
   2.346 +      fun cnf_aux (th,ths) =
   2.347 +        if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   2.348 +        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
   2.349 +        then nodups ctxt th :: ths (*no work to do, terminate*)
   2.350 +        else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   2.351 +            Const (@{const_name HOL.conj}, _) => (*conjunction*)
   2.352 +                cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   2.353 +          | Const (@{const_name All}, _) => (*universal quantifier*)
   2.354 +                let val (th',ctxt') = freeze_spec th (!ctxtr)
   2.355 +                in  ctxtr := ctxt'; cnf_aux (th', ths) end
   2.356 +          | Const (@{const_name Ex}, _) =>
   2.357 +              (*existential quantifier: Insert Skolem functions*)
   2.358 +              cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
   2.359 +          | Const (@{const_name HOL.disj}, _) =>
   2.360 +              (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
   2.361 +                all combinations of converting P, Q to CNF.*)
   2.362 +              let val tac =
   2.363 +                  Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
   2.364 +                   (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
   2.365 +              in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
   2.366 +          | _ => nodups ctxt th :: ths  (*no work to do*)
   2.367 +      and cnf_nil th = cnf_aux (th,[])
   2.368 +      val cls =
   2.369 +            if has_too_many_clauses ctxt (concl_of th)
   2.370 +            then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
   2.371 +            else cnf_aux (th,ths)
   2.372 +  in  (cls, !ctxtr)  end;
   2.373 +
   2.374 +fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
   2.375 +
   2.376 +(*Generalization, removal of redundant equalities, removal of tautologies.*)
   2.377 +fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
   2.378 +
   2.379 +
   2.380 +(**** Generation of contrapositives ****)
   2.381 +
   2.382 +fun is_left (Const (@{const_name Trueprop}, _) $
   2.383 +               (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
   2.384 +  | is_left _ = false;
   2.385 +
   2.386 +(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   2.387 +fun assoc_right th =
   2.388 +  if is_left (prop_of th) then assoc_right (th RS disj_assoc)
   2.389 +  else th;
   2.390 +
   2.391 +(*Must check for negative literal first!*)
   2.392 +val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   2.393 +
   2.394 +(*For ordinary resolution. *)
   2.395 +val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   2.396 +
   2.397 +(*Create a goal or support clause, conclusing False*)
   2.398 +fun make_goal th =   (*Must check for negative literal first!*)
   2.399 +    make_goal (tryres(th, clause_rules))
   2.400 +  handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
   2.401 +
   2.402 +(*Sort clauses by number of literals*)
   2.403 +fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
   2.404 +
   2.405 +fun sort_clauses ths = sort (make_ord fewerlits) ths;
   2.406 +
   2.407 +fun has_bool @{typ bool} = true
   2.408 +  | has_bool (Type (_, Ts)) = exists has_bool Ts
   2.409 +  | has_bool _ = false
   2.410 +
   2.411 +fun has_fun (Type (@{type_name fun}, _)) = true
   2.412 +  | has_fun (Type (_, Ts)) = exists has_fun Ts
   2.413 +  | has_fun _ = false
   2.414 +
   2.415 +(*Is the string the name of a connective? Really only | and Not can remain,
   2.416 +  since this code expects to be called on a clause form.*)
   2.417 +val is_conn = member (op =)
   2.418 +    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
   2.419 +     @{const_name HOL.implies}, @{const_name Not},
   2.420 +     @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
   2.421 +
   2.422 +(*True if the term contains a function--not a logical connective--where the type
   2.423 +  of any argument contains bool.*)
   2.424 +val has_bool_arg_const =
   2.425 +    exists_Const
   2.426 +      (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
   2.427 +
   2.428 +(*A higher-order instance of a first-order constant? Example is the definition of
   2.429 +  one, 1, at a function type in theory Function_Algebras.*)
   2.430 +fun higher_inst_const thy (c,T) =
   2.431 +  case binder_types T of
   2.432 +      [] => false (*not a function type, OK*)
   2.433 +    | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
   2.434 +
   2.435 +(*Returns false if any Vars in the theorem mention type bool.
   2.436 +  Also rejects functions whose arguments are Booleans or other functions.*)
   2.437 +fun is_fol_term thy t =
   2.438 +    Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
   2.439 +    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
   2.440 +                           | _ => false) t orelse
   2.441 +         has_bool_arg_const t orelse
   2.442 +         exists_Const (higher_inst_const thy) t orelse
   2.443 +         has_meta_conn t);
   2.444 +
   2.445 +fun rigid t = not (is_Var (head_of t));
   2.446 +
   2.447 +fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
   2.448 +  | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
   2.449 +  | ok4horn _ = false;
   2.450 +
   2.451 +(*Create a meta-level Horn clause*)
   2.452 +fun make_horn crules th =
   2.453 +  if ok4horn (concl_of th)
   2.454 +  then make_horn crules (tryres(th,crules)) handle THM _ => th
   2.455 +  else th;
   2.456 +
   2.457 +(*Generate Horn clauses for all contrapositives of a clause. The input, th,
   2.458 +  is a HOL disjunction.*)
   2.459 +fun add_contras crules th hcs =
   2.460 +  let fun rots (0,_) = hcs
   2.461 +        | rots (k,th) = zero_var_indexes (make_horn crules th) ::
   2.462 +                        rots(k-1, assoc_right (th RS disj_comm))
   2.463 +  in case nliterals(prop_of th) of
   2.464 +        1 => th::hcs
   2.465 +      | n => rots(n, assoc_right th)
   2.466 +  end;
   2.467 +
   2.468 +(*Use "theorem naming" to label the clauses*)
   2.469 +fun name_thms label =
   2.470 +    let fun name1 th (k, ths) =
   2.471 +          (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
   2.472 +    in  fn ths => #2 (fold_rev name1 ths (length ths, []))  end;
   2.473 +
   2.474 +(*Is the given disjunction an all-negative support clause?*)
   2.475 +fun is_negative th = forall (not o #1) (literals (prop_of th));
   2.476 +
   2.477 +val neg_clauses = filter is_negative;
   2.478 +
   2.479 +
   2.480 +(***** MESON PROOF PROCEDURE *****)
   2.481 +
   2.482 +fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
   2.483 +           As) = rhyps(phi, A::As)
   2.484 +  | rhyps (_, As) = As;
   2.485 +
   2.486 +(** Detecting repeated assumptions in a subgoal **)
   2.487 +
   2.488 +(*The stringtree detects repeated assumptions.*)
   2.489 +fun ins_term t net = Net.insert_term (op aconv) (t, t) net;
   2.490 +
   2.491 +(*detects repetitions in a list of terms*)
   2.492 +fun has_reps [] = false
   2.493 +  | has_reps [_] = false
   2.494 +  | has_reps [t,u] = (t aconv u)
   2.495 +  | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true;
   2.496 +
   2.497 +(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   2.498 +fun TRYING_eq_assume_tac 0 st = Seq.single st
   2.499 +  | TRYING_eq_assume_tac i st =
   2.500 +       TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
   2.501 +       handle THM _ => TRYING_eq_assume_tac (i-1) st;
   2.502 +
   2.503 +fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
   2.504 +
   2.505 +(*Loop checking: FAIL if trying to prove the same thing twice
   2.506 +  -- if *ANY* subgoal has repeated literals*)
   2.507 +fun check_tac st =
   2.508 +  if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   2.509 +  then  Seq.empty  else  Seq.single st;
   2.510 +
   2.511 +
   2.512 +(* net_resolve_tac actually made it slower... *)
   2.513 +fun prolog_step_tac horns i =
   2.514 +    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   2.515 +    TRYALL_eq_assume_tac;
   2.516 +
   2.517 +(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   2.518 +fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
   2.519 +
   2.520 +fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
   2.521 +
   2.522 +
   2.523 +(*Negation Normal Form*)
   2.524 +val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   2.525 +               not_impD, not_iffD, not_allD, not_exD, not_notD];
   2.526 +
   2.527 +fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t
   2.528 +  | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t
   2.529 +  | ok4nnf _ = false;
   2.530 +
   2.531 +fun make_nnf1 ctxt th =
   2.532 +  if ok4nnf (concl_of th)
   2.533 +  then make_nnf1 ctxt (tryres(th, nnf_rls))
   2.534 +    handle THM ("tryres", _, _) =>
   2.535 +        forward_res ctxt (make_nnf1 ctxt)
   2.536 +           (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   2.537 +    handle THM ("tryres", _, _) => th
   2.538 +  else th
   2.539 +
   2.540 +(*The simplification removes defined quantifiers and occurrences of True and False.
   2.541 +  nnf_ss also includes the one-point simprocs,
   2.542 +  which are needed to avoid the various one-point theorems from generating junk clauses.*)
   2.543 +val nnf_simps =
   2.544 +  @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
   2.545 +         if_eq_cancel cases_simp}
   2.546 +val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
   2.547 +
   2.548 +val nnf_ss =
   2.549 +  HOL_basic_ss addsimps nnf_extra_simps
   2.550 +    addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
   2.551 +
   2.552 +val presimplify =
   2.553 +  rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss
   2.554 +
   2.555 +fun make_nnf ctxt th = case prems_of th of
   2.556 +    [] => th |> presimplify |> make_nnf1 ctxt
   2.557 +  | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   2.558 +
   2.559 +(* Pull existential quantifiers to front. This accomplishes Skolemization for
   2.560 +   clauses that arise from a subgoal. *)
   2.561 +fun skolemize_with_choice_thms ctxt choice_ths =
   2.562 +  let
   2.563 +    fun aux th =
   2.564 +      if not (has_conns [@{const_name Ex}] (prop_of th)) then
   2.565 +        th
   2.566 +      else
   2.567 +        tryres (th, choice_ths @
   2.568 +                    [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2])
   2.569 +        |> aux
   2.570 +        handle THM ("tryres", _, _) =>
   2.571 +               tryres (th, [conj_forward, disj_forward, all_forward])
   2.572 +               |> forward_res ctxt aux
   2.573 +               |> aux
   2.574 +               handle THM ("tryres", _, _) =>
   2.575 +                      rename_bvs_RS th ex_forward
   2.576 +                      |> forward_res ctxt aux
   2.577 +  in aux o make_nnf ctxt end
   2.578 +
   2.579 +fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt)
   2.580 +
   2.581 +(* "RS" can fail if "unify_search_bound" is too small. *)
   2.582 +fun try_skolemize ctxt th =
   2.583 +  try (skolemize ctxt) th
   2.584 +  |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^
   2.585 +                                         Display.string_of_thm ctxt th)
   2.586 +           | _ => ())
   2.587 +
   2.588 +fun add_clauses th cls =
   2.589 +  let val ctxt0 = Variable.global_thm_context th
   2.590 +      val (cnfs, ctxt) = make_cnf [] th ctxt0
   2.591 +  in Variable.export ctxt ctxt0 cnfs @ cls end;
   2.592 +
   2.593 +(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   2.594 +  The resulting clauses are HOL disjunctions.*)
   2.595 +fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
   2.596 +val make_clauses = sort_clauses o make_clauses_unsorted;
   2.597 +
   2.598 +(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   2.599 +fun make_horns ths =
   2.600 +    name_thms "Horn#"
   2.601 +      (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
   2.602 +
   2.603 +(*Could simply use nprems_of, which would count remaining subgoals -- no
   2.604 +  discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   2.605 +
   2.606 +fun best_prolog_tac sizef horns =
   2.607 +    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   2.608 +
   2.609 +fun depth_prolog_tac horns =
   2.610 +    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   2.611 +
   2.612 +(*Return all negative clauses, as possible goal clauses*)
   2.613 +fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   2.614 +
   2.615 +fun skolemize_prems_tac ctxt prems =
   2.616 +  cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE
   2.617 +
   2.618 +(*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   2.619 +  Function mkcl converts theorems to clauses.*)
   2.620 +fun MESON preskolem_tac mkcl cltac ctxt i st =
   2.621 +  SELECT_GOAL
   2.622 +    (EVERY [Object_Logic.atomize_prems_tac 1,
   2.623 +            rtac ccontr 1,
   2.624 +            preskolem_tac,
   2.625 +            Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
   2.626 +                      EVERY1 [skolemize_prems_tac ctxt negs,
   2.627 +                              Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   2.628 +  handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
   2.629 +
   2.630 +
   2.631 +(** Best-first search versions **)
   2.632 +
   2.633 +(*ths is a list of additional clauses (HOL disjunctions) to use.*)
   2.634 +fun best_meson_tac sizef =
   2.635 +  MESON all_tac make_clauses
   2.636 +    (fn cls =>
   2.637 +         THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   2.638 +                         (has_fewer_prems 1, sizef)
   2.639 +                         (prolog_step_tac (make_horns cls) 1));
   2.640 +
   2.641 +(*First, breaks the goal into independent units*)
   2.642 +fun safe_best_meson_tac ctxt =
   2.643 +     SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
   2.644 +                  TRYALL (best_meson_tac size_of_subgoals ctxt));
   2.645 +
   2.646 +(** Depth-first search version **)
   2.647 +
   2.648 +val depth_meson_tac =
   2.649 +  MESON all_tac make_clauses
   2.650 +    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
   2.651 +
   2.652 +
   2.653 +(** Iterative deepening version **)
   2.654 +
   2.655 +(*This version does only one inference per call;
   2.656 +  having only one eq_assume_tac speeds it up!*)
   2.657 +fun prolog_step_tac' horns =
   2.658 +    let val (horn0s, _) = (*0 subgoals vs 1 or more*)
   2.659 +            take_prefix Thm.no_prems horns
   2.660 +        val nrtac = net_resolve_tac horns
   2.661 +    in  fn i => eq_assume_tac i ORELSE
   2.662 +                match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   2.663 +                ((assume_tac i APPEND nrtac i) THEN check_tac)
   2.664 +    end;
   2.665 +
   2.666 +fun iter_deepen_prolog_tac horns =
   2.667 +    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
   2.668 +
   2.669 +fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses
   2.670 +  (fn cls =>
   2.671 +    (case (gocls (cls @ ths)) of
   2.672 +      [] => no_tac  (*no goal clauses*)
   2.673 +    | goes =>
   2.674 +        let
   2.675 +          val horns = make_horns (cls @ ths)
   2.676 +          val _ = trace_msg (fn () =>
   2.677 +            cat_lines ("meson method called:" ::
   2.678 +              map (Display.string_of_thm ctxt) (cls @ ths) @
   2.679 +              ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
   2.680 +        in
   2.681 +          THEN_ITER_DEEPEN iter_deepen_limit
   2.682 +            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
   2.683 +        end));
   2.684 +
   2.685 +fun meson_tac ctxt ths =
   2.686 +  SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
   2.687 +
   2.688 +
   2.689 +(**** Code to support ordinary resolution, rather than Model Elimination ****)
   2.690 +
   2.691 +(*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
   2.692 +  with no contrapositives, for ordinary resolution.*)
   2.693 +
   2.694 +(*Rules to convert the head literal into a negated assumption. If the head
   2.695 +  literal is already negated, then using notEfalse instead of notEfalse'
   2.696 +  prevents a double negation.*)
   2.697 +val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
   2.698 +val notEfalse' = rotate_prems 1 notEfalse;
   2.699 +
   2.700 +fun negated_asm_of_head th =
   2.701 +    th RS notEfalse handle THM _ => th RS notEfalse';
   2.702 +
   2.703 +(*Converting one theorem from a disjunction to a meta-level clause*)
   2.704 +fun make_meta_clause th =
   2.705 +  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
   2.706 +  in  
   2.707 +      (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
   2.708 +       negated_asm_of_head o make_horn resolution_clause_rules) fth
   2.709 +  end;
   2.710 +
   2.711 +fun make_meta_clauses ths =
   2.712 +    name_thms "MClause#"
   2.713 +      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
   2.714 +
   2.715 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Mon Oct 04 21:37:42 2010 +0200
     3.3 @@ -0,0 +1,376 @@
     3.4 +(*  Title:      HOL/Tools/Sledgehammer/meson_clausify.ML
     3.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3.6 +    Author:     Jasmin Blanchette, TU Muenchen
     3.7 +
     3.8 +Transformation of axiom rules (elim/intro/etc) into CNF forms.
     3.9 +*)
    3.10 +
    3.11 +signature MESON_CLAUSIFY =
    3.12 +sig
    3.13 +  val new_skolem_var_prefix : string
    3.14 +  val extensionalize_theorem : thm -> thm
    3.15 +  val introduce_combinators_in_cterm : cterm -> thm
    3.16 +  val introduce_combinators_in_theorem : thm -> thm
    3.17 +  val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
    3.18 +  val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    3.19 +  val cnf_axiom :
    3.20 +    Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
    3.21 +  val meson_general_tac : Proof.context -> thm list -> int -> tactic
    3.22 +  val setup: theory -> theory
    3.23 +end;
    3.24 +
    3.25 +structure Meson_Clausify : MESON_CLAUSIFY =
    3.26 +struct
    3.27 +
    3.28 +(* the extra "?" helps prevent clashes *)
    3.29 +val new_skolem_var_prefix = "?SK"
    3.30 +val new_nonskolem_var_prefix = "?V"
    3.31 +
    3.32 +(**** Transformation of Elimination Rules into First-Order Formulas****)
    3.33 +
    3.34 +val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    3.35 +val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
    3.36 +
    3.37 +(* Converts an elim-rule into an equivalent theorem that does not have the
    3.38 +   predicate variable. Leaves other theorems unchanged. We simply instantiate
    3.39 +   the conclusion variable to False. (Cf. "transform_elim_term" in
    3.40 +   "Sledgehammer_Util".) *)
    3.41 +fun transform_elim_theorem th =
    3.42 +  case concl_of th of    (*conclusion variable*)
    3.43 +       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    3.44 +           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    3.45 +    | v as Var(_, @{typ prop}) =>
    3.46 +           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    3.47 +    | _ => th
    3.48 +
    3.49 +
    3.50 +(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    3.51 +
    3.52 +fun mk_old_skolem_term_wrapper t =
    3.53 +  let val T = fastype_of t in
    3.54 +    Const (@{const_name skolem}, T --> T) $ t
    3.55 +  end
    3.56 +
    3.57 +fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
    3.58 +  | beta_eta_in_abs_body t = Envir.beta_eta_contract t
    3.59 +
    3.60 +(*Traverse a theorem, accumulating Skolem function definitions.*)
    3.61 +fun old_skolem_defs th =
    3.62 +  let
    3.63 +    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
    3.64 +        (*Existential: declare a Skolem function, then insert into body and continue*)
    3.65 +        let
    3.66 +          val args = OldTerm.term_frees body
    3.67 +          (* Forms a lambda-abstraction over the formal parameters *)
    3.68 +          val rhs =
    3.69 +            list_abs_free (map dest_Free args,
    3.70 +                           HOLogic.choice_const T $ beta_eta_in_abs_body body)
    3.71 +            |> mk_old_skolem_term_wrapper
    3.72 +          val comb = list_comb (rhs, args)
    3.73 +        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    3.74 +      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    3.75 +        (*Universal quant: insert a free variable into body and continue*)
    3.76 +        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    3.77 +        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
    3.78 +      | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    3.79 +      | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    3.80 +      | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
    3.81 +      | dec_sko _ rhss = rhss
    3.82 +  in  dec_sko (prop_of th) []  end;
    3.83 +
    3.84 +
    3.85 +(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    3.86 +
    3.87 +val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
    3.88 +
    3.89 +(* Removes the lambdas from an equation of the form "t = (%x. u)".
    3.90 +   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
    3.91 +fun extensionalize_theorem th =
    3.92 +  case prop_of th of
    3.93 +    _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
    3.94 +         $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
    3.95 +  | _ => th
    3.96 +
    3.97 +fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
    3.98 +  | is_quasi_lambda_free (t1 $ t2) =
    3.99 +    is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   3.100 +  | is_quasi_lambda_free (Abs _) = false
   3.101 +  | is_quasi_lambda_free _ = true
   3.102 +
   3.103 +val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
   3.104 +val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
   3.105 +val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
   3.106 +
   3.107 +(* FIXME: Requires more use of cterm constructors. *)
   3.108 +fun abstract ct =
   3.109 +  let
   3.110 +      val thy = theory_of_cterm ct
   3.111 +      val Abs(x,_,body) = term_of ct
   3.112 +      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
   3.113 +      val cxT = ctyp_of thy xT
   3.114 +      val cbodyT = ctyp_of thy bodyT
   3.115 +      fun makeK () =
   3.116 +        instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
   3.117 +                     @{thm abs_K}
   3.118 +  in
   3.119 +      case body of
   3.120 +          Const _ => makeK()
   3.121 +        | Free _ => makeK()
   3.122 +        | Var _ => makeK()  (*though Var isn't expected*)
   3.123 +        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   3.124 +        | rator$rand =>
   3.125 +            if loose_bvar1 (rator,0) then (*C or S*)
   3.126 +               if loose_bvar1 (rand,0) then (*S*)
   3.127 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
   3.128 +                     val crand = cterm_of thy (Abs(x,xT,rand))
   3.129 +                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
   3.130 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
   3.131 +                 in
   3.132 +                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
   3.133 +                 end
   3.134 +               else (*C*)
   3.135 +                 let val crator = cterm_of thy (Abs(x,xT,rator))
   3.136 +                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
   3.137 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
   3.138 +                 in
   3.139 +                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
   3.140 +                 end
   3.141 +            else if loose_bvar1 (rand,0) then (*B or eta*)
   3.142 +               if rand = Bound 0 then Thm.eta_conversion ct
   3.143 +               else (*B*)
   3.144 +                 let val crand = cterm_of thy (Abs(x,xT,rand))
   3.145 +                     val crator = cterm_of thy rator
   3.146 +                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
   3.147 +                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
   3.148 +                 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
   3.149 +            else makeK()
   3.150 +        | _ => raise Fail "abstract: Bad term"
   3.151 +  end;
   3.152 +
   3.153 +(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
   3.154 +fun introduce_combinators_in_cterm ct =
   3.155 +  if is_quasi_lambda_free (term_of ct) then
   3.156 +    Thm.reflexive ct
   3.157 +  else case term_of ct of
   3.158 +    Abs _ =>
   3.159 +    let
   3.160 +      val (cv, cta) = Thm.dest_abs NONE ct
   3.161 +      val (v, _) = dest_Free (term_of cv)
   3.162 +      val u_th = introduce_combinators_in_cterm cta
   3.163 +      val cu = Thm.rhs_of u_th
   3.164 +      val comb_eq = abstract (Thm.cabs cv cu)
   3.165 +    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   3.166 +  | _ $ _ =>
   3.167 +    let val (ct1, ct2) = Thm.dest_comb ct in
   3.168 +        Thm.combination (introduce_combinators_in_cterm ct1)
   3.169 +                        (introduce_combinators_in_cterm ct2)
   3.170 +    end
   3.171 +
   3.172 +fun introduce_combinators_in_theorem th =
   3.173 +  if is_quasi_lambda_free (prop_of th) then
   3.174 +    th
   3.175 +  else
   3.176 +    let
   3.177 +      val th = Drule.eta_contraction_rule th
   3.178 +      val eqth = introduce_combinators_in_cterm (cprop_of th)
   3.179 +    in Thm.equal_elim eqth th end
   3.180 +    handle THM (msg, _, _) =>
   3.181 +           (warning ("Error in the combinator translation of " ^
   3.182 +                     Display.string_of_thm_without_context th ^
   3.183 +                     "\nException message: " ^ msg ^ ".");
   3.184 +            (* A type variable of sort "{}" will make abstraction fail. *)
   3.185 +            TrueI)
   3.186 +
   3.187 +(*cterms are used throughout for efficiency*)
   3.188 +val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
   3.189 +
   3.190 +(*Given an abstraction over n variables, replace the bound variables by free
   3.191 +  ones. Return the body, along with the list of free variables.*)
   3.192 +fun c_variant_abs_multi (ct0, vars) =
   3.193 +      let val (cv,ct) = Thm.dest_abs NONE ct0
   3.194 +      in  c_variant_abs_multi (ct, cv::vars)  end
   3.195 +      handle CTERM _ => (ct0, rev vars);
   3.196 +
   3.197 +val skolem_def_raw = @{thms skolem_def_raw}
   3.198 +
   3.199 +(* Given the definition of a Skolem function, return a theorem to replace
   3.200 +   an existential formula by a use of that function.
   3.201 +   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   3.202 +fun old_skolem_theorem_from_def thy rhs0 =
   3.203 +  let
   3.204 +    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
   3.205 +    val rhs' = rhs |> Thm.dest_comb |> snd
   3.206 +    val (ch, frees) = c_variant_abs_multi (rhs', [])
   3.207 +    val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
   3.208 +    val T =
   3.209 +      case hilbert of
   3.210 +        Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
   3.211 +      | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
   3.212 +                         [hilbert])
   3.213 +    val cex = cterm_of thy (HOLogic.exists_const T)
   3.214 +    val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
   3.215 +    val conc =
   3.216 +      Drule.list_comb (rhs, frees)
   3.217 +      |> Drule.beta_conv cabs |> Thm.capply cTrueprop
   3.218 +    fun tacf [prem] =
   3.219 +      rewrite_goals_tac skolem_def_raw
   3.220 +      THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
   3.221 +  in
   3.222 +    Goal.prove_internal [ex_tm] conc tacf
   3.223 +    |> forall_intr_list frees
   3.224 +    |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   3.225 +    |> Thm.varifyT_global
   3.226 +  end
   3.227 +
   3.228 +fun to_definitional_cnf_with_quantifiers thy th =
   3.229 +  let
   3.230 +    val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
   3.231 +    val eqth = eqth RS @{thm eq_reflection}
   3.232 +    val eqth = eqth RS @{thm TruepropI}
   3.233 +  in Thm.equal_elim eqth th end
   3.234 +
   3.235 +fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
   3.236 +  (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
   3.237 +  "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
   3.238 +  string_of_int index_no ^ "_" ^ s
   3.239 +
   3.240 +fun cluster_of_zapped_var_name s =
   3.241 +  let val get_int = the o Int.fromString o nth (space_explode "_" s) in
   3.242 +    ((get_int 1, (get_int 2, get_int 3)),
   3.243 +     String.isPrefix new_skolem_var_prefix s)
   3.244 +  end
   3.245 +
   3.246 +fun zap (cluster as (cluster_no, cluster_skolem)) index_no pos ct =
   3.247 +  ct
   3.248 +  |> (case term_of ct of
   3.249 +        Const (s, _) $ Abs (s', _, _) =>
   3.250 +        if s = @{const_name all} orelse s = @{const_name All} orelse
   3.251 +           s = @{const_name Ex} then
   3.252 +          let
   3.253 +            val skolem = (pos = (s = @{const_name Ex}))
   3.254 +            val (cluster, index_no) =
   3.255 +              if skolem = cluster_skolem then (cluster, index_no)
   3.256 +              else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
   3.257 +          in
   3.258 +            Thm.dest_comb #> snd
   3.259 +            #> Thm.dest_abs (SOME (zapped_var_name cluster index_no s'))
   3.260 +            #> snd #> zap cluster (index_no + 1) pos
   3.261 +          end
   3.262 +        else
   3.263 +          Conv.all_conv
   3.264 +      | Const (s, _) $ _ $ _ =>
   3.265 +        if s = @{const_name "==>"} orelse s = @{const_name implies} then
   3.266 +          Conv.combination_conv (Conv.arg_conv (zap cluster index_no (not pos)))
   3.267 +                                (zap cluster index_no pos)
   3.268 +        else if s = @{const_name conj} orelse s = @{const_name disj} then
   3.269 +          Conv.combination_conv (Conv.arg_conv (zap cluster index_no pos))
   3.270 +                                (zap cluster index_no pos)
   3.271 +        else
   3.272 +          Conv.all_conv
   3.273 +      | Const (s, _) $ _ =>
   3.274 +        if s = @{const_name Trueprop} then
   3.275 +          Conv.arg_conv (zap cluster index_no pos)
   3.276 +        else if s = @{const_name Not} then
   3.277 +          Conv.arg_conv (zap cluster index_no (not pos))
   3.278 +        else
   3.279 +          Conv.all_conv
   3.280 +      | _ => Conv.all_conv)
   3.281 +
   3.282 +fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
   3.283 +
   3.284 +val no_choice =
   3.285 +  @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
   3.286 +  |> Logic.varify_global
   3.287 +  |> Skip_Proof.make_thm @{theory}
   3.288 +
   3.289 +(* Converts an Isabelle theorem into NNF. *)
   3.290 +fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt =
   3.291 +  let
   3.292 +    val thy = ProofContext.theory_of ctxt
   3.293 +    val th =
   3.294 +      th |> transform_elim_theorem
   3.295 +         |> zero_var_indexes
   3.296 +         |> new_skolemizer ? forall_intr_vars
   3.297 +    val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
   3.298 +    val th = th |> Conv.fconv_rule Object_Logic.atomize
   3.299 +                |> extensionalize_theorem
   3.300 +                |> Meson.make_nnf ctxt
   3.301 +  in
   3.302 +    if new_skolemizer then
   3.303 +      let
   3.304 +        fun skolemize choice_ths =
   3.305 +          Meson.skolemize_with_choice_thms ctxt choice_ths
   3.306 +          #> simplify (ss_only @{thms all_simps[symmetric]})
   3.307 +        val pull_out =
   3.308 +          simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
   3.309 +        val (discharger_th, fully_skolemized_th) =
   3.310 +          if null choice_ths then
   3.311 +            th |> `I |>> pull_out ||> skolemize [no_choice]
   3.312 +          else
   3.313 +            th |> skolemize choice_ths |> `I
   3.314 +        val t =
   3.315 +          fully_skolemized_th |> cprop_of
   3.316 +          |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context
   3.317 +          |> cprop_of |> Thm.dest_equals |> snd |> term_of
   3.318 +      in
   3.319 +        if exists_subterm (fn Var ((s, _), _) =>
   3.320 +                              String.isPrefix new_skolem_var_prefix s
   3.321 +                            | _ => false) t then
   3.322 +          let
   3.323 +            val (ct, ctxt) =
   3.324 +              Variable.import_terms true [t] ctxt
   3.325 +              |>> the_single |>> cterm_of thy
   3.326 +          in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end
   3.327 +       else
   3.328 +         (NONE, th, ctxt)
   3.329 +      end
   3.330 +    else
   3.331 +      (NONE, th, ctxt)
   3.332 +  end
   3.333 +
   3.334 +(* Convert a theorem to CNF, with additional premises due to skolemization. *)
   3.335 +fun cnf_axiom ctxt0 new_skolemizer ax_no th =
   3.336 +  let
   3.337 +    val thy = ProofContext.theory_of ctxt0
   3.338 +    val choice_ths = Meson_Choices.get ctxt0
   3.339 +    val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
   3.340 +    fun clausify th =
   3.341 +      Meson.make_cnf (if new_skolemizer then
   3.342 +                        []
   3.343 +                      else
   3.344 +                        map (old_skolem_theorem_from_def thy)
   3.345 +                            (old_skolem_defs th)) th ctxt
   3.346 +    val (cnf_ths, ctxt) =
   3.347 +      clausify nnf_th
   3.348 +      |> (fn ([], _) =>
   3.349 +             clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
   3.350 +           | p => p)
   3.351 +    fun intr_imp ct th =
   3.352 +      Thm.instantiate ([], map (pairself (cterm_of @{theory}))
   3.353 +                               [(Var (("i", 1), @{typ nat}),
   3.354 +                                 HOLogic.mk_nat ax_no)])
   3.355 +                      @{thm skolem_COMBK_D}
   3.356 +      RS Thm.implies_intr ct th
   3.357 +  in
   3.358 +    (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
   3.359 +                        ##> (term_of #> HOLogic.dest_Trueprop
   3.360 +                             #> singleton (Variable.export_terms ctxt ctxt0))),
   3.361 +     cnf_ths |> map (introduce_combinators_in_theorem
   3.362 +                     #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
   3.363 +             |> Variable.export ctxt ctxt0
   3.364 +             |> Meson.finish_cnf
   3.365 +             |> map Thm.close_derivation)
   3.366 +  end
   3.367 +  handle THM _ => (NONE, [])
   3.368 +
   3.369 +fun meson_general_tac ctxt ths =
   3.370 +  let val ctxt = Classical.put_claset HOL_cs ctxt in
   3.371 +    Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
   3.372 +  end
   3.373 +
   3.374 +val setup =
   3.375 +  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
   3.376 +     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
   3.377 +     "MESON resolution proof procedure"
   3.378 +
   3.379 +end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Mon Oct 04 20:55:55 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,376 +0,0 @@
     4.4 -(*  Title:      HOL/Tools/Sledgehammer/meson_clausify.ML
     4.5 -    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4.6 -    Author:     Jasmin Blanchette, TU Muenchen
     4.7 -
     4.8 -Transformation of axiom rules (elim/intro/etc) into CNF forms.
     4.9 -*)
    4.10 -
    4.11 -signature MESON_CLAUSIFY =
    4.12 -sig
    4.13 -  val new_skolem_var_prefix : string
    4.14 -  val extensionalize_theorem : thm -> thm
    4.15 -  val introduce_combinators_in_cterm : cterm -> thm
    4.16 -  val introduce_combinators_in_theorem : thm -> thm
    4.17 -  val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
    4.18 -  val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    4.19 -  val cnf_axiom :
    4.20 -    Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
    4.21 -  val meson_general_tac : Proof.context -> thm list -> int -> tactic
    4.22 -  val setup: theory -> theory
    4.23 -end;
    4.24 -
    4.25 -structure Meson_Clausify : MESON_CLAUSIFY =
    4.26 -struct
    4.27 -
    4.28 -(* the extra "?" helps prevent clashes *)
    4.29 -val new_skolem_var_prefix = "?SK"
    4.30 -val new_nonskolem_var_prefix = "?V"
    4.31 -
    4.32 -(**** Transformation of Elimination Rules into First-Order Formulas****)
    4.33 -
    4.34 -val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    4.35 -val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
    4.36 -
    4.37 -(* Converts an elim-rule into an equivalent theorem that does not have the
    4.38 -   predicate variable. Leaves other theorems unchanged. We simply instantiate
    4.39 -   the conclusion variable to False. (Cf. "transform_elim_term" in
    4.40 -   "Sledgehammer_Util".) *)
    4.41 -fun transform_elim_theorem th =
    4.42 -  case concl_of th of    (*conclusion variable*)
    4.43 -       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    4.44 -           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    4.45 -    | v as Var(_, @{typ prop}) =>
    4.46 -           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    4.47 -    | _ => th
    4.48 -
    4.49 -
    4.50 -(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    4.51 -
    4.52 -fun mk_old_skolem_term_wrapper t =
    4.53 -  let val T = fastype_of t in
    4.54 -    Const (@{const_name skolem}, T --> T) $ t
    4.55 -  end
    4.56 -
    4.57 -fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
    4.58 -  | beta_eta_in_abs_body t = Envir.beta_eta_contract t
    4.59 -
    4.60 -(*Traverse a theorem, accumulating Skolem function definitions.*)
    4.61 -fun old_skolem_defs th =
    4.62 -  let
    4.63 -    fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
    4.64 -        (*Existential: declare a Skolem function, then insert into body and continue*)
    4.65 -        let
    4.66 -          val args = OldTerm.term_frees body
    4.67 -          (* Forms a lambda-abstraction over the formal parameters *)
    4.68 -          val rhs =
    4.69 -            list_abs_free (map dest_Free args,
    4.70 -                           HOLogic.choice_const T $ beta_eta_in_abs_body body)
    4.71 -            |> mk_old_skolem_term_wrapper
    4.72 -          val comb = list_comb (rhs, args)
    4.73 -        in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    4.74 -      | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    4.75 -        (*Universal quant: insert a free variable into body and continue*)
    4.76 -        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    4.77 -        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
    4.78 -      | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    4.79 -      | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    4.80 -      | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
    4.81 -      | dec_sko _ rhss = rhss
    4.82 -  in  dec_sko (prop_of th) []  end;
    4.83 -
    4.84 -
    4.85 -(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    4.86 -
    4.87 -val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
    4.88 -
    4.89 -(* Removes the lambdas from an equation of the form "t = (%x. u)".
    4.90 -   (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
    4.91 -fun extensionalize_theorem th =
    4.92 -  case prop_of th of
    4.93 -    _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
    4.94 -         $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
    4.95 -  | _ => th
    4.96 -
    4.97 -fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
    4.98 -  | is_quasi_lambda_free (t1 $ t2) =
    4.99 -    is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   4.100 -  | is_quasi_lambda_free (Abs _) = false
   4.101 -  | is_quasi_lambda_free _ = true
   4.102 -
   4.103 -val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
   4.104 -val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
   4.105 -val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
   4.106 -
   4.107 -(* FIXME: Requires more use of cterm constructors. *)
   4.108 -fun abstract ct =
   4.109 -  let
   4.110 -      val thy = theory_of_cterm ct
   4.111 -      val Abs(x,_,body) = term_of ct
   4.112 -      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
   4.113 -      val cxT = ctyp_of thy xT
   4.114 -      val cbodyT = ctyp_of thy bodyT
   4.115 -      fun makeK () =
   4.116 -        instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
   4.117 -                     @{thm abs_K}
   4.118 -  in
   4.119 -      case body of
   4.120 -          Const _ => makeK()
   4.121 -        | Free _ => makeK()
   4.122 -        | Var _ => makeK()  (*though Var isn't expected*)
   4.123 -        | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   4.124 -        | rator$rand =>
   4.125 -            if loose_bvar1 (rator,0) then (*C or S*)
   4.126 -               if loose_bvar1 (rand,0) then (*S*)
   4.127 -                 let val crator = cterm_of thy (Abs(x,xT,rator))
   4.128 -                     val crand = cterm_of thy (Abs(x,xT,rand))
   4.129 -                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
   4.130 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
   4.131 -                 in
   4.132 -                   Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
   4.133 -                 end
   4.134 -               else (*C*)
   4.135 -                 let val crator = cterm_of thy (Abs(x,xT,rator))
   4.136 -                     val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
   4.137 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
   4.138 -                 in
   4.139 -                   Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
   4.140 -                 end
   4.141 -            else if loose_bvar1 (rand,0) then (*B or eta*)
   4.142 -               if rand = Bound 0 then Thm.eta_conversion ct
   4.143 -               else (*B*)
   4.144 -                 let val crand = cterm_of thy (Abs(x,xT,rand))
   4.145 -                     val crator = cterm_of thy rator
   4.146 -                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
   4.147 -                     val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
   4.148 -                 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
   4.149 -            else makeK()
   4.150 -        | _ => raise Fail "abstract: Bad term"
   4.151 -  end;
   4.152 -
   4.153 -(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
   4.154 -fun introduce_combinators_in_cterm ct =
   4.155 -  if is_quasi_lambda_free (term_of ct) then
   4.156 -    Thm.reflexive ct
   4.157 -  else case term_of ct of
   4.158 -    Abs _ =>
   4.159 -    let
   4.160 -      val (cv, cta) = Thm.dest_abs NONE ct
   4.161 -      val (v, _) = dest_Free (term_of cv)
   4.162 -      val u_th = introduce_combinators_in_cterm cta
   4.163 -      val cu = Thm.rhs_of u_th
   4.164 -      val comb_eq = abstract (Thm.cabs cv cu)
   4.165 -    in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   4.166 -  | _ $ _ =>
   4.167 -    let val (ct1, ct2) = Thm.dest_comb ct in
   4.168 -        Thm.combination (introduce_combinators_in_cterm ct1)
   4.169 -                        (introduce_combinators_in_cterm ct2)
   4.170 -    end
   4.171 -
   4.172 -fun introduce_combinators_in_theorem th =
   4.173 -  if is_quasi_lambda_free (prop_of th) then
   4.174 -    th
   4.175 -  else
   4.176 -    let
   4.177 -      val th = Drule.eta_contraction_rule th
   4.178 -      val eqth = introduce_combinators_in_cterm (cprop_of th)
   4.179 -    in Thm.equal_elim eqth th end
   4.180 -    handle THM (msg, _, _) =>
   4.181 -           (warning ("Error in the combinator translation of " ^
   4.182 -                     Display.string_of_thm_without_context th ^
   4.183 -                     "\nException message: " ^ msg ^ ".");
   4.184 -            (* A type variable of sort "{}" will make abstraction fail. *)
   4.185 -            TrueI)
   4.186 -
   4.187 -(*cterms are used throughout for efficiency*)
   4.188 -val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
   4.189 -
   4.190 -(*Given an abstraction over n variables, replace the bound variables by free
   4.191 -  ones. Return the body, along with the list of free variables.*)
   4.192 -fun c_variant_abs_multi (ct0, vars) =
   4.193 -      let val (cv,ct) = Thm.dest_abs NONE ct0
   4.194 -      in  c_variant_abs_multi (ct, cv::vars)  end
   4.195 -      handle CTERM _ => (ct0, rev vars);
   4.196 -
   4.197 -val skolem_def_raw = @{thms skolem_def_raw}
   4.198 -
   4.199 -(* Given the definition of a Skolem function, return a theorem to replace
   4.200 -   an existential formula by a use of that function.
   4.201 -   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   4.202 -fun old_skolem_theorem_from_def thy rhs0 =
   4.203 -  let
   4.204 -    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
   4.205 -    val rhs' = rhs |> Thm.dest_comb |> snd
   4.206 -    val (ch, frees) = c_variant_abs_multi (rhs', [])
   4.207 -    val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
   4.208 -    val T =
   4.209 -      case hilbert of
   4.210 -        Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
   4.211 -      | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
   4.212 -                         [hilbert])
   4.213 -    val cex = cterm_of thy (HOLogic.exists_const T)
   4.214 -    val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
   4.215 -    val conc =
   4.216 -      Drule.list_comb (rhs, frees)
   4.217 -      |> Drule.beta_conv cabs |> Thm.capply cTrueprop
   4.218 -    fun tacf [prem] =
   4.219 -      rewrite_goals_tac skolem_def_raw
   4.220 -      THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
   4.221 -  in
   4.222 -    Goal.prove_internal [ex_tm] conc tacf
   4.223 -    |> forall_intr_list frees
   4.224 -    |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   4.225 -    |> Thm.varifyT_global
   4.226 -  end
   4.227 -
   4.228 -fun to_definitional_cnf_with_quantifiers thy th =
   4.229 -  let
   4.230 -    val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
   4.231 -    val eqth = eqth RS @{thm eq_reflection}
   4.232 -    val eqth = eqth RS @{thm TruepropI}
   4.233 -  in Thm.equal_elim eqth th end
   4.234 -
   4.235 -fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
   4.236 -  (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
   4.237 -  "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
   4.238 -  string_of_int index_no ^ "_" ^ s
   4.239 -
   4.240 -fun cluster_of_zapped_var_name s =
   4.241 -  let val get_int = the o Int.fromString o nth (space_explode "_" s) in
   4.242 -    ((get_int 1, (get_int 2, get_int 3)),
   4.243 -     String.isPrefix new_skolem_var_prefix s)
   4.244 -  end
   4.245 -
   4.246 -fun zap (cluster as (cluster_no, cluster_skolem)) index_no pos ct =
   4.247 -  ct
   4.248 -  |> (case term_of ct of
   4.249 -        Const (s, _) $ Abs (s', _, _) =>
   4.250 -        if s = @{const_name all} orelse s = @{const_name All} orelse
   4.251 -           s = @{const_name Ex} then
   4.252 -          let
   4.253 -            val skolem = (pos = (s = @{const_name Ex}))
   4.254 -            val (cluster, index_no) =
   4.255 -              if skolem = cluster_skolem then (cluster, index_no)
   4.256 -              else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
   4.257 -          in
   4.258 -            Thm.dest_comb #> snd
   4.259 -            #> Thm.dest_abs (SOME (zapped_var_name cluster index_no s'))
   4.260 -            #> snd #> zap cluster (index_no + 1) pos
   4.261 -          end
   4.262 -        else
   4.263 -          Conv.all_conv
   4.264 -      | Const (s, _) $ _ $ _ =>
   4.265 -        if s = @{const_name "==>"} orelse s = @{const_name implies} then
   4.266 -          Conv.combination_conv (Conv.arg_conv (zap cluster index_no (not pos)))
   4.267 -                                (zap cluster index_no pos)
   4.268 -        else if s = @{const_name conj} orelse s = @{const_name disj} then
   4.269 -          Conv.combination_conv (Conv.arg_conv (zap cluster index_no pos))
   4.270 -                                (zap cluster index_no pos)
   4.271 -        else
   4.272 -          Conv.all_conv
   4.273 -      | Const (s, _) $ _ =>
   4.274 -        if s = @{const_name Trueprop} then
   4.275 -          Conv.arg_conv (zap cluster index_no pos)
   4.276 -        else if s = @{const_name Not} then
   4.277 -          Conv.arg_conv (zap cluster index_no (not pos))
   4.278 -        else
   4.279 -          Conv.all_conv
   4.280 -      | _ => Conv.all_conv)
   4.281 -
   4.282 -fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
   4.283 -
   4.284 -val no_choice =
   4.285 -  @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
   4.286 -  |> Logic.varify_global
   4.287 -  |> Skip_Proof.make_thm @{theory}
   4.288 -
   4.289 -(* Converts an Isabelle theorem into NNF. *)
   4.290 -fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt =
   4.291 -  let
   4.292 -    val thy = ProofContext.theory_of ctxt
   4.293 -    val th =
   4.294 -      th |> transform_elim_theorem
   4.295 -         |> zero_var_indexes
   4.296 -         |> new_skolemizer ? forall_intr_vars
   4.297 -    val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
   4.298 -    val th = th |> Conv.fconv_rule Object_Logic.atomize
   4.299 -                |> extensionalize_theorem
   4.300 -                |> Meson.make_nnf ctxt
   4.301 -  in
   4.302 -    if new_skolemizer then
   4.303 -      let
   4.304 -        fun skolemize choice_ths =
   4.305 -          Meson.skolemize_with_choice_thms ctxt choice_ths
   4.306 -          #> simplify (ss_only @{thms all_simps[symmetric]})
   4.307 -        val pull_out =
   4.308 -          simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
   4.309 -        val (discharger_th, fully_skolemized_th) =
   4.310 -          if null choice_ths then
   4.311 -            th |> `I |>> pull_out ||> skolemize [no_choice]
   4.312 -          else
   4.313 -            th |> skolemize choice_ths |> `I
   4.314 -        val t =
   4.315 -          fully_skolemized_th |> cprop_of
   4.316 -          |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context
   4.317 -          |> cprop_of |> Thm.dest_equals |> snd |> term_of
   4.318 -      in
   4.319 -        if exists_subterm (fn Var ((s, _), _) =>
   4.320 -                              String.isPrefix new_skolem_var_prefix s
   4.321 -                            | _ => false) t then
   4.322 -          let
   4.323 -            val (ct, ctxt) =
   4.324 -              Variable.import_terms true [t] ctxt
   4.325 -              |>> the_single |>> cterm_of thy
   4.326 -          in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end
   4.327 -       else
   4.328 -         (NONE, th, ctxt)
   4.329 -      end
   4.330 -    else
   4.331 -      (NONE, th, ctxt)
   4.332 -  end
   4.333 -
   4.334 -(* Convert a theorem to CNF, with additional premises due to skolemization. *)
   4.335 -fun cnf_axiom ctxt0 new_skolemizer ax_no th =
   4.336 -  let
   4.337 -    val thy = ProofContext.theory_of ctxt0
   4.338 -    val choice_ths = Meson_Choices.get ctxt0
   4.339 -    val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
   4.340 -    fun clausify th =
   4.341 -      Meson.make_cnf (if new_skolemizer then
   4.342 -                        []
   4.343 -                      else
   4.344 -                        map (old_skolem_theorem_from_def thy)
   4.345 -                            (old_skolem_defs th)) th ctxt
   4.346 -    val (cnf_ths, ctxt) =
   4.347 -      clausify nnf_th
   4.348 -      |> (fn ([], _) =>
   4.349 -             clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
   4.350 -           | p => p)
   4.351 -    fun intr_imp ct th =
   4.352 -      Thm.instantiate ([], map (pairself (cterm_of @{theory}))
   4.353 -                               [(Var (("i", 1), @{typ nat}),
   4.354 -                                 HOLogic.mk_nat ax_no)])
   4.355 -                      @{thm skolem_COMBK_D}
   4.356 -      RS Thm.implies_intr ct th
   4.357 -  in
   4.358 -    (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
   4.359 -                        ##> (term_of #> HOLogic.dest_Trueprop
   4.360 -                             #> singleton (Variable.export_terms ctxt ctxt0))),
   4.361 -     cnf_ths |> map (introduce_combinators_in_theorem
   4.362 -                     #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
   4.363 -             |> Variable.export ctxt ctxt0
   4.364 -             |> Meson.finish_cnf
   4.365 -             |> map Thm.close_derivation)
   4.366 -  end
   4.367 -  handle THM _ => (NONE, [])
   4.368 -
   4.369 -fun meson_general_tac ctxt ths =
   4.370 -  let val ctxt = Classical.put_claset HOL_cs ctxt in
   4.371 -    Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
   4.372 -  end
   4.373 -
   4.374 -val setup =
   4.375 -  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
   4.376 -     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
   4.377 -     "MESON resolution proof procedure"
   4.378 -
   4.379 -end;
     5.1 --- a/src/HOL/Tools/meson.ML	Mon Oct 04 20:55:55 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,712 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/meson.ML
     5.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.6 -
     5.7 -The MESON resolution proof procedure for HOL.
     5.8 -When making clauses, avoids using the rewriter -- instead uses RS recursively.
     5.9 -*)
    5.10 -
    5.11 -signature MESON =
    5.12 -sig
    5.13 -  val trace: bool Unsynchronized.ref
    5.14 -  val term_pair_of: indexname * (typ * 'a) -> term * 'a
    5.15 -  val size_of_subgoals: thm -> int
    5.16 -  val has_too_many_clauses: Proof.context -> term -> bool
    5.17 -  val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    5.18 -  val finish_cnf: thm list -> thm list
    5.19 -  val presimplify: thm -> thm
    5.20 -  val make_nnf: Proof.context -> thm -> thm
    5.21 -  val skolemize_with_choice_thms : Proof.context -> thm list -> thm -> thm
    5.22 -  val skolemize : Proof.context -> thm -> thm
    5.23 -  val is_fol_term: theory -> term -> bool
    5.24 -  val make_clauses_unsorted: thm list -> thm list
    5.25 -  val make_clauses: thm list -> thm list
    5.26 -  val make_horns: thm list -> thm list
    5.27 -  val best_prolog_tac: (thm -> int) -> thm list -> tactic
    5.28 -  val depth_prolog_tac: thm list -> tactic
    5.29 -  val gocls: thm list -> thm list
    5.30 -  val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
    5.31 -  val MESON:
    5.32 -    tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
    5.33 -    -> int -> tactic
    5.34 -  val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
    5.35 -  val safe_best_meson_tac: Proof.context -> int -> tactic
    5.36 -  val depth_meson_tac: Proof.context -> int -> tactic
    5.37 -  val prolog_step_tac': thm list -> int -> tactic
    5.38 -  val iter_deepen_prolog_tac: thm list -> tactic
    5.39 -  val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
    5.40 -  val make_meta_clause: thm -> thm
    5.41 -  val make_meta_clauses: thm list -> thm list
    5.42 -  val meson_tac: Proof.context -> thm list -> int -> tactic
    5.43 -  val setup: theory -> theory
    5.44 -end
    5.45 -
    5.46 -structure Meson : MESON =
    5.47 -struct
    5.48 -
    5.49 -val trace = Unsynchronized.ref false;
    5.50 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    5.51 -
    5.52 -val max_clauses_default = 60;
    5.53 -val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default);
    5.54 -
    5.55 -(*No known example (on 1-5-2007) needs even thirty*)
    5.56 -val iter_deepen_limit = 50;
    5.57 -
    5.58 -val disj_forward = @{thm disj_forward};
    5.59 -val disj_forward2 = @{thm disj_forward2};
    5.60 -val make_pos_rule = @{thm make_pos_rule};
    5.61 -val make_pos_rule' = @{thm make_pos_rule'};
    5.62 -val make_pos_goal = @{thm make_pos_goal};
    5.63 -val make_neg_rule = @{thm make_neg_rule};
    5.64 -val make_neg_rule' = @{thm make_neg_rule'};
    5.65 -val make_neg_goal = @{thm make_neg_goal};
    5.66 -val conj_forward = @{thm conj_forward};
    5.67 -val all_forward = @{thm all_forward};
    5.68 -val ex_forward = @{thm ex_forward};
    5.69 -
    5.70 -val not_conjD = @{thm meson_not_conjD};
    5.71 -val not_disjD = @{thm meson_not_disjD};
    5.72 -val not_notD = @{thm meson_not_notD};
    5.73 -val not_allD = @{thm meson_not_allD};
    5.74 -val not_exD = @{thm meson_not_exD};
    5.75 -val imp_to_disjD = @{thm meson_imp_to_disjD};
    5.76 -val not_impD = @{thm meson_not_impD};
    5.77 -val iff_to_disjD = @{thm meson_iff_to_disjD};
    5.78 -val not_iffD = @{thm meson_not_iffD};
    5.79 -val conj_exD1 = @{thm meson_conj_exD1};
    5.80 -val conj_exD2 = @{thm meson_conj_exD2};
    5.81 -val disj_exD = @{thm meson_disj_exD};
    5.82 -val disj_exD1 = @{thm meson_disj_exD1};
    5.83 -val disj_exD2 = @{thm meson_disj_exD2};
    5.84 -val disj_assoc = @{thm meson_disj_assoc};
    5.85 -val disj_comm = @{thm meson_disj_comm};
    5.86 -val disj_FalseD1 = @{thm meson_disj_FalseD1};
    5.87 -val disj_FalseD2 = @{thm meson_disj_FalseD2};
    5.88 -
    5.89 -
    5.90 -(**** Operators for forward proof ****)
    5.91 -
    5.92 -
    5.93 -(** First-order Resolution **)
    5.94 -
    5.95 -fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
    5.96 -
    5.97 -(*FIXME: currently does not "rename variables apart"*)
    5.98 -fun first_order_resolve thA thB =
    5.99 -  (case
   5.100 -    try (fn () =>
   5.101 -      let val thy = theory_of_thm thA
   5.102 -          val tmA = concl_of thA
   5.103 -          val Const("==>",_) $ tmB $ _ = prop_of thB
   5.104 -          val tenv =
   5.105 -            Pattern.first_order_match thy (tmB, tmA)
   5.106 -                                          (Vartab.empty, Vartab.empty) |> snd
   5.107 -          val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
   5.108 -      in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
   5.109 -    SOME th => th
   5.110 -  | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
   5.111 -
   5.112 -(* Applying "choice" swaps the bound variable names. We tweak
   5.113 -   "Thm.rename_boundvars"'s input to get the desired names. *)
   5.114 -fun fix_bounds (_ $ (Const (@{const_name Ex}, _)
   5.115 -                     $ Abs (_, _, Const (@{const_name All}, _) $ _)))
   5.116 -               (t0 $ (Const (@{const_name All}, T1)
   5.117 -                      $ Abs (a1, T1', Const (@{const_name Ex}, T2)
   5.118 -                                      $ Abs (a2, T2', t')))) =
   5.119 -    t0 $ (Const (@{const_name All}, T1)
   5.120 -          $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t')))
   5.121 -  | fix_bounds _ t = t
   5.122 -
   5.123 -(* Hack to make it less likely that we lose our precious bound variable names in
   5.124 -   "rename_bvs_RS" below, because of a clash. *)
   5.125 -val protect_prefix = "_"
   5.126 -
   5.127 -fun protect_bounds (t $ u) = protect_bounds t $ protect_bounds u
   5.128 -  | protect_bounds (Abs (s, T, t')) =
   5.129 -    Abs (protect_prefix ^ s, T, protect_bounds t')
   5.130 -  | protect_bounds t = t
   5.131 -
   5.132 -(* Forward proof while preserving bound variables names*)
   5.133 -fun rename_bvs_RS th rl =
   5.134 -  let
   5.135 -    val t = concl_of th
   5.136 -    val r = concl_of rl
   5.137 -    val th' = th RS Thm.rename_boundvars r (protect_bounds r) rl
   5.138 -    val t' = concl_of th'
   5.139 -  in Thm.rename_boundvars t' (fix_bounds t' t) th' end
   5.140 -
   5.141 -(*raises exception if no rules apply*)
   5.142 -fun tryres (th, rls) =
   5.143 -  let fun tryall [] = raise THM("tryres", 0, th::rls)
   5.144 -        | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
   5.145 -  in  tryall rls  end;
   5.146 -
   5.147 -(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
   5.148 -  e.g. from conj_forward, should have the form
   5.149 -    "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
   5.150 -  and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
   5.151 -fun forward_res ctxt nf st =
   5.152 -  let fun forward_tacf [prem] = rtac (nf prem) 1
   5.153 -        | forward_tacf prems =
   5.154 -            error (cat_lines
   5.155 -              ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
   5.156 -                Display.string_of_thm ctxt st ::
   5.157 -                "Premises:" :: map (Display.string_of_thm ctxt) prems))
   5.158 -  in
   5.159 -    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
   5.160 -    of SOME(th,_) => th
   5.161 -     | NONE => raise THM("forward_res", 0, [st])
   5.162 -  end;
   5.163 -
   5.164 -(*Are any of the logical connectives in "bs" present in the term?*)
   5.165 -fun has_conns bs =
   5.166 -  let fun has (Const _) = false
   5.167 -        | has (Const(@{const_name Trueprop},_) $ p) = has p
   5.168 -        | has (Const(@{const_name Not},_) $ p) = has p
   5.169 -        | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
   5.170 -        | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
   5.171 -        | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
   5.172 -        | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
   5.173 -        | has _ = false
   5.174 -  in  has  end;
   5.175 -
   5.176 -
   5.177 -(**** Clause handling ****)
   5.178 -
   5.179 -fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
   5.180 -  | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
   5.181 -  | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
   5.182 -  | literals P = [(true,P)];
   5.183 -
   5.184 -(*number of literals in a term*)
   5.185 -val nliterals = length o literals;
   5.186 -
   5.187 -
   5.188 -(*** Tautology Checking ***)
   5.189 -
   5.190 -fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
   5.191 -      signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   5.192 -  | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
   5.193 -  | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
   5.194 -
   5.195 -fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
   5.196 -
   5.197 -(*Literals like X=X are tautologous*)
   5.198 -fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
   5.199 -  | taut_poslit (Const(@{const_name True},_)) = true
   5.200 -  | taut_poslit _ = false;
   5.201 -
   5.202 -fun is_taut th =
   5.203 -  let val (poslits,neglits) = signed_lits th
   5.204 -  in  exists taut_poslit poslits
   5.205 -      orelse
   5.206 -      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
   5.207 -  end
   5.208 -  handle TERM _ => false;       (*probably dest_Trueprop on a weird theorem*)
   5.209 -
   5.210 -
   5.211 -(*** To remove trivial negated equality literals from clauses ***)
   5.212 -
   5.213 -(*They are typically functional reflexivity axioms and are the converses of
   5.214 -  injectivity equivalences*)
   5.215 -
   5.216 -val not_refl_disj_D = @{thm meson_not_refl_disj_D};
   5.217 -
   5.218 -(*Is either term a Var that does not properly occur in the other term?*)
   5.219 -fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
   5.220 -  | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u))
   5.221 -  | eliminable _ = false;
   5.222 -
   5.223 -fun refl_clause_aux 0 th = th
   5.224 -  | refl_clause_aux n th =
   5.225 -       case HOLogic.dest_Trueprop (concl_of th) of
   5.226 -          (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
   5.227 -            refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
   5.228 -        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
   5.229 -            if eliminable(t,u)
   5.230 -            then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
   5.231 -            else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
   5.232 -        | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   5.233 -        | _ => (*not a disjunction*) th;
   5.234 -
   5.235 -fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
   5.236 -      notequal_lits_count P + notequal_lits_count Q
   5.237 -  | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1
   5.238 -  | notequal_lits_count _ = 0;
   5.239 -
   5.240 -(*Simplify a clause by applying reflexivity to its negated equality literals*)
   5.241 -fun refl_clause th =
   5.242 -  let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
   5.243 -  in  zero_var_indexes (refl_clause_aux neqs th)  end
   5.244 -  handle TERM _ => th;  (*probably dest_Trueprop on a weird theorem*)
   5.245 -
   5.246 -
   5.247 -(*** Removal of duplicate literals ***)
   5.248 -
   5.249 -(*Forward proof, passing extra assumptions as theorems to the tactic*)
   5.250 -fun forward_res2 nf hyps st =
   5.251 -  case Seq.pull
   5.252 -        (REPEAT
   5.253 -         (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
   5.254 -         st)
   5.255 -  of SOME(th,_) => th
   5.256 -   | NONE => raise THM("forward_res2", 0, [st]);
   5.257 -
   5.258 -(*Remove duplicates in P|Q by assuming ~P in Q
   5.259 -  rls (initially []) accumulates assumptions of the form P==>False*)
   5.260 -fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
   5.261 -    handle THM _ => tryres(th,rls)
   5.262 -    handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2),
   5.263 -                           [disj_FalseD1, disj_FalseD2, asm_rl])
   5.264 -    handle THM _ => th;
   5.265 -
   5.266 -(*Remove duplicate literals, if there are any*)
   5.267 -fun nodups ctxt th =
   5.268 -  if has_duplicates (op =) (literals (prop_of th))
   5.269 -    then nodups_aux ctxt [] th
   5.270 -    else th;
   5.271 -
   5.272 -
   5.273 -(*** The basic CNF transformation ***)
   5.274 -
   5.275 -fun estimated_num_clauses bound t =
   5.276 - let
   5.277 -  fun sum x y = if x < bound andalso y < bound then x+y else bound
   5.278 -  fun prod x y = if x < bound andalso y < bound then x*y else bound
   5.279 -  
   5.280 -  (*Estimate the number of clauses in order to detect infeasible theorems*)
   5.281 -  fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
   5.282 -    | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
   5.283 -    | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
   5.284 -        if b then sum (signed_nclauses b t) (signed_nclauses b u)
   5.285 -             else prod (signed_nclauses b t) (signed_nclauses b u)
   5.286 -    | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
   5.287 -        if b then prod (signed_nclauses b t) (signed_nclauses b u)
   5.288 -             else sum (signed_nclauses b t) (signed_nclauses b u)
   5.289 -    | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
   5.290 -        if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
   5.291 -             else sum (signed_nclauses (not b) t) (signed_nclauses b u)
   5.292 -    | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) =
   5.293 -        if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
   5.294 -            if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
   5.295 -                          (prod (signed_nclauses (not b) u) (signed_nclauses b t))
   5.296 -                 else sum (prod (signed_nclauses b t) (signed_nclauses b u))
   5.297 -                          (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
   5.298 -        else 1
   5.299 -    | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
   5.300 -    | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
   5.301 -    | signed_nclauses _ _ = 1; (* literal *)
   5.302 - in signed_nclauses true t end
   5.303 -
   5.304 -fun has_too_many_clauses ctxt t =
   5.305 -  let val max_cl = Config.get ctxt max_clauses in
   5.306 -    estimated_num_clauses (max_cl + 1) t > max_cl
   5.307 -  end
   5.308 -
   5.309 -(*Replaces universally quantified variables by FREE variables -- because
   5.310 -  assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
   5.311 -local  
   5.312 -  val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
   5.313 -  val spec_varT = #T (Thm.rep_cterm spec_var);
   5.314 -  fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
   5.315 -in  
   5.316 -  fun freeze_spec th ctxt =
   5.317 -    let
   5.318 -      val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
   5.319 -      val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
   5.320 -      val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
   5.321 -    in (th RS spec', ctxt') end
   5.322 -end;
   5.323 -
   5.324 -(*Used with METAHYPS below. There is one assumption, which gets bound to prem
   5.325 -  and then normalized via function nf. The normal form is given to resolve_tac,
   5.326 -  instantiate a Boolean variable created by resolution with disj_forward. Since
   5.327 -  (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
   5.328 -fun resop nf [prem] = resolve_tac (nf prem) 1;
   5.329 -
   5.330 -(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
   5.331 -   and "Pure.term"? *)
   5.332 -val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
   5.333 -
   5.334 -fun apply_skolem_theorem (th, rls) =
   5.335 -  let
   5.336 -    fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
   5.337 -      | tryall (rl :: rls) =
   5.338 -        first_order_resolve th rl handle THM _ => tryall rls
   5.339 -  in tryall rls end
   5.340 -
   5.341 -(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
   5.342 -   Strips universal quantifiers and breaks up conjunctions.
   5.343 -   Eliminates existential quantifiers using Skolemization theorems. *)
   5.344 -fun cnf old_skolem_ths ctxt (th, ths) =
   5.345 -  let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
   5.346 -      fun cnf_aux (th,ths) =
   5.347 -        if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   5.348 -        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
   5.349 -        then nodups ctxt th :: ths (*no work to do, terminate*)
   5.350 -        else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   5.351 -            Const (@{const_name HOL.conj}, _) => (*conjunction*)
   5.352 -                cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   5.353 -          | Const (@{const_name All}, _) => (*universal quantifier*)
   5.354 -                let val (th',ctxt') = freeze_spec th (!ctxtr)
   5.355 -                in  ctxtr := ctxt'; cnf_aux (th', ths) end
   5.356 -          | Const (@{const_name Ex}, _) =>
   5.357 -              (*existential quantifier: Insert Skolem functions*)
   5.358 -              cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
   5.359 -          | Const (@{const_name HOL.disj}, _) =>
   5.360 -              (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
   5.361 -                all combinations of converting P, Q to CNF.*)
   5.362 -              let val tac =
   5.363 -                  Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN
   5.364 -                   (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1)
   5.365 -              in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
   5.366 -          | _ => nodups ctxt th :: ths  (*no work to do*)
   5.367 -      and cnf_nil th = cnf_aux (th,[])
   5.368 -      val cls =
   5.369 -            if has_too_many_clauses ctxt (concl_of th)
   5.370 -            then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
   5.371 -            else cnf_aux (th,ths)
   5.372 -  in  (cls, !ctxtr)  end;
   5.373 -
   5.374 -fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
   5.375 -
   5.376 -(*Generalization, removal of redundant equalities, removal of tautologies.*)
   5.377 -fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
   5.378 -
   5.379 -
   5.380 -(**** Generation of contrapositives ****)
   5.381 -
   5.382 -fun is_left (Const (@{const_name Trueprop}, _) $
   5.383 -               (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
   5.384 -  | is_left _ = false;
   5.385 -
   5.386 -(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   5.387 -fun assoc_right th =
   5.388 -  if is_left (prop_of th) then assoc_right (th RS disj_assoc)
   5.389 -  else th;
   5.390 -
   5.391 -(*Must check for negative literal first!*)
   5.392 -val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
   5.393 -
   5.394 -(*For ordinary resolution. *)
   5.395 -val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   5.396 -
   5.397 -(*Create a goal or support clause, conclusing False*)
   5.398 -fun make_goal th =   (*Must check for negative literal first!*)
   5.399 -    make_goal (tryres(th, clause_rules))
   5.400 -  handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
   5.401 -
   5.402 -(*Sort clauses by number of literals*)
   5.403 -fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
   5.404 -
   5.405 -fun sort_clauses ths = sort (make_ord fewerlits) ths;
   5.406 -
   5.407 -fun has_bool @{typ bool} = true
   5.408 -  | has_bool (Type (_, Ts)) = exists has_bool Ts
   5.409 -  | has_bool _ = false
   5.410 -
   5.411 -fun has_fun (Type (@{type_name fun}, _)) = true
   5.412 -  | has_fun (Type (_, Ts)) = exists has_fun Ts
   5.413 -  | has_fun _ = false
   5.414 -
   5.415 -(*Is the string the name of a connective? Really only | and Not can remain,
   5.416 -  since this code expects to be called on a clause form.*)
   5.417 -val is_conn = member (op =)
   5.418 -    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
   5.419 -     @{const_name HOL.implies}, @{const_name Not},
   5.420 -     @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
   5.421 -
   5.422 -(*True if the term contains a function--not a logical connective--where the type
   5.423 -  of any argument contains bool.*)
   5.424 -val has_bool_arg_const =
   5.425 -    exists_Const
   5.426 -      (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
   5.427 -
   5.428 -(*A higher-order instance of a first-order constant? Example is the definition of
   5.429 -  one, 1, at a function type in theory Function_Algebras.*)
   5.430 -fun higher_inst_const thy (c,T) =
   5.431 -  case binder_types T of
   5.432 -      [] => false (*not a function type, OK*)
   5.433 -    | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
   5.434 -
   5.435 -(*Returns false if any Vars in the theorem mention type bool.
   5.436 -  Also rejects functions whose arguments are Booleans or other functions.*)
   5.437 -fun is_fol_term thy t =
   5.438 -    Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
   5.439 -    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
   5.440 -                           | _ => false) t orelse
   5.441 -         has_bool_arg_const t orelse
   5.442 -         exists_Const (higher_inst_const thy) t orelse
   5.443 -         has_meta_conn t);
   5.444 -
   5.445 -fun rigid t = not (is_Var (head_of t));
   5.446 -
   5.447 -fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
   5.448 -  | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
   5.449 -  | ok4horn _ = false;
   5.450 -
   5.451 -(*Create a meta-level Horn clause*)
   5.452 -fun make_horn crules th =
   5.453 -  if ok4horn (concl_of th)
   5.454 -  then make_horn crules (tryres(th,crules)) handle THM _ => th
   5.455 -  else th;
   5.456 -
   5.457 -(*Generate Horn clauses for all contrapositives of a clause. The input, th,
   5.458 -  is a HOL disjunction.*)
   5.459 -fun add_contras crules th hcs =
   5.460 -  let fun rots (0,_) = hcs
   5.461 -        | rots (k,th) = zero_var_indexes (make_horn crules th) ::
   5.462 -                        rots(k-1, assoc_right (th RS disj_comm))
   5.463 -  in case nliterals(prop_of th) of
   5.464 -        1 => th::hcs
   5.465 -      | n => rots(n, assoc_right th)
   5.466 -  end;
   5.467 -
   5.468 -(*Use "theorem naming" to label the clauses*)
   5.469 -fun name_thms label =
   5.470 -    let fun name1 th (k, ths) =
   5.471 -          (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
   5.472 -    in  fn ths => #2 (fold_rev name1 ths (length ths, []))  end;
   5.473 -
   5.474 -(*Is the given disjunction an all-negative support clause?*)
   5.475 -fun is_negative th = forall (not o #1) (literals (prop_of th));
   5.476 -
   5.477 -val neg_clauses = filter is_negative;
   5.478 -
   5.479 -
   5.480 -(***** MESON PROOF PROCEDURE *****)
   5.481 -
   5.482 -fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
   5.483 -           As) = rhyps(phi, A::As)
   5.484 -  | rhyps (_, As) = As;
   5.485 -
   5.486 -(** Detecting repeated assumptions in a subgoal **)
   5.487 -
   5.488 -(*The stringtree detects repeated assumptions.*)
   5.489 -fun ins_term t net = Net.insert_term (op aconv) (t, t) net;
   5.490 -
   5.491 -(*detects repetitions in a list of terms*)
   5.492 -fun has_reps [] = false
   5.493 -  | has_reps [_] = false
   5.494 -  | has_reps [t,u] = (t aconv u)
   5.495 -  | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true;
   5.496 -
   5.497 -(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
   5.498 -fun TRYING_eq_assume_tac 0 st = Seq.single st
   5.499 -  | TRYING_eq_assume_tac i st =
   5.500 -       TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
   5.501 -       handle THM _ => TRYING_eq_assume_tac (i-1) st;
   5.502 -
   5.503 -fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
   5.504 -
   5.505 -(*Loop checking: FAIL if trying to prove the same thing twice
   5.506 -  -- if *ANY* subgoal has repeated literals*)
   5.507 -fun check_tac st =
   5.508 -  if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   5.509 -  then  Seq.empty  else  Seq.single st;
   5.510 -
   5.511 -
   5.512 -(* net_resolve_tac actually made it slower... *)
   5.513 -fun prolog_step_tac horns i =
   5.514 -    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   5.515 -    TRYALL_eq_assume_tac;
   5.516 -
   5.517 -(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   5.518 -fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
   5.519 -
   5.520 -fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
   5.521 -
   5.522 -
   5.523 -(*Negation Normal Form*)
   5.524 -val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
   5.525 -               not_impD, not_iffD, not_allD, not_exD, not_notD];
   5.526 -
   5.527 -fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t
   5.528 -  | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t
   5.529 -  | ok4nnf _ = false;
   5.530 -
   5.531 -fun make_nnf1 ctxt th =
   5.532 -  if ok4nnf (concl_of th)
   5.533 -  then make_nnf1 ctxt (tryres(th, nnf_rls))
   5.534 -    handle THM ("tryres", _, _) =>
   5.535 -        forward_res ctxt (make_nnf1 ctxt)
   5.536 -           (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   5.537 -    handle THM ("tryres", _, _) => th
   5.538 -  else th
   5.539 -
   5.540 -(*The simplification removes defined quantifiers and occurrences of True and False.
   5.541 -  nnf_ss also includes the one-point simprocs,
   5.542 -  which are needed to avoid the various one-point theorems from generating junk clauses.*)
   5.543 -val nnf_simps =
   5.544 -  @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
   5.545 -         if_eq_cancel cases_simp}
   5.546 -val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
   5.547 -
   5.548 -val nnf_ss =
   5.549 -  HOL_basic_ss addsimps nnf_extra_simps
   5.550 -    addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
   5.551 -
   5.552 -val presimplify =
   5.553 -  rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss
   5.554 -
   5.555 -fun make_nnf ctxt th = case prems_of th of
   5.556 -    [] => th |> presimplify |> make_nnf1 ctxt
   5.557 -  | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   5.558 -
   5.559 -(* Pull existential quantifiers to front. This accomplishes Skolemization for
   5.560 -   clauses that arise from a subgoal. *)
   5.561 -fun skolemize_with_choice_thms ctxt choice_ths =
   5.562 -  let
   5.563 -    fun aux th =
   5.564 -      if not (has_conns [@{const_name Ex}] (prop_of th)) then
   5.565 -        th
   5.566 -      else
   5.567 -        tryres (th, choice_ths @
   5.568 -                    [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2])
   5.569 -        |> aux
   5.570 -        handle THM ("tryres", _, _) =>
   5.571 -               tryres (th, [conj_forward, disj_forward, all_forward])
   5.572 -               |> forward_res ctxt aux
   5.573 -               |> aux
   5.574 -               handle THM ("tryres", _, _) =>
   5.575 -                      rename_bvs_RS th ex_forward
   5.576 -                      |> forward_res ctxt aux
   5.577 -  in aux o make_nnf ctxt end
   5.578 -
   5.579 -fun skolemize ctxt = skolemize_with_choice_thms ctxt (Meson_Choices.get ctxt)
   5.580 -
   5.581 -(* "RS" can fail if "unify_search_bound" is too small. *)
   5.582 -fun try_skolemize ctxt th =
   5.583 -  try (skolemize ctxt) th
   5.584 -  |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^
   5.585 -                                         Display.string_of_thm ctxt th)
   5.586 -           | _ => ())
   5.587 -
   5.588 -fun add_clauses th cls =
   5.589 -  let val ctxt0 = Variable.global_thm_context th
   5.590 -      val (cnfs, ctxt) = make_cnf [] th ctxt0
   5.591 -  in Variable.export ctxt ctxt0 cnfs @ cls end;
   5.592 -
   5.593 -(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   5.594 -  The resulting clauses are HOL disjunctions.*)
   5.595 -fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
   5.596 -val make_clauses = sort_clauses o make_clauses_unsorted;
   5.597 -
   5.598 -(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   5.599 -fun make_horns ths =
   5.600 -    name_thms "Horn#"
   5.601 -      (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
   5.602 -
   5.603 -(*Could simply use nprems_of, which would count remaining subgoals -- no
   5.604 -  discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   5.605 -
   5.606 -fun best_prolog_tac sizef horns =
   5.607 -    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   5.608 -
   5.609 -fun depth_prolog_tac horns =
   5.610 -    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   5.611 -
   5.612 -(*Return all negative clauses, as possible goal clauses*)
   5.613 -fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   5.614 -
   5.615 -fun skolemize_prems_tac ctxt prems =
   5.616 -  cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE
   5.617 -
   5.618 -(*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   5.619 -  Function mkcl converts theorems to clauses.*)
   5.620 -fun MESON preskolem_tac mkcl cltac ctxt i st =
   5.621 -  SELECT_GOAL
   5.622 -    (EVERY [Object_Logic.atomize_prems_tac 1,
   5.623 -            rtac ccontr 1,
   5.624 -            preskolem_tac,
   5.625 -            Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
   5.626 -                      EVERY1 [skolemize_prems_tac ctxt negs,
   5.627 -                              Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   5.628 -  handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
   5.629 -
   5.630 -
   5.631 -(** Best-first search versions **)
   5.632 -
   5.633 -(*ths is a list of additional clauses (HOL disjunctions) to use.*)
   5.634 -fun best_meson_tac sizef =
   5.635 -  MESON all_tac make_clauses
   5.636 -    (fn cls =>
   5.637 -         THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   5.638 -                         (has_fewer_prems 1, sizef)
   5.639 -                         (prolog_step_tac (make_horns cls) 1));
   5.640 -
   5.641 -(*First, breaks the goal into independent units*)
   5.642 -fun safe_best_meson_tac ctxt =
   5.643 -     SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
   5.644 -                  TRYALL (best_meson_tac size_of_subgoals ctxt));
   5.645 -
   5.646 -(** Depth-first search version **)
   5.647 -
   5.648 -val depth_meson_tac =
   5.649 -  MESON all_tac make_clauses
   5.650 -    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
   5.651 -
   5.652 -
   5.653 -(** Iterative deepening version **)
   5.654 -
   5.655 -(*This version does only one inference per call;
   5.656 -  having only one eq_assume_tac speeds it up!*)
   5.657 -fun prolog_step_tac' horns =
   5.658 -    let val (horn0s, _) = (*0 subgoals vs 1 or more*)
   5.659 -            take_prefix Thm.no_prems horns
   5.660 -        val nrtac = net_resolve_tac horns
   5.661 -    in  fn i => eq_assume_tac i ORELSE
   5.662 -                match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   5.663 -                ((assume_tac i APPEND nrtac i) THEN check_tac)
   5.664 -    end;
   5.665 -
   5.666 -fun iter_deepen_prolog_tac horns =
   5.667 -    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
   5.668 -
   5.669 -fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses
   5.670 -  (fn cls =>
   5.671 -    (case (gocls (cls @ ths)) of
   5.672 -      [] => no_tac  (*no goal clauses*)
   5.673 -    | goes =>
   5.674 -        let
   5.675 -          val horns = make_horns (cls @ ths)
   5.676 -          val _ = trace_msg (fn () =>
   5.677 -            cat_lines ("meson method called:" ::
   5.678 -              map (Display.string_of_thm ctxt) (cls @ ths) @
   5.679 -              ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
   5.680 -        in
   5.681 -          THEN_ITER_DEEPEN iter_deepen_limit
   5.682 -            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
   5.683 -        end));
   5.684 -
   5.685 -fun meson_tac ctxt ths =
   5.686 -  SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
   5.687 -
   5.688 -
   5.689 -(**** Code to support ordinary resolution, rather than Model Elimination ****)
   5.690 -
   5.691 -(*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
   5.692 -  with no contrapositives, for ordinary resolution.*)
   5.693 -
   5.694 -(*Rules to convert the head literal into a negated assumption. If the head
   5.695 -  literal is already negated, then using notEfalse instead of notEfalse'
   5.696 -  prevents a double negation.*)
   5.697 -val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
   5.698 -val notEfalse' = rotate_prems 1 notEfalse;
   5.699 -
   5.700 -fun negated_asm_of_head th =
   5.701 -    th RS notEfalse handle THM _ => th RS notEfalse';
   5.702 -
   5.703 -(*Converting one theorem from a disjunction to a meta-level clause*)
   5.704 -fun make_meta_clause th =
   5.705 -  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
   5.706 -  in  
   5.707 -      (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
   5.708 -       negated_asm_of_head o make_horn resolution_clause_rules) fth
   5.709 -  end;
   5.710 -
   5.711 -fun make_meta_clauses ths =
   5.712 -    name_thms "MClause#"
   5.713 -      (distinct Thm.eq_thm_prop (map make_meta_clause ths));
   5.714 -
   5.715 -end;