1.1 --- a/src/HOL/HOL.thy	Wed Jul 05 16:24:10 2006 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Jul 05 16:24:28 2006 +0200
     1.3 @@ -1401,30 +1401,6 @@
     1.4  setup InductMethod.setup
     1.5  
     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 -
    1.31  subsection {* Code generator setup *}
    1.32  
    1.33  setup {*

     2.1 --- a/src/HOL/Tools/meson.ML	Wed Jul 05 16:24:10 2006 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Wed Jul 05 16:24:28 2006 +0200
     2.3 @@ -279,7 +279,7 @@
     2.4    incomplete, since when actually called, the only connectives likely to
     2.5    remain are & | Not.*)  
     2.6  val is_conn = member (op =)
     2.7 -    ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", 
     2.8 +    ["Trueprop", "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 @@ -386,13 +386,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 -  as well as tags applied to True and False. nnf_ss also includes the one-point simprocs,
    2.18 +(*The simplification removes defined quantifiers and occurrences of True and False. 
    2.19 +  nnf_ss also includes the one-point simprocs,
    2.20    which are needed to avoid the various one-point theorems from generating junk clauses.*)
    2.21 -val tag_True = thm "tag_True";
    2.22 -val tag_False = thm "tag_False";
    2.23  val nnf_simps =
    2.24 -     [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True, 
    2.25 +     [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, 
    2.26        if_False, if_cancel, if_eq_cancel, cases_simp];
    2.27  val nnf_extra_simps =
    2.28        thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;

     3.1 --- a/src/HOL/Tools/res_clause.ML	Wed Jul 05 16:24:10 2006 +0200
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Jul 05 16:24:28 2006 +0200
     3.3 @@ -196,18 +196,10 @@
     3.4  
     3.5  type clause_id = int;
     3.6  type axiom_name = string;
     3.7 -
     3.8 -
     3.9  type polarity = bool;
    3.10  
    3.11 -(* "tag" is used for vampire specific syntax FIXME REMOVE *)
    3.12 -type tag = bool; 
    3.13 -
    3.14 -
    3.15  (**** Isabelle FOL clauses ****)
    3.16  
    3.17 -val tagged = ref false;
    3.18 -
    3.19  type pred_name = string;
    3.20  
    3.21  datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    3.22 @@ -234,7 +226,7 @@
    3.23                   | Fun of string * fol_type list * fol_term list;
    3.24  datatype predicate = Predicate of pred_name * fol_type list * fol_term list;
    3.25  
    3.26 -datatype literal = Literal of polarity * predicate * tag;
    3.27 +datatype literal = Literal of polarity * predicate;
    3.28  
    3.29  fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
    3.30    | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
    3.31 @@ -253,12 +245,12 @@
    3.32  
    3.33  exception CLAUSE of string * term;
    3.34  
    3.35 -fun isFalse (Literal (pol,Predicate(pname,_,[]),_)) =
    3.36 +fun isFalse (Literal (pol, Predicate(pname,_,[]))) =
    3.37        (pol andalso pname = "c_False") orelse
    3.38        (not pol andalso pname = "c_True")
    3.39    | isFalse _ = false;
    3.40  
    3.41 -fun isTrue (Literal (pol,Predicate(pname,_,[]),_)) =
    3.42 +fun isTrue (Literal (pol, Predicate(pname,_,[]))) =
    3.43        (pol andalso pname = "c_True") orelse
    3.44        (not pol andalso pname = "c_False")
    3.45    | isTrue _ = false;
    3.46 @@ -352,20 +344,16 @@
    3.47  	  (Predicate(pname,predType,args'), union_all (ts1::ts2))
    3.48        end;
    3.49  
    3.50 -(*Treatment of literals, possibly negated or tagged*)
    3.51 -fun predicate_of ((Const("Not",_) $ P), polarity, tag) =
    3.52 -      predicate_of (P, not polarity, tag)
    3.53 -  | predicate_of ((Const("HOL.tag",_) $ P), polarity, tag) =
    3.54 -      predicate_of (P, polarity, true)
    3.55 -  | predicate_of (term,polarity,tag) =
    3.56 -        (pred_of (strip_comb term), polarity, tag);
    3.57 +(*Treatment of literals, possibly negated*)
    3.58 +fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity)
    3.59 +  | predicate_of (term,polarity) = (pred_of (strip_comb term), polarity);
    3.60  
    3.61  fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
    3.62    | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
    3.63        literals_of_term1 (literals_of_term1 args P) Q
    3.64    | literals_of_term1 (lits, ts) P =
    3.65 -      let val ((pred, ts'), polarity, tag) = predicate_of (P,true,false)
    3.66 -	  val lits' = Literal(polarity,pred,tag) :: lits
    3.67 +      let val ((pred, ts'), polarity) = predicate_of (P,true)
    3.68 +	  val lits' = Literal(polarity,pred) :: lits
    3.69        in
    3.70  	  (lits', ts union ts')
    3.71        end;
    3.72 @@ -423,7 +411,7 @@
    3.73    | too_general_terms (Fun _, _) = false
    3.74    | too_general_terms (UVar (a,_), t) = not (occurs a t);
    3.75  
    3.76 -fun too_general_lit (Literal (true,Predicate("equal",_,[x,y]),_)) =
    3.77 +fun too_general_lit (Literal (true, Predicate("equal",_,[x,y]))) =
    3.78        too_general_terms (x,y) orelse too_general_terms(y,x)
    3.79    | too_general_lit _ = false;
    3.80  
    3.81 @@ -433,17 +421,16 @@
    3.82  
    3.83  exception MAKE_CLAUSE;
    3.84  fun make_clause (clause_id, axiom_name, th, kind) =
    3.85 -    let val term = prop_of th
    3.86 -	val (lits,types_sorts) = literals_of_term term
    3.87 -    in if forall isFalse lits 
    3.88 -       then error "Problem too trivial for resolution (empty clause)"
    3.89 -       else
    3.90 -	   case kind of Axiom => 
    3.91 -			if forall too_general_lit lits then
    3.92 -			    (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); raise MAKE_CLAUSE)
    3.93 -			else Clause {clause_id = clause_id, axiom_name = axiom_name,th = th, kind = kind, literals = lits, types_sorts = types_sorts}
    3.94 -		      | _ =>  Clause {clause_id = clause_id, axiom_name = axiom_name,th = th, kind = kind, literals = lits, types_sorts = types_sorts}
    3.95 -    end;		     
    3.96 +  let val term = prop_of th
    3.97 +      val (lits,types_sorts) = literals_of_term term
    3.98 +  in if forall isFalse lits 
    3.99 +     then error "Problem too trivial for resolution (empty clause)"
   3.100 +     else if kind=Axiom andalso forall too_general_lit lits 
   3.101 +     then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); 
   3.102 +           raise MAKE_CLAUSE)
   3.103 +     else Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, 
   3.104 +                  kind = kind, literals = lits, types_sorts = types_sorts}
   3.105 +  end;		     
   3.106  
   3.107  fun get_tvar_strs [] = []
   3.108    | get_tvar_strs ((FOLTVar indx,s)::tss) = 
   3.109 @@ -585,7 +572,7 @@
   3.110    if pname = "equal" then preds (*equality is built-in and requires no declaration*)
   3.111    else Symtab.update (pname, length tys + length tms) preds
   3.112  
   3.113 -fun add_literal_preds (Literal(_,pred,_), preds) = add_predicate_preds (pred,preds)
   3.114 +fun add_literal_preds (Literal(_,pred), preds) = add_predicate_preds (pred,preds)
   3.115  
   3.116  fun add_type_sort_preds ((FOLTVar indx,s), preds) = 
   3.117        update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s)))
   3.118 @@ -629,7 +616,7 @@
   3.119  fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = 
   3.120      foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys;
   3.121  
   3.122 -fun add_literal_funcs (Literal(_,pred,_), funcs) = add_predicate_funcs (pred,funcs)
   3.123 +fun add_literal_funcs (Literal(_,pred), funcs) = add_predicate_funcs (pred,funcs)
   3.124  
   3.125  fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
   3.126    let val TConsLit(_, (_, tcons, tvars)) = conclLit
   3.127 @@ -691,7 +678,7 @@
   3.128  fun dfg_sign true s = s
   3.129    | dfg_sign false s = "not(" ^ s ^ ")"  
   3.130  
   3.131 -fun dfg_literal (Literal(pol,pred,tag)) = dfg_sign pol (string_of_predicate pred)
   3.132 +fun dfg_literal (Literal(pol,pred)) = dfg_sign pol (string_of_predicate pred)
   3.133  
   3.134  fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
   3.135    | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
   3.136 @@ -716,7 +703,7 @@
   3.137        (tvar_lits_strs @ lits, tfree_lits)
   3.138    end; 
   3.139  
   3.140 -fun dfg_folterms (Literal(pol,pred,tag)) = 
   3.141 +fun dfg_folterms (Literal(pol,pred)) = 
   3.142    let val Predicate (_, _, folterms) = pred
   3.143    in  folterms  end
   3.144  
   3.145 @@ -821,14 +808,8 @@
   3.146  fun tptp_sign true s = "++" ^ s
   3.147    | tptp_sign false s = "--" ^ s
   3.148  
   3.149 -fun tptp_literal (Literal(pol,pred,tag)) =  (*FIXME REMOVE TAGGING*)
   3.150 -    let val pred_string = string_of_predicate pred
   3.151 -	val tagged_pol = 
   3.152 -	      if (tag andalso !tagged) then (if pol then "+++" else "---")
   3.153 -	      else (if pol then "++" else "--")
   3.154 -     in
   3.155 -	tagged_pol ^ pred_string
   3.156 -    end;
   3.157 +fun tptp_literal (Literal(pol,pred)) = 
   3.158 +      (if pol then "++" else "--") ^ string_of_predicate pred;
   3.159  
   3.160  fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")"
   3.161    | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")";