# HG changeset patch # User paulson # Date 1119626710 -7200 # Node ID a92f96951355768148afd997e94937aa5255144d # Parent b74143e10410af78c2fd15f89e1b06517480577d meson method taking an argument list diff -r b74143e10410 -r a92f96951355 NEWS --- 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 *** diff -r b74143e10410 -r a92f96951355 src/HOL/Hilbert_Choice.thy --- 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" diff -r b74143e10410 -r a92f96951355 src/HOL/Induct/Comb.thy --- 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) \ r^* |] ==> \y'. (x,y') \ r --> (\z. (y',z) \ r^* & (y,z) \ 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^*" diff -r b74143e10410 -r a92f96951355 src/HOL/Induct/PropLog.thy --- 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 ==> \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 ==> \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 diff -r b74143e10410 -r a92f96951355 src/HOL/Reconstruction.thy --- 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 diff -r b74143e10410 -r a92f96951355 src/HOL/Tools/meson.ML --- 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")]]; diff -r b74143e10410 -r a92f96951355 src/HOL/Tools/res_axioms.ML --- 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; diff -r b74143e10410 -r a92f96951355 src/HOL/ex/Classical.thy --- 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 *} diff -r b74143e10410 -r a92f96951355 src/HOL/ex/Primrec.thy --- 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 @@ ==> \k. \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