--- a/NEWS Fri Jun 24 16:21:01 2005 +0200
+++ b/NEWS Fri Jun 24 17:25:10 2005 +0200
@@ -342,6 +342,8 @@
enabled/disabled by the reference use_let_simproc. Potential
INCOMPATIBILITY since simplification is more powerful by default.
+* Classical reasoning: the meson method now accepts theorems as arguments.
+
*** HOLCF ***
--- a/src/HOL/Hilbert_Choice.thy Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy Fri Jun 24 17:25:10 2005 +0200
@@ -616,7 +616,7 @@
use "Tools/meson.ML"
-setup meson_setup
+setup Meson.skolemize_setup
use "Tools/specification_package.ML"
--- a/src/HOL/Induct/Comb.thy Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/Induct/Comb.thy Fri Jun 24 17:25:10 2005 +0200
@@ -95,9 +95,9 @@
"[| diamond(r); (x,y) \<in> r^* |] ==>
\<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)"
apply (unfold diamond_def)
-apply (erule rtrancl_induct, blast, clarify)
-apply (drule spec, drule mp, assumption)
-apply (blast intro: rtrancl_trans [OF _ r_into_rtrancl])
+apply (erule rtrancl_induct)
+apply (meson rtrancl_refl)
+apply (meson rtrancl_trans r_into_rtrancl)
done
lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)"
@@ -210,7 +210,7 @@
lemma parcontract_subset_reduce: "parcontract <= contract^*"
apply (rule subsetI)
apply (simp only: split_tupled_all)
-apply (erule parcontract.induct , blast+)
+apply (erule parcontract.induct, blast+)
done
lemma reduce_eq_parreduce: "contract^* = parcontract^*"
--- a/src/HOL/Induct/PropLog.thy Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/Induct/PropLog.thy Fri Jun 24 17:25:10 2005 +0200
@@ -235,20 +235,16 @@
"{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p"
apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
apply (simp add: sat_thms_p, safe)
-(*Case hyps p t-insert(#v,Y) |- p *)
- apply (rule thms_excluded_middle_rule)
- apply (rule insert_Diff_same [THEN weaken_left])
- apply (erule spec)
- apply (rule insert_Diff_subset2 [THEN weaken_left])
- apply (rule hyps_Diff [THEN Diff_weaken_left])
- apply (erule spec)
-(*Case hyps p t-insert(#v -> false,Y) |- p *)
-apply (rule thms_excluded_middle_rule)
- apply (rule_tac [2] insert_Diff_same [THEN weaken_left])
- apply (erule_tac [2] spec)
-apply (rule insert_Diff_subset2 [THEN weaken_left])
-apply (rule hyps_insert [THEN Diff_weaken_left])
-apply (erule spec)
+ txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
+ apply (rules intro: thms_excluded_middle_rule
+ insert_Diff_same [THEN weaken_left]
+ insert_Diff_subset2 [THEN weaken_left]
+ hyps_Diff [THEN Diff_weaken_left])
+txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
+ apply (rules intro: thms_excluded_middle_rule
+ insert_Diff_same [THEN weaken_left]
+ insert_Diff_subset2 [THEN weaken_left]
+ hyps_insert [THEN Diff_weaken_left])
done
text{*The base case for completeness*}
@@ -263,14 +259,12 @@
theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
apply (erule finite_induct)
-apply (safe intro!: completeness_0)
-apply (drule sat_imp)
-apply (drule spec)
-apply (blast intro: weaken_left_insert [THEN thms.MP])
+ apply (blast intro: completeness_0)
+apply (rules intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
done
theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
-by (fast elim!: soundness completeness)
+by (blast intro: soundness completeness)
end
--- a/src/HOL/Reconstruction.thy Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/Reconstruction.thy Fri Jun 24 17:25:10 2005 +0200
@@ -33,7 +33,8 @@
text{*Every theory of HOL must be a descendant or ancestor of this one!*}
-setup ResAxioms.setup
+setup ResAxioms.clause_setup
+setup ResAxioms.meson_method_setup
setup Reconstruction.setup
end
--- a/src/HOL/Tools/meson.ML Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/Tools/meson.ML Fri Jun 24 17:25:10 2005 +0200
@@ -29,13 +29,12 @@
val depth_meson_tac : int -> tactic
val prolog_step_tac' : thm list -> int -> tactic
val iter_deepen_prolog_tac : thm list -> tactic
- val iter_deepen_meson_tac : int -> tactic
+ val iter_deepen_meson_tac : thm list -> int -> tactic
val meson_tac : int -> tactic
val negate_head : thm -> thm
val select_literal : int -> thm -> thm
val skolemize_tac : int -> tactic
val make_clauses_tac : int -> tactic
- val meson_setup : (theory -> theory) list
end
@@ -61,6 +60,7 @@
val disj_FalseD1 = thm "meson_disj_FalseD1";
val disj_FalseD2 = thm "meson_disj_FalseD2";
+val depth_limit = ref 2000;
(**** Operators for forward proof ****)
@@ -250,7 +250,8 @@
fun make_horn crules th = make_horn crules (tryres(th,crules))
handle THM _ => th;
-(*Generate Horn clauses for all contrapositives of a clause*)
+(*Generate Horn clauses for all contrapositives of a clause. The input, th,
+ is a HOL disjunction.*)
fun add_contras crules (th,hcs) =
let fun rots (0,th) = hcs
| rots (k,th) = zero_var_indexes (make_horn crules th) ::
@@ -267,7 +268,7 @@
in fn ths => #2 (foldr name1 (length ths, []) ths) end;
-(*Find an all-negative support clause*)
+(*Is the given disjunction an all-negative support clause?*)
fun is_negative th = forall (not o #1) (literals (prop_of th));
val neg_clauses = List.filter is_negative;
@@ -349,7 +350,7 @@
(sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
-(*Convert a list of clauses to (contrapositive) Horn clauses*)
+(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
fun make_horns ths =
name_thms "Horn#"
(gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
@@ -366,7 +367,6 @@
(*Return all negative clauses, as possible goal clauses*)
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
-
fun skolemize_prems_tac prems =
cut_facts_tac (map (skolemize o make_nnf) prems) THEN'
REPEAT o (etac exE);
@@ -380,6 +380,7 @@
(** Best-first search versions **)
+(*ths is a list of additional clauses (HOL disjunctions) to use.*)
fun best_meson_tac sizef =
MESON (fn cls =>
THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
@@ -398,7 +399,6 @@
depth_prolog_tac (make_horns cls)]);
-
(** Iterative deepening version **)
(*This version does only one inference per call;
@@ -415,16 +415,19 @@
fun iter_deepen_prolog_tac horns =
ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
-val iter_deepen_meson_tac =
+fun iter_deepen_meson_tac ths =
MESON (fn cls =>
- (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
- (has_fewer_prems 1)
- (prolog_step_tac' (make_horns cls))));
+ case (gocls (cls@ths)) of
+ [] => no_tac (*no goal clauses*)
+ | goes =>
+ (THEN_ITER_DEEPEN (resolve_tac goes 1)
+ (has_fewer_prems 1)
+ (prolog_step_tac' (make_horns (cls@ths)))));
-fun meson_claset_tac cs =
- SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac);
+fun meson_claset_tac ths cs =
+ SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
-val meson_tac = CLASET' meson_claset_tac;
+val meson_tac = CLASET' (meson_claset_tac []);
(**** Code to support ordinary resolution, rather than Model Elimination ****)
@@ -496,28 +499,19 @@
(make_meta_clauses (make_clauses hyps))) 1)),
REPEAT_DETERM_N (length ts) o (etac thin_rl)]
end);
-
-
-(*** proof method setup ***)
+
+
+(*** setup the special skoklemization methods ***)
-fun meson_meth ctxt =
- Method.SIMPLE_METHOD' HEADGOAL
- (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt));
+(*No CHANGED_PROP here, since these always appear in the preamble*)
-val skolemize_meth =
- Method.SIMPLE_METHOD' HEADGOAL
- (CHANGED_PROP o skolemize_tac);
+val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
+
+val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
-val make_clauses_meth =
- Method.SIMPLE_METHOD' HEADGOAL
- (CHANGED_PROP o make_clauses_tac);
-
-
-val meson_setup =
+val skolemize_setup =
[Method.add_methods
- [("meson", Method.ctxt_args meson_meth,
- "The MESON resolution proof procedure"),
- ("skolemize", Method.no_args skolemize_meth,
+ [("skolemize", Method.no_args skolemize_meth,
"Skolemization into existential quantifiers"),
("make_clauses", Method.no_args make_clauses_meth,
"Conversion to !!-quantified meta-level clauses")]];
--- a/src/HOL/Tools/res_axioms.ML Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Jun 24 17:25:10 2005 +0200
@@ -15,6 +15,8 @@
val cnf_axiom : (string * thm) -> thm list
val meta_cnf_axiom : thm -> thm list
val cnf_rule : thm -> thm list
+ val cnf_rules : (string*thm) list -> thm list -> thm list list * thm list
+
val cnf_classical_rules_thy : theory -> thm list list * thm list
val cnf_simpset_rules_thy : theory -> thm list list * thm list
@@ -23,7 +25,8 @@
val claset_rules_of_thy : theory -> (string * thm) list
val simpset_rules_of_thy : theory -> (string * thm) list
val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list
- val setup : (theory -> theory) list
+ val clause_setup : (theory -> theory) list
+ val meson_method_setup : (theory -> theory) list
end;
structure ResAxioms : RES_AXIOMS =
@@ -138,10 +141,7 @@
prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
end
- else th;;
-
-
-
+ else th;
(**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
@@ -169,13 +169,16 @@
fun cnf_rule th = make_clauses [skolem_axiom (transform_elim th)];
-(*Transfer a theorem in to theory Reconstruction.thy if it is not already
+(*Transfer a theorem into theory Reconstruction.thy if it is not already
inside that theory -- because it's needed for Skolemization *)
-val recon_thy = ThyInfo.get_theory"Reconstruction";
+(*This will refer to the final version of theory Reconstruction.*)
+val recon_thy_ref = Theory.self_ref (the_context ());
+(*If called while Reconstruction is being created, it will transfer to the
+ current version. If called afterward, it will transfer to the final version.*)
fun transfer_to_Reconstruction th =
- transfer recon_thy th handle THM _ => th;
+ transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
fun is_taut th =
case (prop_of th) of
@@ -254,7 +257,8 @@
(*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*)
fun to_nnf thy th =
if Term.is_first_order (prop_of th) then
- th |> Thm.transfer thy |> transform_elim |> Drule.freeze_all
+ th |> Thm.transfer thy
+ |> transform_elim |> Drule.freeze_all
|> ObjectLogic.atomize_thm |> make_nnf
else raise THM ("to_nnf: not first-order", 0, [th]);
@@ -397,18 +401,6 @@
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
(* outputs a list of (clause,thm) pairs *)
-(*fun clausify_axiom_pairs (thm_name,thm) =
- let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
- val isa_clauses' = rm_Eps [] isa_clauses
- val clauses_n = length isa_clauses
- fun make_axiom_clauses _ [] []= []
- | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls', thm_name, i) :: make_axiom_clauses (i+1) clss clss'
- in
- make_axiom_clauses 0 isa_clauses' isa_clauses
- end;
-*)
-
-
fun clausify_axiom_pairs (thm_name,thm) =
let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
val isa_clauses' = rm_Eps [] isa_clauses
@@ -435,6 +427,20 @@
and clas = claset_rules_of_thy thy
in skolemlist clas (skolemlist simps thy) end;
-val setup = [clause_cache_setup];
+val clause_setup = [clause_cache_setup];
+
+
+(*** meson proof methods ***)
+
+fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) []));
+
+fun meson_meth ths ctxt =
+ Method.SIMPLE_METHOD' HEADGOAL
+ (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
+
+val meson_method_setup =
+ [Method.add_methods
+ [("meson", Method.thms_ctxt_args meson_meth,
+ "The MESON resolution proof procedure")]];
end;
--- a/src/HOL/ex/Classical.thy Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/ex/Classical.thy Fri Jun 24 17:25:10 2005 +0200
@@ -422,6 +422,11 @@
subsection{*Model Elimination Prover*}
+
+text{*Trying out meson with arguments*}
+lemma "x < y & y < z --> ~ (z < (x::nat))"
+by (meson order_less_irrefl order_less_trans)
+
text{*The "small example" from Bezem, Hendriks and de Nivelle,
Automatic Proof Construction in Type Theory Using Resolution,
JAR 29: 3-4 (2002), pages 253-275 *}
--- a/src/HOL/ex/Primrec.thy Fri Jun 24 16:21:01 2005 +0200
+++ b/src/HOL/ex/Primrec.thy Fri Jun 24 17:25:10 2005 +0200
@@ -286,12 +286,8 @@
==> \<exists>k. \<forall>l. COMP g fs l < ack(k, list_add l)"
apply (unfold COMP_def)
apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
- apply (erule COMP_map_aux [THEN exE])
- apply (rule exI)
- apply (rule allI)
- apply (drule spec)+
- apply (erule less_trans)
- apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
+ apply (drule COMP_map_aux)
+ apply (meson ack_less_mono2 ack_nest_bound less_trans)
done