meson method taking an argument list
authorpaulson
Fri Jun 24 17:25:10 2005 +0200 (2005-06-24)
changeset 16563a92f96951355
parent 16562 b74143e10410
child 16564 6fc73c9dd5f4
meson method taking an argument list
NEWS
src/HOL/Hilbert_Choice.thy
src/HOL/Induct/Comb.thy
src/HOL/Induct/PropLog.thy
src/HOL/Reconstruction.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_axioms.ML
src/HOL/ex/Classical.thy
src/HOL/ex/Primrec.thy
     1.1 --- a/NEWS	Fri Jun 24 16:21:01 2005 +0200
     1.2 +++ b/NEWS	Fri Jun 24 17:25:10 2005 +0200
     1.3 @@ -342,6 +342,8 @@
     1.4  enabled/disabled by the reference use_let_simproc.  Potential
     1.5  INCOMPATIBILITY since simplification is more powerful by default.
     1.6  
     1.7 +* Classical reasoning: the meson method now accepts theorems as arguments.
     1.8 +
     1.9  
    1.10  *** HOLCF ***
    1.11  
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Jun 24 16:21:01 2005 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Jun 24 17:25:10 2005 +0200
     2.3 @@ -616,7 +616,7 @@
     2.4  
     2.5  
     2.6  use "Tools/meson.ML"
     2.7 -setup meson_setup
     2.8 +setup Meson.skolemize_setup
     2.9  
    2.10  use "Tools/specification_package.ML"
    2.11  
     3.1 --- a/src/HOL/Induct/Comb.thy	Fri Jun 24 16:21:01 2005 +0200
     3.2 +++ b/src/HOL/Induct/Comb.thy	Fri Jun 24 17:25:10 2005 +0200
     3.3 @@ -95,9 +95,9 @@
     3.4      "[| diamond(r);  (x,y) \<in> r^* |] ==>   
     3.5            \<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)"
     3.6  apply (unfold diamond_def)
     3.7 -apply (erule rtrancl_induct, blast, clarify)
     3.8 -apply (drule spec, drule mp, assumption)
     3.9 -apply (blast intro: rtrancl_trans [OF _ r_into_rtrancl])
    3.10 +apply (erule rtrancl_induct)
    3.11 +apply (meson rtrancl_refl)
    3.12 +apply (meson rtrancl_trans r_into_rtrancl)
    3.13  done
    3.14  
    3.15  lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)"
    3.16 @@ -210,7 +210,7 @@
    3.17  lemma parcontract_subset_reduce: "parcontract <= contract^*"
    3.18  apply (rule subsetI)
    3.19  apply (simp only: split_tupled_all)
    3.20 -apply (erule parcontract.induct , blast+)
    3.21 +apply (erule parcontract.induct, blast+)
    3.22  done
    3.23  
    3.24  lemma reduce_eq_parreduce: "contract^* = parcontract^*"
     4.1 --- a/src/HOL/Induct/PropLog.thy	Fri Jun 24 16:21:01 2005 +0200
     4.2 +++ b/src/HOL/Induct/PropLog.thy	Fri Jun 24 17:25:10 2005 +0200
     4.3 @@ -235,20 +235,16 @@
     4.4      "{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p" 
     4.5  apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
     4.6   apply (simp add: sat_thms_p, safe)
     4.7 -(*Case hyps p t-insert(#v,Y) |- p *)
     4.8 - apply (rule thms_excluded_middle_rule)
     4.9 -  apply (rule insert_Diff_same [THEN weaken_left])
    4.10 -  apply (erule spec)
    4.11 - apply (rule insert_Diff_subset2 [THEN weaken_left])
    4.12 - apply (rule hyps_Diff [THEN Diff_weaken_left])
    4.13 - apply (erule spec)
    4.14 -(*Case hyps p t-insert(#v -> false,Y) |- p *)
    4.15 -apply (rule thms_excluded_middle_rule)
    4.16 - apply (rule_tac [2] insert_Diff_same [THEN weaken_left])
    4.17 - apply (erule_tac [2] spec)
    4.18 -apply (rule insert_Diff_subset2 [THEN weaken_left])
    4.19 -apply (rule hyps_insert [THEN Diff_weaken_left])
    4.20 -apply (erule spec)
    4.21 + txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
    4.22 + apply (rules intro: thms_excluded_middle_rule 
    4.23 +		     insert_Diff_same [THEN weaken_left]
    4.24 +                     insert_Diff_subset2 [THEN weaken_left] 
    4.25 +                     hyps_Diff [THEN Diff_weaken_left])
    4.26 +txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
    4.27 + apply (rules intro: thms_excluded_middle_rule 
    4.28 +		     insert_Diff_same [THEN weaken_left]
    4.29 +                     insert_Diff_subset2 [THEN weaken_left] 
    4.30 +                     hyps_insert [THEN Diff_weaken_left])
    4.31  done
    4.32  
    4.33  text{*The base case for completeness*}
    4.34 @@ -263,14 +259,12 @@
    4.35  
    4.36  theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
    4.37  apply (erule finite_induct)
    4.38 -apply (safe intro!: completeness_0)
    4.39 -apply (drule sat_imp)
    4.40 -apply (drule spec) 
    4.41 -apply (blast intro: weaken_left_insert [THEN thms.MP])  
    4.42 + apply (blast intro: completeness_0)
    4.43 +apply (rules intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
    4.44  done
    4.45  
    4.46  theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
    4.47 -by (fast elim!: soundness completeness)
    4.48 +by (blast intro: soundness completeness)
    4.49  
    4.50  end
    4.51  
     5.1 --- a/src/HOL/Reconstruction.thy	Fri Jun 24 16:21:01 2005 +0200
     5.2 +++ b/src/HOL/Reconstruction.thy	Fri Jun 24 17:25:10 2005 +0200
     5.3 @@ -33,7 +33,8 @@
     5.4  
     5.5  text{*Every theory of HOL must be a descendant or ancestor of this one!*}
     5.6  
     5.7 -setup ResAxioms.setup
     5.8 +setup ResAxioms.clause_setup
     5.9 +setup ResAxioms.meson_method_setup
    5.10  setup Reconstruction.setup
    5.11  
    5.12  end
     6.1 --- a/src/HOL/Tools/meson.ML	Fri Jun 24 16:21:01 2005 +0200
     6.2 +++ b/src/HOL/Tools/meson.ML	Fri Jun 24 17:25:10 2005 +0200
     6.3 @@ -29,13 +29,12 @@
     6.4    val depth_meson_tac	: int -> tactic
     6.5    val prolog_step_tac'	: thm list -> int -> tactic
     6.6    val iter_deepen_prolog_tac	: thm list -> tactic
     6.7 -  val iter_deepen_meson_tac	: int -> tactic
     6.8 +  val iter_deepen_meson_tac	: thm list -> int -> tactic
     6.9    val meson_tac		: int -> tactic
    6.10    val negate_head	: thm -> thm
    6.11    val select_literal	: int -> thm -> thm
    6.12    val skolemize_tac	: int -> tactic
    6.13    val make_clauses_tac	: int -> tactic
    6.14 -  val meson_setup	: (theory -> theory) list
    6.15  end
    6.16  
    6.17  
    6.18 @@ -61,6 +60,7 @@
    6.19  val disj_FalseD1 = thm "meson_disj_FalseD1";
    6.20  val disj_FalseD2 = thm "meson_disj_FalseD2";
    6.21  
    6.22 +val depth_limit = ref 2000;
    6.23  
    6.24  (**** Operators for forward proof ****)
    6.25  
    6.26 @@ -250,7 +250,8 @@
    6.27  fun make_horn crules th = make_horn crules (tryres(th,crules))
    6.28  			  handle THM _ => th;
    6.29  
    6.30 -(*Generate Horn clauses for all contrapositives of a clause*)
    6.31 +(*Generate Horn clauses for all contrapositives of a clause. The input, th,
    6.32 +  is a HOL disjunction.*)
    6.33  fun add_contras crules (th,hcs) =
    6.34    let fun rots (0,th) = hcs
    6.35  	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
    6.36 @@ -267,7 +268,7 @@
    6.37  
    6.38      in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    6.39  
    6.40 -(*Find an all-negative support clause*)
    6.41 +(*Is the given disjunction an all-negative support clause?*)
    6.42  fun is_negative th = forall (not o #1) (literals (prop_of th));
    6.43  
    6.44  val neg_clauses = List.filter is_negative;
    6.45 @@ -349,7 +350,7 @@
    6.46      (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
    6.47  
    6.48  
    6.49 -(*Convert a list of clauses to (contrapositive) Horn clauses*)
    6.50 +(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    6.51  fun make_horns ths =
    6.52      name_thms "Horn#"
    6.53        (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
    6.54 @@ -366,7 +367,6 @@
    6.55  (*Return all negative clauses, as possible goal clauses*)
    6.56  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    6.57  
    6.58 -
    6.59  fun skolemize_prems_tac prems =
    6.60      cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
    6.61      REPEAT o (etac exE);
    6.62 @@ -380,6 +380,7 @@
    6.63  
    6.64  (** Best-first search versions **)
    6.65  
    6.66 +(*ths is a list of additional clauses (HOL disjunctions) to use.*)
    6.67  fun best_meson_tac sizef =
    6.68    MESON (fn cls =>
    6.69           THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
    6.70 @@ -398,7 +399,6 @@
    6.71                               depth_prolog_tac (make_horns cls)]);
    6.72  
    6.73  
    6.74 -
    6.75  (** Iterative deepening version **)
    6.76  
    6.77  (*This version does only one inference per call;
    6.78 @@ -415,16 +415,19 @@
    6.79  fun iter_deepen_prolog_tac horns =
    6.80      ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
    6.81  
    6.82 -val iter_deepen_meson_tac =
    6.83 +fun iter_deepen_meson_tac ths =
    6.84    MESON (fn cls =>
    6.85 -         (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
    6.86 -                           (has_fewer_prems 1)
    6.87 -                           (prolog_step_tac' (make_horns cls))));
    6.88 +           case (gocls (cls@ths)) of
    6.89 +           	[] => no_tac  (*no goal clauses*)
    6.90 +              | goes => 
    6.91 +		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
    6.92 +				   (has_fewer_prems 1)
    6.93 +				   (prolog_step_tac' (make_horns (cls@ths)))));
    6.94  
    6.95 -fun meson_claset_tac cs =
    6.96 -  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac);
    6.97 +fun meson_claset_tac ths cs =
    6.98 +  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
    6.99  
   6.100 -val meson_tac = CLASET' meson_claset_tac;
   6.101 +val meson_tac = CLASET' (meson_claset_tac []);
   6.102  
   6.103  
   6.104  (**** Code to support ordinary resolution, rather than Model Elimination ****)
   6.105 @@ -496,28 +499,19 @@
   6.106                    (make_meta_clauses (make_clauses hyps))) 1)),
   6.107  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   6.108       end);
   6.109 -
   6.110 -
   6.111 -(*** proof method setup ***)
   6.112 +     
   6.113 +     
   6.114 +(*** setup the special skoklemization methods ***)
   6.115  
   6.116 -fun meson_meth ctxt =
   6.117 -  Method.SIMPLE_METHOD' HEADGOAL
   6.118 -    (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt));
   6.119 +(*No CHANGED_PROP here, since these always appear in the preamble*)
   6.120  
   6.121 -val skolemize_meth =
   6.122 -  Method.SIMPLE_METHOD' HEADGOAL
   6.123 -    (CHANGED_PROP o skolemize_tac);
   6.124 +val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
   6.125 +
   6.126 +val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   6.127  
   6.128 -val make_clauses_meth =
   6.129 -  Method.SIMPLE_METHOD' HEADGOAL
   6.130 -    (CHANGED_PROP o make_clauses_tac);
   6.131 -
   6.132 -
   6.133 -val meson_setup =
   6.134 +val skolemize_setup =
   6.135   [Method.add_methods
   6.136 -  [("meson", Method.ctxt_args meson_meth, 
   6.137 -    "The MESON resolution proof procedure"),
   6.138 -   ("skolemize", Method.no_args skolemize_meth, 
   6.139 +  [("skolemize", Method.no_args skolemize_meth, 
   6.140      "Skolemization into existential quantifiers"),
   6.141     ("make_clauses", Method.no_args make_clauses_meth, 
   6.142      "Conversion to !!-quantified meta-level clauses")]];
     7.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Jun 24 16:21:01 2005 +0200
     7.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Jun 24 17:25:10 2005 +0200
     7.3 @@ -15,6 +15,8 @@
     7.4    val cnf_axiom : (string * thm) -> thm list
     7.5    val meta_cnf_axiom : thm -> thm list
     7.6    val cnf_rule : thm -> thm list
     7.7 +  val cnf_rules : (string*thm) list -> thm list -> thm list list * thm list
     7.8 +
     7.9    val cnf_classical_rules_thy : theory -> thm list list * thm list
    7.10   
    7.11    val cnf_simpset_rules_thy : theory -> thm list list * thm list
    7.12 @@ -23,7 +25,8 @@
    7.13    val claset_rules_of_thy : theory -> (string * thm) list
    7.14    val simpset_rules_of_thy : theory -> (string * thm) list
    7.15    val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list
    7.16 -  val setup : (theory -> theory) list
    7.17 +  val clause_setup : (theory -> theory) list
    7.18 +  val meson_method_setup : (theory -> theory) list
    7.19    end;
    7.20  
    7.21  structure ResAxioms : RES_AXIOMS =
    7.22 @@ -138,10 +141,7 @@
    7.23  
    7.24  	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
    7.25      end
    7.26 - else th;;	
    7.27 -
    7.28 -
    7.29 -
    7.30 + else th;
    7.31  
    7.32  
    7.33  (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    7.34 @@ -169,13 +169,16 @@
    7.35  
    7.36  fun cnf_rule th = make_clauses [skolem_axiom (transform_elim th)];
    7.37  
    7.38 -(*Transfer a theorem in to theory Reconstruction.thy if it is not already
    7.39 +(*Transfer a theorem into theory Reconstruction.thy if it is not already
    7.40    inside that theory -- because it's needed for Skolemization *)
    7.41  
    7.42 -val recon_thy = ThyInfo.get_theory"Reconstruction";
    7.43 +(*This will refer to the final version of theory Reconstruction.*)
    7.44 +val recon_thy_ref = Theory.self_ref (the_context ());  
    7.45  
    7.46 +(*If called while Reconstruction is being created, it will transfer to the
    7.47 +  current version. If called afterward, it will transfer to the final version.*)
    7.48  fun transfer_to_Reconstruction th =
    7.49 -    transfer recon_thy th handle THM _ => th;
    7.50 +    transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
    7.51  
    7.52  fun is_taut th =
    7.53        case (prop_of th) of
    7.54 @@ -254,7 +257,8 @@
    7.55  (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*)
    7.56  fun to_nnf thy th = 
    7.57      if Term.is_first_order (prop_of th) then
    7.58 -      th |> Thm.transfer thy |> transform_elim |> Drule.freeze_all
    7.59 +      th |> Thm.transfer thy
    7.60 +         |> transform_elim |> Drule.freeze_all
    7.61  	 |> ObjectLogic.atomize_thm |> make_nnf
    7.62      else raise THM ("to_nnf: not first-order", 0, [th]);
    7.63  
    7.64 @@ -397,18 +401,6 @@
    7.65  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
    7.66  
    7.67  (* outputs a list of (clause,thm) pairs *)
    7.68 -(*fun clausify_axiom_pairs (thm_name,thm) =
    7.69 -    let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
    7.70 -        val isa_clauses' = rm_Eps [] isa_clauses
    7.71 -        val clauses_n = length isa_clauses
    7.72 -	fun make_axiom_clauses _ [] []= []
    7.73 -	  | 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'
    7.74 -    in
    7.75 -	make_axiom_clauses 0 isa_clauses' isa_clauses		
    7.76 -    end;
    7.77 -*)
    7.78 -
    7.79 -
    7.80  fun clausify_axiom_pairs (thm_name,thm) =
    7.81      let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
    7.82          val isa_clauses' = rm_Eps [] isa_clauses
    7.83 @@ -435,6 +427,20 @@
    7.84        and clas  = claset_rules_of_thy thy
    7.85    in skolemlist clas (skolemlist simps thy) end;
    7.86    
    7.87 -val setup = [clause_cache_setup];  
    7.88 +val clause_setup = [clause_cache_setup];  
    7.89 +
    7.90 +
    7.91 +(*** meson proof methods ***)
    7.92 +
    7.93 +fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) []));
    7.94 +
    7.95 +fun meson_meth ths ctxt =
    7.96 +  Method.SIMPLE_METHOD' HEADGOAL
    7.97 +    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
    7.98 +
    7.99 +val meson_method_setup =
   7.100 + [Method.add_methods
   7.101 +  [("meson", Method.thms_ctxt_args meson_meth, 
   7.102 +    "The MESON resolution proof procedure")]];
   7.103  
   7.104  end; 
     8.1 --- a/src/HOL/ex/Classical.thy	Fri Jun 24 16:21:01 2005 +0200
     8.2 +++ b/src/HOL/ex/Classical.thy	Fri Jun 24 17:25:10 2005 +0200
     8.3 @@ -422,6 +422,11 @@
     8.4  
     8.5  subsection{*Model Elimination Prover*}
     8.6  
     8.7 +
     8.8 +text{*Trying out meson with arguments*}
     8.9 +lemma "x < y & y < z --> ~ (z < (x::nat))"
    8.10 +by (meson order_less_irrefl order_less_trans)
    8.11 +
    8.12  text{*The "small example" from Bezem, Hendriks and de Nivelle,
    8.13  Automatic Proof Construction in Type Theory Using Resolution,
    8.14  JAR 29: 3-4 (2002), pages 253-275 *}
     9.1 --- a/src/HOL/ex/Primrec.thy	Fri Jun 24 16:21:01 2005 +0200
     9.2 +++ b/src/HOL/ex/Primrec.thy	Fri Jun 24 17:25:10 2005 +0200
     9.3 @@ -286,12 +286,8 @@
     9.4    ==> \<exists>k. \<forall>l. COMP g fs  l < ack(k, list_add l)"
     9.5    apply (unfold COMP_def)
     9.6    apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
     9.7 -  apply (erule COMP_map_aux [THEN exE])
     9.8 -  apply (rule exI)
     9.9 -  apply (rule allI)
    9.10 -  apply (drule spec)+
    9.11 -  apply (erule less_trans)
    9.12 -  apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
    9.13 +  apply (drule COMP_map_aux)
    9.14 +  apply (meson ack_less_mono2 ack_nest_bound less_trans)
    9.15    done
    9.16  
    9.17