1.1 --- a/src/HOL/Tools/meson.ML Thu Aug 16 21:52:08 2007 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Fri Aug 17 00:03:50 2007 +0200
1.3 @@ -11,35 +11,42 @@
1.4 FUNCTION nodups -- if done to goal clauses too!
1.5 *)
1.6
1.7 -signature BASIC_MESON =
1.8 +signature MESON =
1.9 sig
1.10 - val size_of_subgoals : thm -> int
1.11 - val make_cnf : thm list -> thm -> thm list
1.12 - val finish_cnf : thm list -> thm list
1.13 - val make_nnf : thm -> thm
1.14 - val make_nnf1 : thm -> thm
1.15 - val skolemize : thm -> thm
1.16 - val make_clauses : thm list -> thm list
1.17 - val make_horns : thm list -> thm list
1.18 - val best_prolog_tac : (thm -> int) -> thm list -> tactic
1.19 - val depth_prolog_tac : thm list -> tactic
1.20 - val gocls : thm list -> thm list
1.21 - val skolemize_prems_tac : thm list -> int -> tactic
1.22 - val MESON : (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
1.23 - val best_meson_tac : (thm -> int) -> int -> tactic
1.24 - val safe_best_meson_tac : int -> tactic
1.25 - val depth_meson_tac : int -> tactic
1.26 - val prolog_step_tac' : thm list -> int -> tactic
1.27 - val iter_deepen_prolog_tac : thm list -> tactic
1.28 - val iter_deepen_meson_tac : thm list -> int -> tactic
1.29 - val meson_tac : int -> tactic
1.30 - val negate_head : thm -> thm
1.31 - val select_literal : int -> thm -> thm
1.32 - val skolemize_tac : int -> tactic
1.33 + val term_pair_of: indexname * (typ * 'a) -> term * 'a
1.34 + val first_order_resolve: thm -> thm -> thm
1.35 + val flexflex_first_order: thm -> thm
1.36 + val size_of_subgoals: thm -> int
1.37 + val make_cnf: thm list -> thm -> thm list
1.38 + val finish_cnf: thm list -> thm list
1.39 + val generalize: thm -> thm
1.40 + val make_nnf: thm -> thm
1.41 + val make_nnf1: thm -> thm
1.42 + val skolemize: thm -> thm
1.43 + val is_fol_term: theory -> term -> bool
1.44 + val make_clauses: thm list -> thm list
1.45 + val make_horns: thm list -> thm list
1.46 + val best_prolog_tac: (thm -> int) -> thm list -> tactic
1.47 + val depth_prolog_tac: thm list -> tactic
1.48 + val gocls: thm list -> thm list
1.49 + val skolemize_prems_tac: thm list -> int -> tactic
1.50 + val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
1.51 + val best_meson_tac: (thm -> int) -> int -> tactic
1.52 + val safe_best_meson_tac: int -> tactic
1.53 + val depth_meson_tac: int -> tactic
1.54 + val prolog_step_tac': thm list -> int -> tactic
1.55 + val iter_deepen_prolog_tac: thm list -> tactic
1.56 + val iter_deepen_meson_tac: thm list -> int -> tactic
1.57 + val make_meta_clause: thm -> thm
1.58 + val make_meta_clauses: thm list -> thm list
1.59 + val meson_claset_tac: thm list -> claset -> int -> tactic
1.60 + val meson_tac: int -> tactic
1.61 + val negate_head: thm -> thm
1.62 + val select_literal: int -> thm -> thm
1.63 + val skolemize_tac: int -> tactic
1.64 end
1.65
1.66 -
1.67 -structure Meson =
1.68 +structure Meson: MESON =
1.69 struct
1.70
1.71 val not_conjD = thm "meson_not_conjD";
1.72 @@ -82,31 +89,31 @@
1.73 in thA RS (cterm_instantiate ct_pairs thB) end
1.74 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
1.75
1.76 -fun flexflex_first_order th =
1.77 +fun flexflex_first_order th =
1.78 case (tpairs_of th) of
1.79 [] => th
1.80 | pairs =>
1.81 - let val thy = theory_of_thm th
1.82 - val (tyenv,tenv) =
1.83 - foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
1.84 - val t_pairs = map term_pair_of (Vartab.dest tenv)
1.85 - val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
1.86 - in th' end
1.87 - handle THM _ => th;
1.88 + let val thy = theory_of_thm th
1.89 + val (tyenv,tenv) =
1.90 + foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
1.91 + val t_pairs = map term_pair_of (Vartab.dest tenv)
1.92 + val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
1.93 + in th' end
1.94 + handle THM _ => th;
1.95
1.96 (*raises exception if no rules apply -- unlike RL*)
1.97 -fun tryres (th, rls) =
1.98 +fun tryres (th, rls) =
1.99 let fun tryall [] = raise THM("tryres", 0, th::rls)
1.100 | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
1.101 in tryall rls end;
1.102 -
1.103 +
1.104 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
1.105 e.g. from conj_forward, should have the form
1.106 "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
1.107 and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
1.108 fun forward_res nf st =
1.109 let fun forward_tacf [prem] = rtac (nf prem) 1
1.110 - | forward_tacf prems =
1.111 + | forward_tacf prems =
1.112 error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
1.113 string_of_thm st ^
1.114 "\nPremises:\n" ^
1.115 @@ -126,9 +133,9 @@
1.116 | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
1.117 | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
1.118 | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
1.119 - | has _ = false
1.120 + | has _ = false
1.121 in has end;
1.122 -
1.123 +
1.124
1.125 (**** Clause handling ****)
1.126
1.127 @@ -143,11 +150,11 @@
1.128
1.129 (*** Tautology Checking ***)
1.130
1.131 -fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
1.132 +fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
1.133 signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
1.134 | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
1.135 | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
1.136 -
1.137 +
1.138 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
1.139
1.140 (*Literals like X=X are tautologous*)
1.141 @@ -161,14 +168,14 @@
1.142 orelse
1.143 exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
1.144 end
1.145 - handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
1.146 + handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
1.147
1.148
1.149 (*** To remove trivial negated equality literals from clauses ***)
1.150
1.151 (*They are typically functional reflexivity axioms and are the converses of
1.152 injectivity equivalences*)
1.153 -
1.154 +
1.155 val not_refl_disj_D = thm"meson_not_refl_disj_D";
1.156
1.157 (*Is either term a Var that does not properly occur in the other term?*)
1.158 @@ -179,25 +186,25 @@
1.159 fun refl_clause_aux 0 th = th
1.160 | refl_clause_aux n th =
1.161 case HOLogic.dest_Trueprop (concl_of th) of
1.162 - (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
1.163 + (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
1.164 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
1.165 - | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
1.166 - if eliminable(t,u)
1.167 - then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
1.168 - else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
1.169 - | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
1.170 - | _ => (*not a disjunction*) th;
1.171 + | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
1.172 + if eliminable(t,u)
1.173 + then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
1.174 + else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
1.175 + | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
1.176 + | _ => (*not a disjunction*) th;
1.177
1.178 -fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
1.179 +fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
1.180 notequal_lits_count P + notequal_lits_count Q
1.181 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
1.182 | notequal_lits_count _ = 0;
1.183
1.184 (*Simplify a clause by applying reflexivity to its negated equality literals*)
1.185 -fun refl_clause th =
1.186 +fun refl_clause th =
1.187 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
1.188 in zero_var_indexes (refl_clause_aux neqs th) end
1.189 - handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
1.190 + handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
1.191
1.192
1.193 (*** The basic CNF transformation ***)
1.194 @@ -210,22 +217,22 @@
1.195 (*Estimate the number of clauses in order to detect infeasible theorems*)
1.196 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
1.197 | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
1.198 - | signed_nclauses b (Const("op &",_) $ t $ u) =
1.199 + | signed_nclauses b (Const("op &",_) $ t $ u) =
1.200 if b then sum (signed_nclauses b t) (signed_nclauses b u)
1.201 else prod (signed_nclauses b t) (signed_nclauses b u)
1.202 - | signed_nclauses b (Const("op |",_) $ t $ u) =
1.203 + | signed_nclauses b (Const("op |",_) $ t $ u) =
1.204 if b then prod (signed_nclauses b t) (signed_nclauses b u)
1.205 else sum (signed_nclauses b t) (signed_nclauses b u)
1.206 - | signed_nclauses b (Const("op -->",_) $ t $ u) =
1.207 + | signed_nclauses b (Const("op -->",_) $ t $ u) =
1.208 if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
1.209 else sum (signed_nclauses (not b) t) (signed_nclauses b u)
1.210 - | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
1.211 + | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
1.212 if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
1.213 - if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
1.214 - (prod (signed_nclauses (not b) u) (signed_nclauses b t))
1.215 - else sum (prod (signed_nclauses b t) (signed_nclauses b u))
1.216 - (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
1.217 - else 1
1.218 + if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
1.219 + (prod (signed_nclauses (not b) u) (signed_nclauses b t))
1.220 + else sum (prod (signed_nclauses b t) (signed_nclauses b u))
1.221 + (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
1.222 + else 1
1.223 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
1.224 | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
1.225 | signed_nclauses _ _ = 1; (* literal *)
1.226 @@ -247,12 +254,12 @@
1.227 (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
1.228 fun resop nf [prem] = resolve_tac (nf prem) 1;
1.229
1.230 -(*Any need to extend this list with
1.231 +(*Any need to extend this list with
1.232 "HOL.type_class","HOL.eq_class","ProtoPure.term"?*)
1.233 -val has_meta_conn =
1.234 +val has_meta_conn =
1.235 exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
1.236
1.237 -fun apply_skolem_ths (th, rls) =
1.238 +fun apply_skolem_ths (th, rls) =
1.239 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
1.240 | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
1.241 in tryall rls end;
1.242 @@ -262,28 +269,28 @@
1.243 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
1.244 fun cnf skoths (th,ths) =
1.245 let fun cnf_aux (th,ths) =
1.246 - if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
1.247 - else if not (has_conns ["All","Ex","op &"] (prop_of th))
1.248 - then th::ths (*no work to do, terminate*)
1.249 - else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
1.250 - Const ("op &", _) => (*conjunction*)
1.251 - cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
1.252 - | Const ("All", _) => (*universal quantifier*)
1.253 - cnf_aux (freeze_spec th, ths)
1.254 - | Const ("Ex", _) =>
1.255 - (*existential quantifier: Insert Skolem functions*)
1.256 - cnf_aux (apply_skolem_ths (th,skoths), ths)
1.257 - | Const ("op |", _) =>
1.258 - (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
1.259 - all combinations of converting P, Q to CNF.*)
1.260 - let val tac =
1.261 - (METAHYPS (resop cnf_nil) 1) THEN
1.262 - (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
1.263 - in Seq.list_of (tac (th RS disj_forward)) @ ths end
1.264 - | _ => (*no work to do*) th::ths
1.265 + if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
1.266 + else if not (has_conns ["All","Ex","op &"] (prop_of th))
1.267 + then th::ths (*no work to do, terminate*)
1.268 + else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
1.269 + Const ("op &", _) => (*conjunction*)
1.270 + cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
1.271 + | Const ("All", _) => (*universal quantifier*)
1.272 + cnf_aux (freeze_spec th, ths)
1.273 + | Const ("Ex", _) =>
1.274 + (*existential quantifier: Insert Skolem functions*)
1.275 + cnf_aux (apply_skolem_ths (th,skoths), ths)
1.276 + | Const ("op |", _) =>
1.277 + (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
1.278 + all combinations of converting P, Q to CNF.*)
1.279 + let val tac =
1.280 + (METAHYPS (resop cnf_nil) 1) THEN
1.281 + (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
1.282 + in Seq.list_of (tac (th RS disj_forward)) @ ths end
1.283 + | _ => (*no work to do*) th::ths
1.284 and cnf_nil th = cnf_aux (th,[])
1.285 - in
1.286 - if too_many_clauses (concl_of th)
1.287 + in
1.288 + if too_many_clauses (concl_of th)
1.289 then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
1.290 else cnf_aux (th,ths)
1.291 end;
1.292 @@ -292,7 +299,7 @@
1.293 | all_names _ = [];
1.294
1.295 fun new_names n [] = []
1.296 - | new_names n (x::xs) =
1.297 + | new_names n (x::xs) =
1.298 if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs
1.299 else new_names n xs;
1.300
1.301 @@ -302,7 +309,7 @@
1.302 let val old_names = all_names (prop_of th)
1.303 in Drule.rename_bvars (new_names 0 old_names) th end;
1.304
1.305 -(*Convert all suitable free variables to schematic variables,
1.306 +(*Convert all suitable free variables to schematic variables,
1.307 but don't discharge assumptions.*)
1.308 fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th)));
1.309
1.310 @@ -317,9 +324,9 @@
1.311 (*Forward proof, passing extra assumptions as theorems to the tactic*)
1.312 fun forward_res2 nf hyps st =
1.313 case Seq.pull
1.314 - (REPEAT
1.315 - (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
1.316 - st)
1.317 + (REPEAT
1.318 + (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
1.319 + st)
1.320 of SOME(th,_) => th
1.321 | NONE => raise THM("forward_res2", 0, [st]);
1.322
1.323 @@ -328,7 +335,7 @@
1.324 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
1.325 handle THM _ => tryres(th,rls)
1.326 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
1.327 - [disj_FalseD1, disj_FalseD2, asm_rl])
1.328 + [disj_FalseD1, disj_FalseD2, asm_rl])
1.329 handle THM _ => th;
1.330
1.331 (*Remove duplicate literals, if there are any*)
1.332 @@ -340,12 +347,12 @@
1.333
1.334 (**** Generation of contrapositives ****)
1.335
1.336 -fun is_left (Const ("Trueprop", _) $
1.337 +fun is_left (Const ("Trueprop", _) $
1.338 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
1.339 | is_left _ = false;
1.340 -
1.341 +
1.342 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
1.343 -fun assoc_right th =
1.344 +fun assoc_right th =
1.345 if is_left (prop_of th) then assoc_right (th RS disj_assoc)
1.346 else th;
1.347
1.348 @@ -369,34 +376,34 @@
1.349 fun has_bool (Type("bool",_)) = true
1.350 | has_bool (Type(_, Ts)) = exists has_bool Ts
1.351 | has_bool _ = false;
1.352 -
1.353 -(*Is the string the name of a connective? Really only | and Not can remain,
1.354 - since this code expects to be called on a clause form.*)
1.355 +
1.356 +(*Is the string the name of a connective? Really only | and Not can remain,
1.357 + since this code expects to be called on a clause form.*)
1.358 val is_conn = member (op =)
1.359 - ["Trueprop", "op &", "op |", "op -->", "Not",
1.360 + ["Trueprop", "op &", "op |", "op -->", "Not",
1.361 "All", "Ex", "Ball", "Bex"];
1.362
1.363 -(*True if the term contains a function--not a logical connective--where the type
1.364 +(*True if the term contains a function--not a logical connective--where the type
1.365 of any argument contains bool.*)
1.366 -val has_bool_arg_const =
1.367 +val has_bool_arg_const =
1.368 exists_Const
1.369 (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
1.370
1.371 -(*A higher-order instance of a first-order constant? Example is the definition of
1.372 +(*A higher-order instance of a first-order constant? Example is the definition of
1.373 HOL.one, 1, at a function type in theory SetsAndFunctions.*)
1.374 -fun higher_inst_const thy (c,T) =
1.375 +fun higher_inst_const thy (c,T) =
1.376 case binder_types T of
1.377 [] => false (*not a function type, OK*)
1.378 | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
1.379
1.380 -(*Raises an exception if any Vars in the theorem mention type bool.
1.381 +(*Raises an exception if any Vars in the theorem mention type bool.
1.382 Also rejects functions whose arguments are Booleans or other functions.*)
1.383 fun is_fol_term thy t =
1.384 Term.is_first_order ["all","All","Ex"] t andalso
1.385 not (exists (has_bool o fastype_of) (term_vars t) orelse
1.386 - has_bool_arg_const t orelse
1.387 - exists_Const (higher_inst_const thy) t orelse
1.388 - has_meta_conn t);
1.389 + has_bool_arg_const t orelse
1.390 + exists_Const (higher_inst_const thy) t orelse
1.391 + has_meta_conn t);
1.392
1.393 fun rigid t = not (is_Var (head_of t));
1.394
1.395 @@ -405,8 +412,8 @@
1.396 | ok4horn _ = false;
1.397
1.398 (*Create a meta-level Horn clause*)
1.399 -fun make_horn crules th =
1.400 - if ok4horn (concl_of th)
1.401 +fun make_horn crules th =
1.402 + if ok4horn (concl_of th)
1.403 then make_horn crules (tryres(th,crules)) handle THM _ => th
1.404 else th;
1.405
1.406 @@ -414,17 +421,17 @@
1.407 is a HOL disjunction.*)
1.408 fun add_contras crules (th,hcs) =
1.409 let fun rots (0,th) = hcs
1.410 - | rots (k,th) = zero_var_indexes (make_horn crules th) ::
1.411 - rots(k-1, assoc_right (th RS disj_comm))
1.412 + | rots (k,th) = zero_var_indexes (make_horn crules th) ::
1.413 + rots(k-1, assoc_right (th RS disj_comm))
1.414 in case nliterals(prop_of th) of
1.415 - 1 => th::hcs
1.416 + 1 => th::hcs
1.417 | n => rots(n, assoc_right th)
1.418 end;
1.419
1.420 (*Use "theorem naming" to label the clauses*)
1.421 fun name_thms label =
1.422 let fun name1 (th, (k,ths)) =
1.423 - (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
1.424 + (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
1.425 in fn ths => #2 (foldr name1 (length ths, []) ths) end;
1.426
1.427 (*Is the given disjunction an all-negative support clause?*)
1.428 @@ -436,7 +443,7 @@
1.429 (***** MESON PROOF PROCEDURE *****)
1.430
1.431 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
1.432 - As) = rhyps(phi, A::As)
1.433 + As) = rhyps(phi, A::As)
1.434 | rhyps (_, As) = As;
1.435
1.436 (** Detecting repeated assumptions in a subgoal **)
1.437 @@ -449,7 +456,7 @@
1.438 | has_reps [_] = false
1.439 | has_reps [t,u] = (t aconv u)
1.440 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
1.441 - handle Net.INSERT => true;
1.442 + handle Net.INSERT => true;
1.443
1.444 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
1.445 fun TRYING_eq_assume_tac 0 st = Seq.single st
1.446 @@ -485,8 +492,8 @@
1.447 | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
1.448 | ok4nnf _ = false;
1.449
1.450 -fun make_nnf1 th =
1.451 - if ok4nnf (concl_of th)
1.452 +fun make_nnf1 th =
1.453 + if ok4nnf (concl_of th)
1.454 then make_nnf1 (tryres(th, nnf_rls))
1.455 handle THM _ =>
1.456 forward_res make_nnf1
1.457 @@ -494,23 +501,23 @@
1.458 handle THM _ => th
1.459 else th;
1.460
1.461 -(*The simplification removes defined quantifiers and occurrences of True and False.
1.462 +(*The simplification removes defined quantifiers and occurrences of True and False.
1.463 nnf_ss also includes the one-point simprocs,
1.464 which are needed to avoid the various one-point theorems from generating junk clauses.*)
1.465 val nnf_simps =
1.466 - [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
1.467 + [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
1.468 if_False, if_cancel, if_eq_cancel, cases_simp];
1.469 val nnf_extra_simps =
1.470 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
1.471
1.472 val nnf_ss =
1.473 - HOL_basic_ss addsimps nnf_extra_simps
1.474 + HOL_basic_ss addsimps nnf_extra_simps
1.475 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
1.476
1.477 fun make_nnf th = case prems_of th of
1.478 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
1.479 - |> simplify nnf_ss
1.480 - |> make_nnf1
1.481 + |> simplify nnf_ss
1.482 + |> make_nnf1
1.483 | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
1.484
1.485 (*Pull existential quantifiers to front. This accomplishes Skolemization for
1.486 @@ -553,20 +560,20 @@
1.487
1.488 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
1.489 Function mkcl converts theorems to clauses.*)
1.490 -fun MESON mkcl cltac i st =
1.491 +fun MESON mkcl cltac i st =
1.492 SELECT_GOAL
1.493 (EVERY [ObjectLogic.atomize_prems_tac 1,
1.494 rtac ccontr 1,
1.495 - METAHYPS (fn negs =>
1.496 - EVERY1 [skolemize_prems_tac negs,
1.497 - METAHYPS (cltac o mkcl)]) 1]) i st
1.498 - handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
1.499 + METAHYPS (fn negs =>
1.500 + EVERY1 [skolemize_prems_tac negs,
1.501 + METAHYPS (cltac o mkcl)]) 1]) i st
1.502 + handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
1.503
1.504 (** Best-first search versions **)
1.505
1.506 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
1.507 fun best_meson_tac sizef =
1.508 - MESON make_clauses
1.509 + MESON make_clauses
1.510 (fn cls =>
1.511 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
1.512 (has_fewer_prems 1, sizef)
1.513 @@ -600,19 +607,19 @@
1.514 fun iter_deepen_prolog_tac horns =
1.515 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
1.516
1.517 -fun iter_deepen_meson_tac ths = MESON make_clauses
1.518 +fun iter_deepen_meson_tac ths = MESON make_clauses
1.519 (fn cls =>
1.520 case (gocls (cls@ths)) of
1.521 - [] => no_tac (*no goal clauses*)
1.522 - | goes =>
1.523 - let val horns = make_horns (cls@ths)
1.524 - val _ =
1.525 - Output.debug (fn () => ("meson method called:\n" ^
1.526 - space_implode "\n" (map string_of_thm (cls@ths)) ^
1.527 - "\nclauses:\n" ^
1.528 - space_implode "\n" (map string_of_thm horns)))
1.529 - in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
1.530 - end
1.531 + [] => no_tac (*no goal clauses*)
1.532 + | goes =>
1.533 + let val horns = make_horns (cls@ths)
1.534 + val _ =
1.535 + Output.debug (fn () => ("meson method called:\n" ^
1.536 + space_implode "\n" (map string_of_thm (cls@ths)) ^
1.537 + "\nclauses:\n" ^
1.538 + space_implode "\n" (map string_of_thm horns)))
1.539 + in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
1.540 + end
1.541 );
1.542
1.543 fun meson_claset_tac ths cs =
1.544 @@ -623,7 +630,7 @@
1.545
1.546 (**** Code to support ordinary resolution, rather than Model Elimination ****)
1.547
1.548 -(*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
1.549 +(*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
1.550 with no contrapositives, for ordinary resolution.*)
1.551
1.552 (*Rules to convert the head literal into a negated assumption. If the head
1.553 @@ -632,21 +639,21 @@
1.554 val notEfalse = read_instantiate [("R","False")] notE;
1.555 val notEfalse' = rotate_prems 1 notEfalse;
1.556
1.557 -fun negated_asm_of_head th =
1.558 +fun negated_asm_of_head th =
1.559 th RS notEfalse handle THM _ => th RS notEfalse';
1.560
1.561 (*Converting one clause*)
1.562 -val make_meta_clause =
1.563 +val make_meta_clause =
1.564 zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules;
1.565 -
1.566 +
1.567 fun make_meta_clauses ths =
1.568 name_thms "MClause#"
1.569 (distinct Thm.eq_thm_prop (map make_meta_clause ths));
1.570
1.571 (*Permute a rule's premises to move the i-th premise to the last position.*)
1.572 fun make_last i th =
1.573 - let val n = nprems_of th
1.574 - in if 1 <= i andalso i <= n
1.575 + let val n = nprems_of th
1.576 + in if 1 <= i andalso i <= n
1.577 then Thm.permute_prems (i-1) 1 th
1.578 else raise THM("select_literal", i, [th])
1.579 end;
1.580 @@ -660,17 +667,17 @@
1.581
1.582
1.583 (*Top-level Skolemization. Allows part of the conversion to clauses to be
1.584 - expressed as a tactic (or Isar method). Each assumption of the selected
1.585 + expressed as a tactic (or Isar method). Each assumption of the selected
1.586 goal is converted to NNF and then its existential quantifiers are pulled
1.587 - to the front. Finally, all existential quantifiers are eliminated,
1.588 + to the front. Finally, all existential quantifiers are eliminated,
1.589 leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
1.590 might generate many subgoals.*)
1.591
1.592 -fun skolemize_tac i st =
1.593 +fun skolemize_tac i st =
1.594 let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
1.595 - in
1.596 + in
1.597 EVERY' [METAHYPS
1.598 - (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
1.599 + (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
1.600 THEN REPEAT (etac exE 1))),
1.601 REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
1.602 end
1.603 @@ -678,5 +685,3 @@
1.604
1.605 end;
1.606
1.607 -structure BasicMeson: BASIC_MESON = Meson;
1.608 -open BasicMeson;