the experimental tagging system, and the usual tidying
authorpaulson
Thu Sep 15 11:15:52 2005 +0200 (2005-09-15)
changeset 17404d16c3a62c396
parent 17403 de60322ff13a
child 17405 e4dc583a2d79
the experimental tagging system, and the usual tidying
src/HOL/HOL.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Sep 15 10:33:35 2005 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Sep 15 11:15:52 2005 +0200
     1.3 @@ -1282,6 +1282,28 @@
     1.4  
     1.5  setup InductMethod.setup
     1.6  
     1.7 +subsubsection{*Tags, for the ATP Linkup*}
     1.8 +
     1.9 +constdefs
    1.10 +  tag :: "bool => bool"
    1.11 +   "tag P == P"
    1.12 +
    1.13 +text{*These label the distinguished literals of introduction and elimination
    1.14 +rules.*}
    1.15 +
    1.16 +lemma tagI: "P ==> tag P"
    1.17 +by (simp add: tag_def)
    1.18 +
    1.19 +lemma tagD: "tag P ==> P"
    1.20 +by (simp add: tag_def)
    1.21 +
    1.22 +text{*Applications of "tag" to True and False must go!*}
    1.23 +
    1.24 +lemma tag_True: "tag True = True"
    1.25 +by (simp add: tag_def)
    1.26 +
    1.27 +lemma tag_False: "tag False = False"
    1.28 +by (simp add: tag_def)
    1.29  
    1.30  end
    1.31  
     2.1 --- a/src/HOL/Tools/meson.ML	Thu Sep 15 10:33:35 2005 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Thu Sep 15 11:15:52 2005 +0200
     2.3 @@ -225,7 +225,7 @@
     2.4    incomplete, since when actually called, the only connectives likely to
     2.5    remain are & | Not.*)  
     2.6  fun is_conn c = c mem_string
     2.7 -    ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
     2.8 +    ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", 
     2.9       "All", "Ex", "Ball", "Bex"];
    2.10  
    2.11  (*True if the term contains a function where the type of any argument contains
    2.12 @@ -329,8 +329,11 @@
    2.13             (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
    2.14      handle THM _ => th;
    2.15  
    2.16 -(*The simplification removes defined quantifiers and occurrences of True and False.*)
    2.17 -val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms;
    2.18 +(*The simplification removes defined quantifiers and occurrences of True and False, as well as tags applied to True and False.*)
    2.19 +val tag_True = thm "tag_True";
    2.20 +val tag_False = thm "tag_False";
    2.21 +val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
    2.22 +val nnf_ss = HOL_basic_ss addsimps nnf_simps@simp_thms;
    2.23  
    2.24  fun make_nnf th = th |> simplify nnf_ss
    2.25                       |> check_is_fol |> make_nnf1
     3.1 --- a/src/HOL/Tools/res_atp.ML	Thu Sep 15 10:33:35 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Sep 15 11:15:52 2005 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4  
     3.5  fun debug_tac tac = (debug "testing"; tac);
     3.6  
     3.7 -val prover = ref "spass";   (* use spass as default prover *)
     3.8 +val prover = ref "E";   (* use E as the default prover *)
     3.9  val custom_spass =   (*specialized options for SPASS*)
    3.10        ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    3.11             "-DocProof","-TimeLimit=60"];
     4.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Sep 15 10:33:35 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Sep 15 11:15:52 2005 +0200
     4.3 @@ -8,18 +8,17 @@
     4.4  signature RES_AXIOMS =
     4.5    sig
     4.6    exception ELIMR2FOL of string
     4.7 +  val tagging_enabled : bool
     4.8    val elimRule_tac : thm -> Tactical.tactic
     4.9    val elimR2Fol : thm -> term
    4.10    val transform_elim : thm -> thm
    4.11    val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
    4.12    val cnf_axiom : (string * thm) -> thm list
    4.13    val meta_cnf_axiom : thm -> thm list
    4.14 -  val cnf_rule : thm -> thm list
    4.15 -  val cnf_rules : (string*thm) list -> thm list -> thm list list * thm list
    4.16    val rm_Eps : (term * term) list -> thm list -> term list
    4.17    val claset_rules_of_thy : theory -> (string * thm) list
    4.18    val simpset_rules_of_thy : theory -> (string * thm) list
    4.19 -  val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list
    4.20 +  val clausify_rules_pairs : (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list
    4.21    val clause_setup : (theory -> theory) list
    4.22    val meson_method_setup : (theory -> theory) list
    4.23    end;
    4.24 @@ -28,6 +27,8 @@
    4.25   
    4.26  struct
    4.27  
    4.28 +val tagging_enabled = false (*compile_time option*)
    4.29 +
    4.30  (**** Transformation of Elimination Rules into First-Order Formulas****)
    4.31  
    4.32  (* a tactic used to prove an elim-rule. *)
    4.33 @@ -133,8 +134,6 @@
    4.34  
    4.35  (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    4.36  
    4.37 -(* to be fixed: cnf_intro, cnf_rule, is_introR *)
    4.38 -
    4.39  (* repeated resolution *)
    4.40  fun repeat_RS thm1 thm2 =
    4.41      let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    4.42 @@ -182,7 +181,7 @@
    4.43  
    4.44  (*Traverse a term, accumulating Skolem function definitions.*)
    4.45  fun declare_skofuns s t thy =
    4.46 -  let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, thy) =
    4.47 +  let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) =
    4.48  	    (*Existential: declare a Skolem function, then insert into body and continue*)
    4.49  	    let val cname = s ^ "_" ^ Int.toString n
    4.50  		val args = term_frees xtp  (*get the formal parameter list*)
    4.51 @@ -194,20 +193,25 @@
    4.52  		val def = equals cT $ c $ rhs
    4.53  		val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
    4.54  		           (*Theory is augmented with the constant, then its def*)
    4.55 -		val thy'' = Theory.add_defs_i false [(cname ^ "_def", def)] thy'
    4.56 -	    in dec_sko (subst_bound (list_comb(c,args), p)) (n+1, thy'') end
    4.57 -	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thy) =
    4.58 +		val cdef = cname ^ "_def"
    4.59 +		val thy'' = Theory.add_defs_i false [(cdef, def)] thy'
    4.60 +	    in dec_sko (subst_bound (list_comb(c,args), p)) 
    4.61 +	               (n+1, (thy'', get_axiom thy'' cdef :: axs)) 
    4.62 +	    end
    4.63 +	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
    4.64  	    (*Universal quant: insert a free variable into body and continue*)
    4.65  	    let val fname = variant (add_term_names (p,[])) a
    4.66 -	    in dec_sko (subst_bound (Free(fname,T), p)) (n, thy) end
    4.67 +	    in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
    4.68  	| dec_sko (Const ("op &", _) $ p $ q) nthy = 
    4.69  	    dec_sko q (dec_sko p nthy)
    4.70  	| dec_sko (Const ("op |", _) $ p $ q) nthy = 
    4.71  	    dec_sko q (dec_sko p nthy)
    4.72 +	| dec_sko (Const ("HOL.tag", _) $ p) nthy = 
    4.73 +	    dec_sko p nthy
    4.74  	| dec_sko (Const ("Trueprop", _) $ p) nthy = 
    4.75  	    dec_sko p nthy
    4.76 -	| dec_sko t (n,thy) = (n,thy) (*Do nothing otherwise*)
    4.77 -  in  #2 (dec_sko t (1,thy))  end;
    4.78 +	| dec_sko t nthx = nthx (*Do nothing otherwise*)
    4.79 +  in  #2 (dec_sko t (1, (thy,[])))  end;
    4.80  
    4.81  (*cterms are used throughout for efficiency*)
    4.82  val cTrueprop = Thm.cterm_of (Theory.sign_of HOL.thy) HOLogic.Trueprop;
    4.83 @@ -251,8 +255,8 @@
    4.84  (*Declare Skolem functions for a theorem, supplied in nnf and with its name*)
    4.85  fun skolem thy (name,th) =
    4.86    let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)
    4.87 -      val thy' = declare_skofuns cname (#prop (rep_thm th)) thy
    4.88 -  in (map (skolem_of_def o #2) (axioms_of thy'), thy') end;
    4.89 +      val (thy',axs) = declare_skofuns cname (#prop (rep_thm th)) thy
    4.90 +  in (map skolem_of_def axs, thy') end;
    4.91  
    4.92  (*Populate the clause cache using the supplied theorems*)
    4.93  fun skolemlist [] thy = thy
    4.94 @@ -313,18 +317,15 @@
    4.95  	(sk_term,(t,sk_term)::epss)
    4.96      end;
    4.97  
    4.98 -
    4.99 +(*FIXME: use a-list lookup!!*)
   4.100  fun sk_lookup [] t = NONE
   4.101    | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then SOME (sk_tm) else (sk_lookup tms t);
   4.102  
   4.103 -
   4.104 -
   4.105  (* get the proper skolem term to replace epsilon term *)
   4.106  fun get_skolem epss t = 
   4.107      case (sk_lookup epss t) of NONE => get_new_skolem epss t
   4.108  		             | SOME sk => (sk,epss);
   4.109  
   4.110 -
   4.111  fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = 
   4.112         get_skolem epss t
   4.113    | rm_Eps_cls_aux epss (P $ Q) =
   4.114 @@ -333,11 +334,9 @@
   4.115         in (P' $ Q',epss'') end
   4.116    | rm_Eps_cls_aux epss t = (t,epss);
   4.117  
   4.118 -
   4.119  fun rm_Eps_cls epss th = rm_Eps_cls_aux epss (prop_of th);
   4.120  
   4.121 -
   4.122 -(* remove the epsilon terms in a formula, by skolem terms. *)
   4.123 +(* replace the epsilon terms in a formula by skolem terms. *)
   4.124  fun rm_Eps _ [] = []
   4.125    | rm_Eps epss (th::thms) = 
   4.126        let val (th',epss') = rm_Eps_cls epss th
   4.127 @@ -347,15 +346,26 @@
   4.128  
   4.129  (**** Extract and Clausify theorems from a theory's claset and simpset ****)
   4.130  
   4.131 +(*Preserve the name of "th" after the transformation "f"*)
   4.132 +fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th);
   4.133 +
   4.134 +(*Tags identify the major premise or conclusion, as hints to resolution provers.
   4.135 +  However, they don't appear to help in recent tests, and they complicate the code.*)
   4.136 +val tagI = thm "tagI";
   4.137 +val tagD = thm "tagD";
   4.138 +
   4.139 +val tag_intro = preserve_name (fn th => th RS tagI);
   4.140 +val tag_elim  = preserve_name (fn th => tagD RS th);
   4.141 +
   4.142  fun claset_rules_of_thy thy =
   4.143 -    let val clsset = rep_cs (claset_of thy)
   4.144 -	val safeEs = #safeEs clsset
   4.145 -	val safeIs = #safeIs clsset
   4.146 -	val hazEs = #hazEs clsset
   4.147 -	val hazIs = #hazIs clsset
   4.148 -    in
   4.149 -	map pairname (safeEs @ safeIs @ hazEs @ hazIs)
   4.150 -    end;
   4.151 +  let val cs = rep_cs (claset_of thy)
   4.152 +      val intros = (#safeIs cs) @ (#hazIs cs)
   4.153 +      val elims  = (#safeEs cs) @ (#hazEs cs)
   4.154 +  in
   4.155 +     if tagging_enabled 
   4.156 +     then map pairname (map tag_intro intros @ map tag_elim elims)
   4.157 +     else map pairname (intros @  elims)
   4.158 +  end;
   4.159  
   4.160  fun simpset_rules_of_thy thy =
   4.161      let val rules = #rules (fst (rep_ss (simpset_of thy)))
   4.162 @@ -368,31 +378,40 @@
   4.163  fun cnf_rules [] err_list = ([],err_list)
   4.164    | cnf_rules ((name,th) :: thms) err_list = 
   4.165        let val (ts,es) = cnf_rules thms err_list
   4.166 -      in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;  (* FIXME avoid handle _ *)
   4.167 +      in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;  
   4.168  
   4.169  
   4.170  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
   4.171  
   4.172 +fun addclause (c,th) l =
   4.173 +  if ResClause.isTaut c then l else (c,th) :: l;
   4.174 +
   4.175  (* outputs a list of (clause,thm) pairs *)
   4.176  fun clausify_axiom_pairs (thm_name,thm) =
   4.177 -    let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
   4.178 +    let val isa_clauses = cnf_axiom (thm_name,thm) 
   4.179          val isa_clauses' = rm_Eps [] isa_clauses
   4.180          val clauses_n = length isa_clauses
   4.181 -        val thy = theory_of_thm thm
   4.182  	fun make_axiom_clauses _ [] []= []
   4.183  	  | make_axiom_clauses i (cls::clss) (cls'::clss') =
   4.184 -	      (ResClause.make_axiom_clause cls (thm_name,i), cls') :: 
   4.185 -	      make_axiom_clauses (i+1) clss clss'
   4.186 +	      addclause (ResClause.make_axiom_clause cls (thm_name,i), cls') 
   4.187 +	                (make_axiom_clauses (i+1) clss clss')
   4.188      in
   4.189  	make_axiom_clauses 0 isa_clauses' isa_clauses		
   4.190 -    end;
   4.191 +    end
   4.192  
   4.193  fun clausify_rules_pairs [] err_list = ([],err_list)
   4.194    | clausify_rules_pairs ((name,thm)::thms) err_list =
   4.195        let val (ts,es) = clausify_rules_pairs thms err_list
   4.196        in
   4.197  	  ((clausify_axiom_pairs (name,thm))::ts, es) 
   4.198 -	  handle  _ => (ts, (thm::es))  (* FIXME avoid handle _ *)
   4.199 +	  handle THM (msg,_,_) =>  
   4.200 +		  (debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
   4.201 +		   (ts, (thm::es)))
   4.202 +             |  ResClause.CLAUSE (msg,t) => 
   4.203 +                  (debug ("Cannot clausify " ^ name ^ ": " ^ msg ^
   4.204 +                          ": " ^ TermLib.string_of_term t); 
   4.205 +		   (ts, (thm::es)))
   4.206 +
   4.207        end;
   4.208  
   4.209  
     5.1 --- a/src/HOL/Tools/res_clause.ML	Thu Sep 15 10:33:35 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Sep 15 11:15:52 2005 +0200
     5.3 @@ -10,49 +10,49 @@
     5.4  (* works for writeoutclasimp on typed *)
     5.5  signature RES_CLAUSE =
     5.6    sig
     5.7 -    exception ARCLAUSE of string
     5.8 -    exception CLAUSE of string
     5.9 -    type arityClause 
    5.10 -    type classrelClause
    5.11 -    val classrelClauses_of : string * string list -> classrelClause list
    5.12 -    type clause
    5.13 -    val init : theory -> unit
    5.14 -    val keep_types : bool ref
    5.15 -    val make_axiom_arity_clause :
    5.16 -       string * (string * string list list) -> arityClause
    5.17 -    val make_axiom_classrelClause :
    5.18 -       string * string option -> classrelClause
    5.19 -    val make_axiom_clause : Term.term -> string * int -> clause
    5.20 -    val make_conjecture_clause : Term.term -> clause
    5.21 -    val make_conjecture_clause_thm : Thm.thm -> clause
    5.22 -    val make_hypothesis_clause : Term.term -> clause
    5.23 -    val special_equal : bool ref
    5.24 -    val get_axiomName : clause ->  string
    5.25 -    val typed : unit -> unit
    5.26 -    val untyped : unit -> unit
    5.27 -    val num_of_clauses : clause -> int
    5.28 +  val keep_types : bool ref
    5.29 +  val special_equal : bool ref
    5.30 +  val tagged : bool ref
    5.31 +
    5.32 +  exception ARCLAUSE of string
    5.33 +  exception CLAUSE of string * term
    5.34 +  type arityClause 
    5.35 +  type classrelClause
    5.36 +  val classrelClauses_of : string * string list -> classrelClause list
    5.37 +  type clause
    5.38 +  val init : theory -> unit
    5.39 +  val make_axiom_arity_clause :
    5.40 +     string * (string * string list list) -> arityClause
    5.41 +  val make_axiom_classrelClause :  string * string option -> classrelClause
    5.42 +  val make_axiom_clause : Term.term -> string * int -> clause
    5.43 +  val make_conjecture_clause : Term.term -> clause
    5.44 +  val make_conjecture_clause_thm : Thm.thm -> clause
    5.45 +  val make_hypothesis_clause : Term.term -> clause
    5.46 +  val get_axiomName : clause ->  string
    5.47 +  val isTaut : clause -> bool
    5.48 +  val num_of_clauses : clause -> int
    5.49  
    5.50 -    val dfg_clauses2str : string list -> string
    5.51 -    val clause2dfg : clause -> string * string list
    5.52 -    val clauses2dfg : clause list -> string -> clause list -> clause list ->
    5.53 -             (string * int) list -> (string * int) list -> string list -> string
    5.54 -    val tfree_dfg_clause : string -> string
    5.55 +  val dfg_clauses2str : string list -> string
    5.56 +  val clause2dfg : clause -> string * string list
    5.57 +  val clauses2dfg : clause list -> string -> clause list -> clause list ->
    5.58 +	   (string * int) list -> (string * int) list -> string list -> string
    5.59 +  val tfree_dfg_clause : string -> string
    5.60  
    5.61 -    val tptp_arity_clause : arityClause -> string
    5.62 -    val tptp_classrelClause : classrelClause -> string
    5.63 -    val tptp_clause : clause -> string list
    5.64 -    val tptp_clauses2str : string list -> string
    5.65 -    val clause2tptp : clause -> string * string list
    5.66 -    val tfree_clause : string -> string
    5.67 -    val schematic_var_prefix : string
    5.68 -    val fixed_var_prefix : string
    5.69 -    val tvar_prefix : string
    5.70 -    val tfree_prefix : string
    5.71 -    val clause_prefix : string 
    5.72 -    val arclause_prefix : string
    5.73 -    val const_prefix : string
    5.74 -    val tconst_prefix : string 
    5.75 -    val class_prefix : string 
    5.76 +  val tptp_arity_clause : arityClause -> string
    5.77 +  val tptp_classrelClause : classrelClause -> string
    5.78 +  val tptp_clause : clause -> string list
    5.79 +  val tptp_clauses2str : string list -> string
    5.80 +  val clause2tptp : clause -> string * string list
    5.81 +  val tfree_clause : string -> string
    5.82 +  val schematic_var_prefix : string
    5.83 +  val fixed_var_prefix : string
    5.84 +  val tvar_prefix : string
    5.85 +  val tfree_prefix : string
    5.86 +  val clause_prefix : string 
    5.87 +  val arclause_prefix : string
    5.88 +  val const_prefix : string
    5.89 +  val tconst_prefix : string 
    5.90 +  val class_prefix : string 
    5.91    end;
    5.92  
    5.93  structure ResClause: RES_CLAUSE =
    5.94 @@ -157,9 +157,6 @@
    5.95  (***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****)
    5.96  
    5.97  val keep_types = ref true;
    5.98 -fun untyped () = (keep_types := false);
    5.99 -fun typed () = (keep_types := true);
   5.100 -
   5.101  
   5.102  datatype kind = Axiom | Hypothesis | Conjecture;
   5.103  fun name_of_kind Axiom = "axiom"
   5.104 @@ -189,7 +186,6 @@
   5.105  
   5.106  (**** Isabelle FOL clauses ****)
   5.107  
   5.108 -(* by default it is false *)
   5.109  val tagged = ref false;
   5.110  
   5.111  type pred_name = string;
   5.112 @@ -223,7 +219,7 @@
   5.113                      functions: (string*int) list};
   5.114  
   5.115  
   5.116 -exception CLAUSE of string;
   5.117 +exception CLAUSE of string * term;
   5.118  
   5.119  
   5.120  (*** make clauses ***)
   5.121 @@ -233,6 +229,13 @@
   5.122        (not pol andalso a = "c_True")
   5.123    | isFalse _ = false;
   5.124  
   5.125 +fun isTrue (Literal (pol,Predicate(a,_,[]),_)) =
   5.126 +      (pol andalso a = "c_True") orelse
   5.127 +      (not pol andalso a = "c_False")
   5.128 +  | isTrue _ = false;
   5.129 +  
   5.130 +fun isTaut (Clause {literals,...}) = exists isTrue literals;  
   5.131 +
   5.132  fun make_clause (clause_id,axiom_name,kind,literals,
   5.133                   types_sorts,tvar_type_literals,
   5.134                   tfree_type_literals,tvars, predicates, functions) =
   5.135 @@ -303,10 +306,10 @@
   5.136        let val (typof,(folTyps,funcs)) = maybe_type_of c T
   5.137        in (make_fixed_const c, (typof,folTyps), funcs) end
   5.138    | pred_name_type (Free(x,T))  = 
   5.139 -      if isMeta x then raise CLAUSE("Predicate Not First Order") 
   5.140 +      if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) 
   5.141        else (make_fixed_var x, ("",[]), [])
   5.142 -  | pred_name_type (Var(_,_))   = raise CLAUSE("Predicate Not First Order")
   5.143 -  | pred_name_type _          = raise CLAUSE("Predicate input unexpected");
   5.144 +  | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v)
   5.145 +  | pred_name_type t        = raise CLAUSE("Predicate input unexpected", t);
   5.146  
   5.147  
   5.148  (* For type equality *)
   5.149 @@ -330,7 +333,7 @@
   5.150        in
   5.151  	    (t, ("",[]), [(t, length args)])
   5.152        end
   5.153 -  | fun_name_type _  args = raise CLAUSE("Function Not First Order");
   5.154 +  | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f);
   5.155  
   5.156  
   5.157  fun term_of (Var(ind_nm,T)) = 
   5.158 @@ -339,17 +342,19 @@
   5.159  	  (UVar(make_schematic_var ind_nm, folType), (ts, funcs))
   5.160        end
   5.161    | term_of (Free(x,T)) = 
   5.162 -      let val (folType,(ts, funcs)) = type_of T
   5.163 +      let val (folType, (ts,funcs)) = type_of T
   5.164        in
   5.165  	  if isMeta x then (UVar(make_schematic_var(x,0),folType),
   5.166  			    (ts, ((make_schematic_var(x,0)),0)::funcs))
   5.167  	  else
   5.168 -	      (Fun(make_fixed_var x,folType,[]), (ts, ((make_fixed_var x),0)::funcs))
   5.169 +	      (Fun(make_fixed_var x, folType, []), 
   5.170 +	       (ts, ((make_fixed_var x),0)::funcs))
   5.171        end
   5.172    | term_of (Const(c,T)) =  (* impossible to be equality *)
   5.173        let val (folType,(ts,funcs)) = type_of T
   5.174 -       in
   5.175 -	  (Fun(make_fixed_const c,folType,[]),(ts, ((make_fixed_const c),0)::funcs))
   5.176 +      in
   5.177 +	  (Fun(make_fixed_const c, folType, []),
   5.178 +	   (ts, ((make_fixed_const c),0)::funcs))
   5.179        end    
   5.180    | term_of (app as (t $ a)) = 
   5.181        let val (f,args) = strip_comb app
   5.182 @@ -360,7 +365,7 @@
   5.183  		  val ts3 = ResLib.flat_noDup (ts1::ts2)
   5.184  		  val funcs'' = ResLib.flat_noDup((funcs::funcs'))
   5.185  	      in
   5.186 -		  (Fun(funName,funType,args'),(ts3,funcs''))
   5.187 +		  (Fun(funName,funType,args'), (ts3,funcs''))
   5.188  	      end
   5.189  	  fun term_of_eq ((Const ("op =", typ)),args) =
   5.190  	      let val arg_typ = eq_arg_type typ
   5.191 @@ -370,60 +375,58 @@
   5.192  	      in
   5.193  		  (Fun(equal_name,arg_typ,args'),
   5.194  		   (ResLib.flat_noDup ts, 
   5.195 -		    (((make_fixed_var equal_name),2):: ResLib.flat_noDup funcs)))
   5.196 +		    (make_fixed_var equal_name, 2):: ResLib.flat_noDup funcs))
   5.197  	      end
   5.198        in
   5.199 -	    case f of Const ("op =", typ) => term_of_eq (f,args)
   5.200 -		  | Const(_,_) => term_of_aux ()
   5.201 -		    | Free(s,_)  => if isMeta s 
   5.202 -				    then raise CLAUSE("Function Not First Order") 
   5.203 -				    else term_of_aux()
   5.204 -		    | _          => raise CLAUSE("Function Not First Order")
   5.205 +	 case f of Const ("op =", typ) => term_of_eq (f,args)
   5.206 +		 | Const(_,_) => term_of_aux ()
   5.207 +		 | Free(s,_)  => 
   5.208 +		     if isMeta s 
   5.209 +		     then raise CLAUSE("Function Not First Order 2", f)
   5.210 +		     else term_of_aux()
   5.211 +		 | _ => raise CLAUSE("Function Not First Order 3", f)
   5.212        end
   5.213 -  | term_of _ = raise CLAUSE("Function Not First Order"); 
   5.214 +  | term_of t = raise CLAUSE("Function Not First Order 4", t); 
   5.215  
   5.216  
   5.217 -fun pred_of_eq ((Const ("op =", typ)),args) =
   5.218 -    let val arg_typ = eq_arg_type typ 
   5.219 -	val (args',ts_funcs) = ListPair.unzip (map term_of args)
   5.220 -        val (ts,funcs) = ListPair.unzip ts_funcs
   5.221 -	val equal_name = make_fixed_const "op ="
   5.222 -    in
   5.223 -	(Predicate(equal_name,arg_typ,args'),
   5.224 -	 ResLib.flat_noDup ts, 
   5.225 -	 [((make_fixed_var equal_name), 2)], 
   5.226 -	 (ResLib.flat_noDup funcs))
   5.227 -    end;
   5.228 -
   5.229 -(* The input "pred" cannot be an equality *)
   5.230 -fun pred_of_nonEq (pred,args) = 
   5.231 -    let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
   5.232 -	val (args',ts_funcs) = ListPair.unzip (map term_of args)
   5.233 -        val (ts2,ffuncs) = ListPair.unzip ts_funcs
   5.234 -	val ts3 = ResLib.flat_noDup (ts1::ts2)
   5.235 -        val ffuncs' = (ResLib.flat_noDup ffuncs)
   5.236 -        val newfuncs = distinct (pfuncs@ffuncs')
   5.237 -	val arity = 
   5.238 -	  case pred of
   5.239 -	      Const (c,_) => 
   5.240 -	            if !keep_types andalso not (no_types_needed c)
   5.241 -	            then 1 + length args
   5.242 -	            else length args
   5.243 -	    | _ => length args
   5.244 -    in
   5.245 -	(Predicate(predName,predType,args'), ts3, 
   5.246 -	 [(predName, arity)], newfuncs)
   5.247 -    end;
   5.248 +fun pred_of (Const("op =", typ), args) =
   5.249 +      let val arg_typ = eq_arg_type typ 
   5.250 +	  val (args',ts_funcs) = ListPair.unzip (map term_of args)
   5.251 +	  val (ts,funcs) = ListPair.unzip ts_funcs
   5.252 +	  val equal_name = make_fixed_const "op ="
   5.253 +      in
   5.254 +	  (Predicate(equal_name,arg_typ,args'),
   5.255 +	   ResLib.flat_noDup ts, 
   5.256 +	   [((make_fixed_var equal_name), 2)], 
   5.257 +	   (ResLib.flat_noDup funcs))
   5.258 +      end
   5.259 +  | pred_of (pred,args) = 
   5.260 +      let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
   5.261 +	  val (args',ts_funcs) = ListPair.unzip (map term_of args)
   5.262 +	  val (ts2,ffuncs) = ListPair.unzip ts_funcs
   5.263 +	  val ts3 = ResLib.flat_noDup (ts1::ts2)
   5.264 +	  val ffuncs' = (ResLib.flat_noDup ffuncs)
   5.265 +	  val newfuncs = distinct (pfuncs@ffuncs')
   5.266 +	  val arity = 
   5.267 +	    case pred of
   5.268 +		Const (c,_) => 
   5.269 +		      if !keep_types andalso not (no_types_needed c)
   5.270 +		      then 1 + length args
   5.271 +		      else length args
   5.272 +	      | _ => length args
   5.273 +      in
   5.274 +	  (Predicate(predName,predType,args'), ts3, 
   5.275 +	   [(predName, arity)], newfuncs)
   5.276 +      end;
   5.277  
   5.278  
   5.279 -(* Changed for typed equality *)
   5.280 -(* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *)
   5.281 -fun predicate_of term =
   5.282 -    let val (pred,args) = strip_comb term
   5.283 -    in
   5.284 -	case pred of (Const ("op =", _)) => pred_of_eq (pred,args)
   5.285 -		   | _ => pred_of_nonEq (pred,args)
   5.286 -    end;
   5.287 +(*Treatment of literals, possibly negated or tagged*)
   5.288 +fun predicate_of ((Const("Not",_) $ P), polarity, tag) =
   5.289 +      predicate_of (P, not polarity, tag)
   5.290 +  | predicate_of ((Const("HOL.tag",_) $ P), polarity, tag) =
   5.291 +      predicate_of (P, polarity, true)
   5.292 +  | predicate_of (term,polarity,tag) =
   5.293 +        (pred_of (strip_comb term), polarity, tag);
   5.294  
   5.295  fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) =    
   5.296        literals_of_term(P,lits_ts, preds, funcs)
   5.297 @@ -434,16 +437,10 @@
   5.298  	  literals_of_term(Q, (lits',ts'), distinct(preds'@preds), 
   5.299  	                   distinct(funcs'@funcs))
   5.300        end
   5.301 -  | literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = 
   5.302 -      let val (pred,ts', preds', funcs') = predicate_of P
   5.303 -	  val lits' = Literal(false,pred,false) :: lits
   5.304 -	  val ts'' = ResLib.no_rep_app ts ts'
   5.305 -      in
   5.306 -	  (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
   5.307 -      end
   5.308    | literals_of_term (P,(lits,ts), preds, funcs) = 
   5.309 -      let val (pred,ts', preds', funcs') = predicate_of P
   5.310 -	  val lits' = Literal(true,pred,false) :: lits
   5.311 +      let val ((pred,ts', preds', funcs'), pol, tag) = 
   5.312 +              predicate_of (P,true,false)
   5.313 +	  val lits' = Literal(pol,pred,tag) :: lits
   5.314  	  val ts'' = ResLib.no_rep_app ts ts' 
   5.315        in
   5.316  	  (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
   5.317 @@ -759,27 +756,24 @@
   5.318    end
   5.319  
   5.320   
   5.321 -fun get_uvars (UVar(str,typ)) = [str] 
   5.322 -|   get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
   5.323 -
   5.324 -
   5.325 -fun is_uvar  (UVar(str,typ)) = true
   5.326 -|   is_uvar  (Fun (str,typ,tlist)) = false;
   5.327 -
   5.328 -fun uvar_name  (UVar(str,typ)) = str
   5.329 -|   uvar_name  _ = (raise CLAUSE("Not a variable"));
   5.330 +fun get_uvars (UVar(a,typ)) = [a] 
   5.331 +|   get_uvars (Fun (_,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
   5.332  
   5.333  
   5.334 +fun is_uvar (UVar _) = true
   5.335 +|   is_uvar (Fun _) = false;
   5.336 +
   5.337 +fun uvar_name (UVar(a,_)) = a
   5.338 +|   uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
   5.339 +
   5.340  fun mergelist [] = []
   5.341 -|   mergelist (x::xs ) = x@(mergelist xs)
   5.342 -
   5.343 +|   mergelist (x::xs ) = x @ mergelist xs
   5.344  
   5.345  fun dfg_vars (Clause cls) =
   5.346 -    let val lits =  (#literals cls)
   5.347 +    let val lits = #literals cls
   5.348          val folterms = mergelist(map dfg_folterms lits)
   5.349 -        val vars =  ResLib.flat_noDup(map get_uvars folterms)	
   5.350      in 
   5.351 -        vars
   5.352 +        ResLib.flat_noDup(map get_uvars folterms)
   5.353      end
   5.354  
   5.355