src/HOL/Tools/res_axioms.ML
author mengj
Fri Nov 18 07:08:18 2005 +0100 (2005-11-18)
changeset 18198 95330fc0ea8d
parent 18144 4edcb5fdc3b0
child 18274 bbca1d2da0e9
permissions -rw-r--r--
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
paulson@15347
     1
(*  Author: Jia Meng, Cambridge University Computer Laboratory
paulson@15347
     2
    ID: $Id$
paulson@15347
     3
    Copyright 2004 University of Cambridge
paulson@15347
     4
paulson@15347
     5
Transformation of axiom rules (elim/intro/etc) into CNF forms.    
paulson@15347
     6
*)
paulson@15347
     7
paulson@15997
     8
signature RES_AXIOMS =
paulson@15997
     9
  sig
paulson@15997
    10
  exception ELIMR2FOL of string
paulson@17404
    11
  val tagging_enabled : bool
paulson@15997
    12
  val elimRule_tac : thm -> Tactical.tactic
paulson@16012
    13
  val elimR2Fol : thm -> term
paulson@15997
    14
  val transform_elim : thm -> thm
quigley@16039
    15
  val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
mengj@18000
    16
  val clausify_axiom_pairsH : (string*thm) -> (ResHolClause.clause*thm) list
paulson@15997
    17
  val cnf_axiom : (string * thm) -> thm list
paulson@15997
    18
  val meta_cnf_axiom : thm -> thm list
paulson@15997
    19
  val claset_rules_of_thy : theory -> (string * thm) list
paulson@15997
    20
  val simpset_rules_of_thy : theory -> (string * thm) list
paulson@17484
    21
  val claset_rules_of_ctxt: Proof.context -> (string * thm) list
paulson@17484
    22
  val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
paulson@17829
    23
  val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
mengj@18000
    24
  val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list
paulson@16563
    25
  val clause_setup : (theory -> theory) list
paulson@16563
    26
  val meson_method_setup : (theory -> theory) list
mengj@17905
    27
  val pairname : thm -> (string * thm)
mengj@18000
    28
  val repeat_RS : thm -> thm -> thm
mengj@18198
    29
  val cnf_axiom_aux : thm -> thm list
mengj@18000
    30
paulson@15997
    31
  end;
paulson@15347
    32
mengj@18198
    33
structure ResAxioms : RES_AXIOMS =
paulson@15997
    34
 
paulson@15997
    35
struct
paulson@15347
    36
mengj@18000
    37
paulson@17404
    38
val tagging_enabled = false (*compile_time option*)
paulson@17404
    39
paulson@15997
    40
(**** Transformation of Elimination Rules into First-Order Formulas****)
paulson@15347
    41
paulson@15390
    42
(* a tactic used to prove an elim-rule. *)
paulson@16009
    43
fun elimRule_tac th =
paulson@16009
    44
    ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN
paulson@16588
    45
    REPEAT(fast_tac HOL_cs 1);
paulson@15347
    46
paulson@15347
    47
exception ELIMR2FOL of string;
paulson@15347
    48
paulson@15390
    49
(* functions used to construct a formula *)
paulson@15390
    50
paulson@15347
    51
fun make_disjs [x] = x
paulson@15956
    52
  | make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs)
paulson@15347
    53
paulson@15347
    54
fun make_conjs [x] = x
paulson@15956
    55
  | make_conjs (x :: xs) =  HOLogic.mk_conj(x, make_conjs xs)
paulson@15956
    56
paulson@15956
    57
fun add_EX tm [] = tm
paulson@15956
    58
  | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
paulson@15347
    59
paulson@15347
    60
paulson@15347
    61
paulson@15956
    62
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q)
paulson@15371
    63
  | is_neg _ _ = false;
paulson@15371
    64
paulson@15347
    65
paulson@15347
    66
exception STRIP_CONCL;
paulson@15347
    67
paulson@15347
    68
paulson@15371
    69
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
paulson@15956
    70
      let val P' = HOLogic.dest_Trueprop P
paulson@15956
    71
  	  val prems' = P'::prems
paulson@15956
    72
      in
paulson@15371
    73
	strip_concl' prems' bvs  Q
paulson@15956
    74
      end
paulson@15371
    75
  | strip_concl' prems bvs P = 
paulson@15956
    76
      let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
paulson@15956
    77
      in
paulson@15371
    78
	add_EX (make_conjs (P'::prems)) bvs
paulson@15956
    79
      end;
paulson@15371
    80
paulson@15371
    81
paulson@18141
    82
fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = 
paulson@18141
    83
      strip_concl prems ((x,xtp)::bvs) concl body
paulson@15371
    84
  | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
paulson@18141
    85
      if (is_neg P concl) then (strip_concl' prems bvs Q)
paulson@18141
    86
      else strip_concl (HOLogic.dest_Trueprop P::prems) bvs  concl Q
paulson@15371
    87
  | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
paulson@15347
    88
 
paulson@15347
    89
paulson@15371
    90
fun trans_elim (main,others,concl) =
paulson@15371
    91
    let val others' = map (strip_concl [] [] concl) others
paulson@15347
    92
	val disjs = make_disjs others'
paulson@15347
    93
    in
paulson@15956
    94
	HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs)
paulson@15347
    95
    end;
paulson@15347
    96
paulson@15347
    97
paulson@15390
    98
(* aux function of elim2Fol, take away predicate variable. *)
paulson@15371
    99
fun elimR2Fol_aux prems concl = 
paulson@15347
   100
    let val nprems = length prems
paulson@15347
   101
	val main = hd prems
paulson@15347
   102
    in
paulson@15956
   103
	if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main)
paulson@15371
   104
        else trans_elim (main, tl prems, concl)
paulson@15347
   105
    end;
paulson@15347
   106
paulson@15956
   107
    
paulson@16012
   108
(* convert an elim rule into an equivalent formula, of type term. *)
paulson@15347
   109
fun elimR2Fol elimR = 
paulson@15347
   110
    let val elimR' = Drule.freeze_all elimR
paulson@15347
   111
	val (prems,concl) = (prems_of elimR', concl_of elimR')
paulson@15347
   112
    in
paulson@15347
   113
	case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) 
paulson@15956
   114
		      => HOLogic.mk_Trueprop (elimR2Fol_aux prems concl)
paulson@15956
   115
                    | Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl) 
paulson@15347
   116
		    | _ => raise ELIMR2FOL("Not an elimination rule!")
paulson@15347
   117
    end;
paulson@15347
   118
paulson@15347
   119
paulson@15390
   120
(* check if a rule is an elim rule *)
paulson@16009
   121
fun is_elimR th = 
paulson@16009
   122
    case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true
paulson@15347
   123
			 | Var(indx,Type("prop",[])) => true
paulson@15347
   124
			 | _ => false;
paulson@15347
   125
paulson@15997
   126
(* convert an elim-rule into an equivalent theorem that does not have the 
paulson@15997
   127
   predicate variable.  Leave other theorems unchanged.*) 
paulson@16009
   128
fun transform_elim th =
paulson@16009
   129
  if is_elimR th then
paulson@16009
   130
    let val tm = elimR2Fol th
paulson@16009
   131
	val ctm = cterm_of (sign_of_thm th) tm	
paulson@18009
   132
    in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end
paulson@16563
   133
 else th;
paulson@15997
   134
paulson@15997
   135
paulson@15997
   136
(**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
paulson@15997
   137
paulson@15390
   138
(* repeated resolution *)
paulson@15347
   139
fun repeat_RS thm1 thm2 =
paulson@15347
   140
    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
paulson@15347
   141
    in
paulson@15347
   142
	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
paulson@15347
   143
    end;
paulson@15347
   144
paulson@15347
   145
paulson@16563
   146
(*Transfer a theorem into theory Reconstruction.thy if it is not already
paulson@15359
   147
  inside that theory -- because it's needed for Skolemization *)
paulson@15359
   148
paulson@16563
   149
(*This will refer to the final version of theory Reconstruction.*)
paulson@16563
   150
val recon_thy_ref = Theory.self_ref (the_context ());  
paulson@15359
   151
paulson@16563
   152
(*If called while Reconstruction is being created, it will transfer to the
paulson@16563
   153
  current version. If called afterward, it will transfer to the final version.*)
paulson@16009
   154
fun transfer_to_Reconstruction th =
paulson@16563
   155
    transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
paulson@15347
   156
paulson@15955
   157
fun is_taut th =
paulson@15955
   158
      case (prop_of th) of
paulson@15955
   159
           (Const ("Trueprop", _) $ Const ("True", _)) => true
paulson@15955
   160
         | _ => false;
paulson@15955
   161
paulson@15955
   162
(* remove tautologous clauses *)
paulson@15955
   163
val rm_redundant_cls = List.filter (not o is_taut);
paulson@18141
   164
     
paulson@15997
   165
       
paulson@16009
   166
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
paulson@16009
   167
paulson@18141
   168
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
paulson@18141
   169
  prefix for the Skolem constant. Result is a new theory*)
paulson@18141
   170
fun declare_skofuns s th thy =
paulson@17404
   171
  let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) =
paulson@16009
   172
	    (*Existential: declare a Skolem function, then insert into body and continue*)
paulson@16009
   173
	    let val cname = s ^ "_" ^ Int.toString n
paulson@16012
   174
		val args = term_frees xtp  (*get the formal parameter list*)
paulson@16009
   175
		val Ts = map type_of args
paulson@16009
   176
		val cT = Ts ---> T
paulson@18141
   177
		val c = Const (Sign.full_name thy cname, cT)
paulson@16009
   178
		val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
paulson@16012
   179
		        (*Forms a lambda-abstraction over the formal parameters*)
paulson@16009
   180
		val def = equals cT $ c $ rhs
paulson@16009
   181
		val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
paulson@16012
   182
		           (*Theory is augmented with the constant, then its def*)
paulson@17404
   183
		val cdef = cname ^ "_def"
paulson@17404
   184
		val thy'' = Theory.add_defs_i false [(cdef, def)] thy'
paulson@17404
   185
	    in dec_sko (subst_bound (list_comb(c,args), p)) 
paulson@17404
   186
	               (n+1, (thy'', get_axiom thy'' cdef :: axs)) 
paulson@17404
   187
	    end
paulson@17404
   188
	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
paulson@16012
   189
	    (*Universal quant: insert a free variable into body and continue*)
paulson@16009
   190
	    let val fname = variant (add_term_names (p,[])) a
paulson@17404
   191
	    in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
paulson@18141
   192
	| dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
paulson@18141
   193
	| dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
paulson@18141
   194
	| dec_sko (Const ("HOL.tag", _) $ p) nthy = dec_sko p nthy
paulson@18141
   195
	| dec_sko (Const ("Trueprop", _) $ p) nthy = dec_sko p nthy
paulson@17404
   196
	| dec_sko t nthx = nthx (*Do nothing otherwise*)
paulson@18141
   197
  in  #2 (dec_sko (#prop (rep_thm th)) (1, (thy,[])))  end;
paulson@18141
   198
paulson@18141
   199
(*Traverse a theorem, accumulating Skolem function definitions.*)
paulson@18141
   200
fun assume_skofuns th =
paulson@18141
   201
  let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
paulson@18141
   202
	    (*Existential: declare a Skolem function, then insert into body and continue*)
paulson@18141
   203
	    let val name = variant (add_term_names (p,[])) (gensym "sko_")
paulson@18141
   204
                val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
paulson@18141
   205
		val args = term_frees xtp \\ skos  (*the formal parameters*)
paulson@18141
   206
		val Ts = map type_of args
paulson@18141
   207
		val cT = Ts ---> T
paulson@18141
   208
		val c = Free (name, cT)
paulson@18141
   209
		val rhs = list_abs_free (map dest_Free args,        
paulson@18141
   210
		                         HOLogic.choice_const T $ xtp)
paulson@18141
   211
		      (*Forms a lambda-abstraction over the formal parameters*)
paulson@18141
   212
		val def = equals cT $ c $ rhs
paulson@18141
   213
	    in dec_sko (subst_bound (list_comb(c,args), p)) 
paulson@18141
   214
	               (def :: defs)
paulson@18141
   215
	    end
paulson@18141
   216
	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
paulson@18141
   217
	    (*Universal quant: insert a free variable into body and continue*)
paulson@18141
   218
	    let val fname = variant (add_term_names (p,[])) a
paulson@18141
   219
	    in dec_sko (subst_bound (Free(fname,T), p)) defs end
paulson@18141
   220
	| dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
paulson@18141
   221
	| dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
paulson@18141
   222
	| dec_sko (Const ("HOL.tag", _) $ p) defs = dec_sko p defs
paulson@18141
   223
	| dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
paulson@18141
   224
	| dec_sko t defs = defs (*Do nothing otherwise*)
paulson@18141
   225
  in  dec_sko (#prop (rep_thm th)) []  end;
paulson@16009
   226
paulson@16009
   227
(*cterms are used throughout for efficiency*)
paulson@18141
   228
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
paulson@16009
   229
paulson@16009
   230
(*cterm version of mk_cTrueprop*)
paulson@16009
   231
fun c_mkTrueprop A = Thm.capply cTrueprop A;
paulson@16009
   232
paulson@16009
   233
(*Given an abstraction over n variables, replace the bound variables by free
paulson@16009
   234
  ones. Return the body, along with the list of free variables.*)
paulson@16009
   235
fun c_variant_abs_multi (ct0, vars) = 
paulson@16009
   236
      let val (cv,ct) = Thm.dest_abs NONE ct0
paulson@16009
   237
      in  c_variant_abs_multi (ct, cv::vars)  end
paulson@16009
   238
      handle CTERM _ => (ct0, rev vars);
paulson@16009
   239
paulson@16009
   240
(*Given the definition of a Skolem function, return a theorem to replace 
paulson@18141
   241
  an existential formula by a use of that function. 
paulson@18141
   242
   Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
paulson@16588
   243
fun skolem_of_def def =  
paulson@16009
   244
  let val (c,rhs) = Drule.dest_equals (cprop_of (Drule.freeze_all def))
paulson@16009
   245
      val (ch, frees) = c_variant_abs_multi (rhs, [])
paulson@18141
   246
      val (chilbert,cabs) = Thm.dest_comb ch
paulson@18141
   247
      val {sign,t, ...} = rep_cterm chilbert
paulson@18141
   248
      val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
paulson@18141
   249
                      | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
paulson@16009
   250
      val cex = Thm.cterm_of sign (HOLogic.exists_const T)
paulson@16009
   251
      val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
paulson@16009
   252
      and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
paulson@18141
   253
      fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
paulson@18141
   254
  in  Goal.prove_raw [ex_tm] conc tacf 
paulson@18141
   255
       |> forall_intr_list frees
paulson@18141
   256
       |> forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
paulson@18141
   257
       |> Thm.varifyT
paulson@18141
   258
  end;
paulson@16009
   259
mengj@18198
   260
(*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*)
mengj@18198
   261
(*It now works for HOL too. *)
paulson@18141
   262
fun to_nnf th = 
paulson@18141
   263
    th |> transfer_to_Reconstruction
paulson@16588
   264
       |> transform_elim |> Drule.freeze_all
paulson@16588
   265
       |> ObjectLogic.atomize_thm |> make_nnf;
paulson@16009
   266
mengj@18198
   267
mengj@18198
   268
mengj@18198
   269
paulson@16009
   270
(*The cache prevents repeated clausification of a theorem, 
wenzelm@16800
   271
  and also repeated declaration of Skolem functions*)  (* FIXME better use Termtab!? *)
paulson@15955
   272
val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
paulson@15955
   273
paulson@18141
   274
paulson@18141
   275
(*Generate Skolem functions for a theorem supplied in nnf*)
paulson@18141
   276
fun skolem_of_nnf th =
paulson@18141
   277
  map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
paulson@18141
   278
mengj@18198
   279
(*Skolemize a named theorem, returning a modified theory.*)
mengj@18198
   280
(*also works for HOL*) 
paulson@18141
   281
fun skolem_thm th = 
paulson@18141
   282
  Option.map (fn nnfth => Meson.make_cnf (skolem_of_nnf nnfth) nnfth)
paulson@18141
   283
	 (SOME (to_nnf th)  handle THM _ => NONE);
paulson@18141
   284
mengj@18198
   285
paulson@16009
   286
(*Declare Skolem functions for a theorem, supplied in nnf and with its name*)
mengj@18198
   287
(*in case skolemization fails, the input theory is not changed*)
paulson@16009
   288
fun skolem thy (name,th) =
paulson@16588
   289
  let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)
paulson@18141
   290
  in Option.map 
paulson@18141
   291
        (fn nnfth => 
paulson@18141
   292
          let val (thy',defs) = declare_skofuns cname nnfth thy
paulson@18141
   293
              val skoths = map skolem_of_def defs
paulson@18141
   294
          in (thy', Meson.make_cnf skoths nnfth) end)
mengj@18198
   295
      (SOME (to_nnf th)  handle THM _ => NONE) 
paulson@18141
   296
  end;
paulson@16009
   297
paulson@16009
   298
(*Populate the clause cache using the supplied theorems*)
paulson@18141
   299
fun skolem_cache ((name,th), thy) =
paulson@18144
   300
  case Symtab.lookup (!clause_cache) name of
paulson@18144
   301
      NONE => 
paulson@18144
   302
	(case skolem thy (name, Thm.transfer thy th) of
paulson@18144
   303
	     NONE => thy
paulson@18144
   304
	   | SOME (thy',cls) => 
paulson@18144
   305
	       (change clause_cache (Symtab.update (name, (th, cls))); thy'))
paulson@18144
   306
    | SOME (th',cls) =>
paulson@18144
   307
        if eq_thm(th,th') then thy
paulson@18144
   308
	else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); 
paulson@18144
   309
	      warning (string_of_thm th);
paulson@18144
   310
	      warning (string_of_thm th');
paulson@18144
   311
	      thy);
paulson@18141
   312
paulson@16009
   313
paulson@16009
   314
(*Exported function to convert Isabelle theorems into axiom clauses*) 
paulson@18141
   315
fun cnf_axiom_g cnf (name,th) =
paulson@18144
   316
  case name of
paulson@18144
   317
	"" => cnf th (*no name, so can't cache*)
paulson@18144
   318
      | s  => case Symtab.lookup (!clause_cache) s of
paulson@18144
   319
		NONE => 
paulson@18144
   320
		  let val cls = cnf th
paulson@18144
   321
		  in change clause_cache (Symtab.update (s, (th, cls))); cls end
paulson@18144
   322
	      | SOME(th',cls) =>
paulson@18144
   323
		  if eq_thm(th,th') then cls
paulson@18144
   324
		  else (warning ("cnf_axiom: duplicate or variant of theorem " ^ name); 
paulson@18144
   325
		        warning (string_of_thm th);
paulson@18144
   326
		        warning (string_of_thm th');
paulson@18144
   327
		        cls);
paulson@15347
   328
paulson@18141
   329
fun pairname th = (Thm.name_of_thm th, th);
paulson@18141
   330
paulson@18141
   331
mengj@18198
   332
(*no first-order check, so works for HOL too.*)
paulson@18141
   333
fun cnf_axiom_aux th = Option.getOpt (skolem_thm th, []);
mengj@18000
   334
mengj@18198
   335
paulson@18141
   336
mengj@18198
   337
val cnf_axiom = cnf_axiom_g cnf_axiom_aux;
mengj@18000
   338
mengj@18000
   339
paulson@15956
   340
fun meta_cnf_axiom th = 
paulson@15956
   341
    map Meson.make_meta_clause (cnf_axiom (pairname th));
paulson@15499
   342
paulson@15347
   343
paulson@15347
   344
paulson@15872
   345
(**** Extract and Clausify theorems from a theory's claset and simpset ****)
paulson@15347
   346
paulson@17404
   347
(*Preserve the name of "th" after the transformation "f"*)
paulson@17404
   348
fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th);
paulson@17404
   349
paulson@17404
   350
(*Tags identify the major premise or conclusion, as hints to resolution provers.
paulson@17404
   351
  However, they don't appear to help in recent tests, and they complicate the code.*)
paulson@17404
   352
val tagI = thm "tagI";
paulson@17404
   353
val tagD = thm "tagD";
paulson@17404
   354
paulson@17404
   355
val tag_intro = preserve_name (fn th => th RS tagI);
paulson@17404
   356
val tag_elim  = preserve_name (fn th => tagD RS th);
paulson@17404
   357
paulson@17484
   358
fun rules_of_claset cs =
paulson@17484
   359
  let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
paulson@17484
   360
      val intros = safeIs @ hazIs
paulson@17484
   361
      val elims  = safeEs @ hazEs
paulson@17404
   362
  in
paulson@17484
   363
     debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ 
paulson@17484
   364
            " elims: " ^ Int.toString(length elims));
paulson@17404
   365
     if tagging_enabled 
paulson@17404
   366
     then map pairname (map tag_intro intros @ map tag_elim elims)
paulson@17484
   367
     else map pairname (intros @ elims)
paulson@17404
   368
  end;
paulson@15347
   369
paulson@17484
   370
fun rules_of_simpset ss =
paulson@17484
   371
  let val ({rules,...}, _) = rep_ss ss
paulson@17484
   372
      val simps = Net.entries rules
paulson@17484
   373
  in 
paulson@17484
   374
      debug ("rules_of_simpset: " ^ Int.toString(length simps));
paulson@17484
   375
      map (fn r => (#name r, #thm r)) simps
paulson@17484
   376
  end;
paulson@17484
   377
paulson@17484
   378
fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
paulson@17484
   379
fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
paulson@17484
   380
paulson@17484
   381
fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
paulson@17484
   382
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
paulson@15347
   383
paulson@15347
   384
paulson@15872
   385
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)
paulson@15347
   386
paulson@15347
   387
(* classical rules *)
mengj@18000
   388
fun cnf_rules_g cnf_axiom [] err_list = ([],err_list)
mengj@18000
   389
  | cnf_rules_g cnf_axiom ((name,th) :: ths) err_list = 
mengj@18000
   390
      let val (ts,es) = cnf_rules_g cnf_axiom ths err_list
paulson@17404
   391
      in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;  
paulson@15347
   392
paulson@15347
   393
mengj@18198
   394
(*works for both FOL and HOL*)
mengj@18000
   395
val cnf_rules = cnf_rules_g cnf_axiom;
mengj@18000
   396
mengj@18000
   397
mengj@18198
   398
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
paulson@15347
   399
paulson@18141
   400
fun make_axiom_clauses _ _ [] = []
paulson@18141
   401
  | make_axiom_clauses name i (cls::clss) =
paulson@18141
   402
      (ResClause.make_axiom_clause (prop_of cls) (name,i), cls) ::
paulson@18141
   403
      (make_axiom_clauses name (i+1) clss)
mengj@18000
   404
paulson@17829
   405
(* outputs a list of (clause,theorem) pairs *)
paulson@18141
   406
fun clausify_axiom_pairs (name,th) = 
paulson@18141
   407
    filter (fn (c,th) => not (ResClause.isTaut c))
paulson@18141
   408
           (make_axiom_clauses name 0 (cnf_axiom (name,th)));
mengj@18000
   409
paulson@18141
   410
fun make_axiom_clausesH _ _ [] = []
paulson@18141
   411
  | make_axiom_clausesH name i (cls::clss) =
paulson@18141
   412
      (ResHolClause.make_axiom_clause (prop_of cls) (name,i), cls) ::
paulson@18141
   413
      (make_axiom_clausesH name (i+1) clss)
mengj@18000
   414
paulson@18141
   415
fun clausify_axiom_pairsH (name,th) = 
paulson@18141
   416
    filter (fn (c,th) => not (ResHolClause.isTaut c))
mengj@18198
   417
           (make_axiom_clausesH name 0 (cnf_axiom (name,th)));
mengj@18000
   418
mengj@18000
   419
paulson@17829
   420
fun clausify_rules_pairs_aux result [] = result
paulson@17829
   421
  | clausify_rules_pairs_aux result ((name,th)::ths) =
paulson@17829
   422
      clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths
paulson@17829
   423
      handle THM (msg,_,_) =>  
paulson@17829
   424
	      (debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
paulson@17829
   425
	       clausify_rules_pairs_aux result ths)
paulson@17829
   426
	 |  ResClause.CLAUSE (msg,t) => 
paulson@17829
   427
	      (debug ("Cannot clausify " ^ name ^ ": " ^ msg ^
paulson@17829
   428
		      ": " ^ TermLib.string_of_term t); 
paulson@17829
   429
	       clausify_rules_pairs_aux result ths)
paulson@17404
   430
mengj@18000
   431
mengj@18000
   432
fun clausify_rules_pairs_auxH result [] = result
mengj@18000
   433
  | clausify_rules_pairs_auxH result ((name,th)::ths) =
mengj@18000
   434
      clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths
mengj@18000
   435
      handle THM (msg,_,_) =>  
mengj@18000
   436
	      (debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
mengj@18000
   437
	       clausify_rules_pairs_auxH result ths)
mengj@18000
   438
	 |  ResHolClause.LAM2COMB (t) => 
mengj@18000
   439
	      (debug ("Cannot clausify "  ^ TermLib.string_of_term t); 
mengj@18000
   440
	       clausify_rules_pairs_auxH result ths)
quigley@16039
   441
paulson@15347
   442
mengj@18000
   443
mengj@18000
   444
val clausify_rules_pairs = clausify_rules_pairs_aux [];
mengj@18000
   445
mengj@18000
   446
val clausify_rules_pairsH = clausify_rules_pairs_auxH [];
paulson@18141
   447
paulson@16009
   448
(*Setup function: takes a theory and installs ALL simprules and claset rules 
paulson@16009
   449
  into the clause cache*)
paulson@16009
   450
fun clause_cache_setup thy =
paulson@16009
   451
  let val simps = simpset_rules_of_thy thy
paulson@16009
   452
      and clas  = claset_rules_of_thy thy
paulson@18141
   453
  in List.foldl skolem_cache (List.foldl skolem_cache thy clas) simps end;
paulson@18141
   454
(*Could be duplicate theorem names, due to multiple attributes*)
paulson@16009
   455
  
paulson@16563
   456
val clause_setup = [clause_cache_setup];  
paulson@16563
   457
paulson@16563
   458
paulson@16563
   459
(*** meson proof methods ***)
paulson@16563
   460
paulson@16563
   461
fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) []));
paulson@16563
   462
paulson@16563
   463
fun meson_meth ths ctxt =
paulson@16563
   464
  Method.SIMPLE_METHOD' HEADGOAL
paulson@16563
   465
    (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
paulson@16563
   466
paulson@16563
   467
val meson_method_setup =
paulson@16563
   468
 [Method.add_methods
paulson@16563
   469
  [("meson", Method.thms_ctxt_args meson_meth, 
paulson@16563
   470
    "The MESON resolution proof procedure")]];
paulson@15347
   471
paulson@15347
   472
end;