src/HOL/Tools/meson.ML
changeset 16563 a92f96951355
parent 16173 9e2f6c0a779d
child 16588 8de758143786
     1.1 --- a/src/HOL/Tools/meson.ML	Fri Jun 24 16:21:01 2005 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Jun 24 17:25:10 2005 +0200
     1.3 @@ -29,13 +29,12 @@
     1.4    val depth_meson_tac	: int -> tactic
     1.5    val prolog_step_tac'	: thm list -> int -> tactic
     1.6    val iter_deepen_prolog_tac	: thm list -> tactic
     1.7 -  val iter_deepen_meson_tac	: int -> tactic
     1.8 +  val iter_deepen_meson_tac	: thm list -> int -> tactic
     1.9    val meson_tac		: int -> tactic
    1.10    val negate_head	: thm -> thm
    1.11    val select_literal	: int -> thm -> thm
    1.12    val skolemize_tac	: int -> tactic
    1.13    val make_clauses_tac	: int -> tactic
    1.14 -  val meson_setup	: (theory -> theory) list
    1.15  end
    1.16  
    1.17  
    1.18 @@ -61,6 +60,7 @@
    1.19  val disj_FalseD1 = thm "meson_disj_FalseD1";
    1.20  val disj_FalseD2 = thm "meson_disj_FalseD2";
    1.21  
    1.22 +val depth_limit = ref 2000;
    1.23  
    1.24  (**** Operators for forward proof ****)
    1.25  
    1.26 @@ -250,7 +250,8 @@
    1.27  fun make_horn crules th = make_horn crules (tryres(th,crules))
    1.28  			  handle THM _ => th;
    1.29  
    1.30 -(*Generate Horn clauses for all contrapositives of a clause*)
    1.31 +(*Generate Horn clauses for all contrapositives of a clause. The input, th,
    1.32 +  is a HOL disjunction.*)
    1.33  fun add_contras crules (th,hcs) =
    1.34    let fun rots (0,th) = hcs
    1.35  	| rots (k,th) = zero_var_indexes (make_horn crules th) ::
    1.36 @@ -267,7 +268,7 @@
    1.37  
    1.38      in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    1.39  
    1.40 -(*Find an all-negative support clause*)
    1.41 +(*Is the given disjunction an all-negative support clause?*)
    1.42  fun is_negative th = forall (not o #1) (literals (prop_of th));
    1.43  
    1.44  val neg_clauses = List.filter is_negative;
    1.45 @@ -349,7 +350,7 @@
    1.46      (sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths)));
    1.47  
    1.48  
    1.49 -(*Convert a list of clauses to (contrapositive) Horn clauses*)
    1.50 +(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    1.51  fun make_horns ths =
    1.52      name_thms "Horn#"
    1.53        (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
    1.54 @@ -366,7 +367,6 @@
    1.55  (*Return all negative clauses, as possible goal clauses*)
    1.56  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    1.57  
    1.58 -
    1.59  fun skolemize_prems_tac prems =
    1.60      cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
    1.61      REPEAT o (etac exE);
    1.62 @@ -380,6 +380,7 @@
    1.63  
    1.64  (** Best-first search versions **)
    1.65  
    1.66 +(*ths is a list of additional clauses (HOL disjunctions) to use.*)
    1.67  fun best_meson_tac sizef =
    1.68    MESON (fn cls =>
    1.69           THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
    1.70 @@ -398,7 +399,6 @@
    1.71                               depth_prolog_tac (make_horns cls)]);
    1.72  
    1.73  
    1.74 -
    1.75  (** Iterative deepening version **)
    1.76  
    1.77  (*This version does only one inference per call;
    1.78 @@ -415,16 +415,19 @@
    1.79  fun iter_deepen_prolog_tac horns =
    1.80      ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
    1.81  
    1.82 -val iter_deepen_meson_tac =
    1.83 +fun iter_deepen_meson_tac ths =
    1.84    MESON (fn cls =>
    1.85 -         (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
    1.86 -                           (has_fewer_prems 1)
    1.87 -                           (prolog_step_tac' (make_horns cls))));
    1.88 +           case (gocls (cls@ths)) of
    1.89 +           	[] => no_tac  (*no goal clauses*)
    1.90 +              | goes => 
    1.91 +		 (THEN_ITER_DEEPEN (resolve_tac goes 1)
    1.92 +				   (has_fewer_prems 1)
    1.93 +				   (prolog_step_tac' (make_horns (cls@ths)))));
    1.94  
    1.95 -fun meson_claset_tac cs =
    1.96 -  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac);
    1.97 +fun meson_claset_tac ths cs =
    1.98 +  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
    1.99  
   1.100 -val meson_tac = CLASET' meson_claset_tac;
   1.101 +val meson_tac = CLASET' (meson_claset_tac []);
   1.102  
   1.103  
   1.104  (**** Code to support ordinary resolution, rather than Model Elimination ****)
   1.105 @@ -496,28 +499,19 @@
   1.106                    (make_meta_clauses (make_clauses hyps))) 1)),
   1.107  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   1.108       end);
   1.109 -
   1.110 -
   1.111 -(*** proof method setup ***)
   1.112 +     
   1.113 +     
   1.114 +(*** setup the special skoklemization methods ***)
   1.115  
   1.116 -fun meson_meth ctxt =
   1.117 -  Method.SIMPLE_METHOD' HEADGOAL
   1.118 -    (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt));
   1.119 +(*No CHANGED_PROP here, since these always appear in the preamble*)
   1.120  
   1.121 -val skolemize_meth =
   1.122 -  Method.SIMPLE_METHOD' HEADGOAL
   1.123 -    (CHANGED_PROP o skolemize_tac);
   1.124 +val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
   1.125 +
   1.126 +val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
   1.127  
   1.128 -val make_clauses_meth =
   1.129 -  Method.SIMPLE_METHOD' HEADGOAL
   1.130 -    (CHANGED_PROP o make_clauses_tac);
   1.131 -
   1.132 -
   1.133 -val meson_setup =
   1.134 +val skolemize_setup =
   1.135   [Method.add_methods
   1.136 -  [("meson", Method.ctxt_args meson_meth, 
   1.137 -    "The MESON resolution proof procedure"),
   1.138 -   ("skolemize", Method.no_args skolemize_meth, 
   1.139 +  [("skolemize", Method.no_args skolemize_meth, 
   1.140      "Skolemization into existential quantifiers"),
   1.141     ("make_clauses", Method.no_args make_clauses_meth, 
   1.142      "Conversion to !!-quantified meta-level clauses")]];