new skolemize_tac and skolemize method
authorpaulson
Fri May 28 11:20:04 2004 +0200 (2004-05-28)
changeset 14813826edbc317e6
parent 14812 4b2c006d0534
child 14814 c6b91c8aee1d
new skolemize_tac and skolemize method
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Fri May 28 11:19:15 2004 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri May 28 11:20:04 2004 +0200
     1.3 @@ -345,7 +345,7 @@
     1.4  val meson_tac = CLASET' meson_claset_tac;
     1.5  
     1.6  
     1.7 -(** Code to support ordinary resolution, rather than Model Elimination **)
     1.8 +(**** Code to support ordinary resolution, rather than Model Elimination ****)
     1.9  
    1.10  (*Convert a list of clauses to meta-level clauses, with no contrapositives,
    1.11    for ordinary resolution.*)
    1.12 @@ -381,6 +381,23 @@
    1.13  (*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
    1.14  fun select_literal i cl = negate_head (make_last i cl);
    1.15  
    1.16 +(*Top-level Skolemization. Allows part of the conversion to clauses to be
    1.17 +  expressed as a tactic (or Isar method).  Each assumption of the selected 
    1.18 +  goal is converted to NNF and then its existential quantifiers are pulled
    1.19 +  to the front. Finally, all existential quantifiers are eliminated, 
    1.20 +  leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
    1.21 +  might generate many subgoals.*)
    1.22 +val skolemize_tac = 
    1.23 +  SUBGOAL
    1.24 +    (fn (prop,_) =>
    1.25 +     let val ts = Logic.strip_assums_hyp prop
    1.26 +     in EVERY1 
    1.27 +	 [METAHYPS
    1.28 +	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
    1.29 +                         THEN REPEAT (etac exE 1))),
    1.30 +	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.31 +     end);
    1.32 +
    1.33  
    1.34  
    1.35  (** proof method setup **)
    1.36 @@ -395,7 +412,10 @@
    1.37  
    1.38  val meson_setup =
    1.39   [Method.add_methods
    1.40 -  [("meson", Method.ctxt_args meson_meth, "The MESON resolution proof procedure")]];
    1.41 +  [("meson", Method.ctxt_args meson_meth, 
    1.42 +    "The MESON resolution proof procedure"),
    1.43 +   ("skolemize", Method.no_args (Method.METHOD (fn _ => skolemize_tac 1)), 
    1.44 +    "Skolemization into existential quantifiers")]];
    1.45  
    1.46  end;
    1.47