1.1 --- a/src/HOL/Tools/meson.ML Tue Oct 09 17:11:20 2007 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Tue Oct 09 18:14:00 2007 +0200
1.3 @@ -6,9 +6,6 @@
1.4 The MESON resolution proof procedure for HOL.
1.5
1.6 When making clauses, avoids using the rewriter -- instead uses RS recursively
1.7 -
1.8 -NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E. ELIMINATES NEED FOR
1.9 -FUNCTION nodups -- if done to goal clauses too!
1.10 *)
1.11
1.12 signature MESON =
1.13 @@ -18,9 +15,8 @@
1.14 val flexflex_first_order: thm -> thm
1.15 val size_of_subgoals: thm -> int
1.16 val too_many_clauses: term -> bool
1.17 - val make_cnf: thm list -> thm -> thm list
1.18 + val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
1.19 val finish_cnf: thm list -> thm list
1.20 - val generalize: thm -> thm
1.21 val make_nnf: thm -> thm
1.22 val make_nnf1: thm -> thm
1.23 val skolemize: thm -> thm
1.24 @@ -102,10 +98,15 @@
1.25 in th' end
1.26 handle THM _ => th;
1.27
1.28 -(*raises exception if no rules apply -- unlike RL*)
1.29 +(*Forward proof while preserving bound variables names*)
1.30 +fun rename_bvs_RS th rl =
1.31 + let val th' = th RS rl
1.32 + in Thm.rename_boundvars (concl_of th') (concl_of th) th' end;
1.33 +
1.34 +(*raises exception if no rules apply*)
1.35 fun tryres (th, rls) =
1.36 let fun tryall [] = raise THM("tryres", 0, th::rls)
1.37 - | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
1.38 + | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls)
1.39 in tryall rls end;
1.40
1.41 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
1.42 @@ -208,6 +209,32 @@
1.43 handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
1.44
1.45
1.46 +(*** Removal of duplicate literals ***)
1.47 +
1.48 +(*Forward proof, passing extra assumptions as theorems to the tactic*)
1.49 +fun forward_res2 nf hyps st =
1.50 + case Seq.pull
1.51 + (REPEAT
1.52 + (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
1.53 + st)
1.54 + of SOME(th,_) => th
1.55 + | NONE => raise THM("forward_res2", 0, [st]);
1.56 +
1.57 +(*Remove duplicates in P|Q by assuming ~P in Q
1.58 + rls (initially []) accumulates assumptions of the form P==>False*)
1.59 +fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
1.60 + handle THM _ => tryres(th,rls)
1.61 + handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
1.62 + [disj_FalseD1, disj_FalseD2, asm_rl])
1.63 + handle THM _ => th;
1.64 +
1.65 +(*Remove duplicate literals, if there are any*)
1.66 +fun nodups th =
1.67 + if has_duplicates (op =) (literals (prop_of th))
1.68 + then nodups_aux [] th
1.69 + else th;
1.70 +
1.71 +
1.72 (*** The basic CNF transformation ***)
1.73
1.74 val max_clauses = 40;
1.75 @@ -243,11 +270,19 @@
1.76 fun too_many_clauses t = nclauses t >= max_clauses;
1.77
1.78 (*Replaces universally quantified variables by FREE variables -- because
1.79 - assumptions may not contain scheme variables. Later, we call "generalize". *)
1.80 -fun freeze_spec th =
1.81 - let val newname = gensym "mes_"
1.82 - val spec' = read_instantiate [("x", newname)] spec
1.83 - in th RS spec' end;
1.84 + assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
1.85 +local
1.86 + val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
1.87 + val spec_varT = #T (Thm.rep_cterm spec_var);
1.88 + fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
1.89 +in
1.90 + fun freeze_spec th ctxt =
1.91 + let
1.92 + val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
1.93 + val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
1.94 + val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
1.95 + in (th RS spec', ctxt') end
1.96 +end;
1.97
1.98 (*Used with METAHYPS below. There is one assumption, which gets bound to prem
1.99 and then normalized via function nf. The normal form is given to resolve_tac,
1.100 @@ -268,16 +303,18 @@
1.101 (*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
1.102 Strips universal quantifiers and breaks up conjunctions.
1.103 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
1.104 -fun cnf skoths (th,ths) =
1.105 - let fun cnf_aux (th,ths) =
1.106 +fun cnf skoths ctxt (th,ths) =
1.107 + let val ctxtr = ref ctxt
1.108 + fun cnf_aux (th,ths) =
1.109 if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
1.110 else if not (has_conns ["All","Ex","op &"] (prop_of th))
1.111 - then th::ths (*no work to do, terminate*)
1.112 + then nodups th :: ths (*no work to do, terminate*)
1.113 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
1.114 Const ("op &", _) => (*conjunction*)
1.115 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
1.116 | Const ("All", _) => (*universal quantifier*)
1.117 - cnf_aux (freeze_spec th, ths)
1.118 + let val (th',ctxt') = freeze_spec th (!ctxtr)
1.119 + in ctxtr := ctxt'; cnf_aux (th', ths) end
1.120 | Const ("Ex", _) =>
1.121 (*existential quantifier: Insert Skolem functions*)
1.122 cnf_aux (apply_skolem_ths (th,skoths), ths)
1.123 @@ -288,62 +325,18 @@
1.124 (METAHYPS (resop cnf_nil) 1) THEN
1.125 (fn st' => st' |> METAHYPS (resop cnf_nil) 1)
1.126 in Seq.list_of (tac (th RS disj_forward)) @ ths end
1.127 - | _ => (*no work to do*) th::ths
1.128 + | _ => nodups th :: ths (*no work to do*)
1.129 and cnf_nil th = cnf_aux (th,[])
1.130 - in
1.131 - if too_many_clauses (concl_of th)
1.132 - then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
1.133 - else cnf_aux (th,ths)
1.134 - end;
1.135 + val cls =
1.136 + if too_many_clauses (concl_of th)
1.137 + then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
1.138 + else cnf_aux (th,ths)
1.139 + in (cls, !ctxtr) end;
1.140
1.141 -fun all_names (Const ("all", _) $ Abs(x,_,P)) = x :: all_names P
1.142 - | all_names _ = [];
1.143 -
1.144 -fun new_names n [] = []
1.145 - | new_names n (x::xs) =
1.146 - if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs
1.147 - else new_names n xs;
1.148 -
1.149 -(*The gensym names are ugly, so don't let the user see them. When forall_elim_vars
1.150 - is called, it will ensure that no name clauses ensue.*)
1.151 -fun nice_names th =
1.152 - let val old_names = all_names (prop_of th)
1.153 - in Drule.rename_bvars (new_names 0 old_names) th end;
1.154 -
1.155 -(*Convert all suitable free variables to schematic variables,
1.156 - but don't discharge assumptions.*)
1.157 -fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th)));
1.158 -
1.159 -fun make_cnf skoths th = cnf skoths (th, []);
1.160 +fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
1.161
1.162 (*Generalization, removal of redundant equalities, removal of tautologies.*)
1.163 -fun finish_cnf ths = filter (not o is_taut) (map (refl_clause o generalize) ths);
1.164 -
1.165 -
1.166 -(**** Removal of duplicate literals ****)
1.167 -
1.168 -(*Forward proof, passing extra assumptions as theorems to the tactic*)
1.169 -fun forward_res2 nf hyps st =
1.170 - case Seq.pull
1.171 - (REPEAT
1.172 - (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
1.173 - st)
1.174 - of SOME(th,_) => th
1.175 - | NONE => raise THM("forward_res2", 0, [st]);
1.176 -
1.177 -(*Remove duplicates in P|Q by assuming ~P in Q
1.178 - rls (initially []) accumulates assumptions of the form P==>False*)
1.179 -fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
1.180 - handle THM _ => tryres(th,rls)
1.181 - handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
1.182 - [disj_FalseD1, disj_FalseD2, asm_rl])
1.183 - handle THM _ => th;
1.184 -
1.185 -(*Remove duplicate literals, if there are any*)
1.186 -fun nodups th =
1.187 - if has_duplicates (op =) (literals (prop_of th))
1.188 - then nodups_aux [] th
1.189 - else th;
1.190 +fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
1.191
1.192
1.193 (**** Generation of contrapositives ****)
1.194 @@ -530,13 +523,16 @@
1.195 handle THM _ =>
1.196 skolemize (forward_res skolemize
1.197 (tryres (th, [conj_forward, disj_forward, all_forward])))
1.198 - handle THM _ => forward_res skolemize (th RS ex_forward);
1.199 + handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward);
1.200
1.201 +fun add_clauses (th,cls) =
1.202 + let val ctxt0 = Variable.thm_context th
1.203 + val (cnfs,ctxt) = make_cnf [] th ctxt0
1.204 + in Variable.export ctxt ctxt0 cnfs @ cls end;
1.205
1.206 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
1.207 The resulting clauses are HOL disjunctions.*)
1.208 -fun make_clauses ths =
1.209 - (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
1.210 +fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
1.211
1.212 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
1.213 fun make_horns ths =