# HG changeset patch # User paulson # Date 1152109468 -7200 # Node ID 5419a71d0baae880f3cc2227fddd97f010836ca9 # Parent a2070352371c8c6151a87d24443e7bab59f06881 removed the "tagging" feature diff -r a2070352371c -r 5419a71d0baa src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jul 05 16:24:10 2006 +0200 +++ b/src/HOL/HOL.thy Wed Jul 05 16:24:28 2006 +0200 @@ -1401,30 +1401,6 @@ setup InductMethod.setup -subsubsection {*Tags, for the ATP Linkup *} - -constdefs - tag :: "bool => bool" - "tag P == P" - -text{*These label the distinguished literals of introduction and elimination -rules.*} - -lemma tagI: "P ==> tag P" -by (simp add: tag_def) - -lemma tagD: "tag P ==> P" -by (simp add: tag_def) - -text{*Applications of "tag" to True and False must go!*} - -lemma tag_True: "tag True = True" -by (simp add: tag_def) - -lemma tag_False: "tag False = False" -by (simp add: tag_def) - - subsection {* Code generator setup *} setup {* diff -r a2070352371c -r 5419a71d0baa src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Jul 05 16:24:10 2006 +0200 +++ b/src/HOL/Tools/meson.ML Wed Jul 05 16:24:28 2006 +0200 @@ -279,7 +279,7 @@ incomplete, since when actually called, the only connectives likely to remain are & | Not.*) val is_conn = member (op =) - ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", + ["Trueprop", "op &", "op |", "op -->", "op =", "Not", "All", "Ex", "Ball", "Bex"]; (*True if the term contains a function where the type of any argument contains @@ -386,13 +386,11 @@ (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) handle THM _ => th; -(*The simplification removes defined quantifiers and occurrences of True and False, - as well as tags applied to True and False. nnf_ss also includes the one-point simprocs, +(*The simplification removes defined quantifiers and occurrences of True and False. + nnf_ss also includes the one-point simprocs, which are needed to avoid the various one-point theorems from generating junk clauses.*) -val tag_True = thm "tag_True"; -val tag_False = thm "tag_False"; val nnf_simps = - [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True, + [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, if_False, if_cancel, if_eq_cancel, cases_simp]; val nnf_extra_simps = thms"split_ifs" @ ex_simps @ all_simps @ simp_thms; diff -r a2070352371c -r 5419a71d0baa src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Jul 05 16:24:10 2006 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Jul 05 16:24:28 2006 +0200 @@ -196,18 +196,10 @@ type clause_id = int; type axiom_name = string; - - type polarity = bool; -(* "tag" is used for vampire specific syntax FIXME REMOVE *) -type tag = bool; - - (**** Isabelle FOL clauses ****) -val tagged = ref false; - type pred_name = string; datatype typ_var = FOLTVar of indexname | FOLTFree of string; @@ -234,7 +226,7 @@ | Fun of string * fol_type list * fol_term list; datatype predicate = Predicate of pred_name * fol_type list * fol_term list; -datatype literal = Literal of polarity * predicate * tag; +datatype literal = Literal of polarity * predicate; fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); @@ -253,12 +245,12 @@ exception CLAUSE of string * term; -fun isFalse (Literal (pol,Predicate(pname,_,[]),_)) = +fun isFalse (Literal (pol, Predicate(pname,_,[]))) = (pol andalso pname = "c_False") orelse (not pol andalso pname = "c_True") | isFalse _ = false; -fun isTrue (Literal (pol,Predicate(pname,_,[]),_)) = +fun isTrue (Literal (pol, Predicate(pname,_,[]))) = (pol andalso pname = "c_True") orelse (not pol andalso pname = "c_False") | isTrue _ = false; @@ -352,20 +344,16 @@ (Predicate(pname,predType,args'), union_all (ts1::ts2)) end; -(*Treatment of literals, possibly negated or tagged*) -fun predicate_of ((Const("Not",_) $ P), polarity, tag) = - predicate_of (P, not polarity, tag) - | predicate_of ((Const("HOL.tag",_) $ P), polarity, tag) = - predicate_of (P, polarity, true) - | predicate_of (term,polarity,tag) = - (pred_of (strip_comb term), polarity, tag); +(*Treatment of literals, possibly negated*) +fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity) + | predicate_of (term,polarity) = (pred_of (strip_comb term), polarity); fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P | literals_of_term1 args (Const("op |",_) $ P $ Q) = literals_of_term1 (literals_of_term1 args P) Q | literals_of_term1 (lits, ts) P = - let val ((pred, ts'), polarity, tag) = predicate_of (P,true,false) - val lits' = Literal(polarity,pred,tag) :: lits + let val ((pred, ts'), polarity) = predicate_of (P,true) + val lits' = Literal(polarity,pred) :: lits in (lits', ts union ts') end; @@ -423,7 +411,7 @@ | too_general_terms (Fun _, _) = false | too_general_terms (UVar (a,_), t) = not (occurs a t); -fun too_general_lit (Literal (true,Predicate("equal",_,[x,y]),_)) = +fun too_general_lit (Literal (true, Predicate("equal",_,[x,y]))) = too_general_terms (x,y) orelse too_general_terms(y,x) | too_general_lit _ = false; @@ -433,17 +421,16 @@ exception MAKE_CLAUSE; fun make_clause (clause_id, axiom_name, th, kind) = - let val term = prop_of th - val (lits,types_sorts) = literals_of_term term - in if forall isFalse lits - then error "Problem too trivial for resolution (empty clause)" - else - case kind of Axiom => - if forall too_general_lit lits then - (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); raise MAKE_CLAUSE) - else Clause {clause_id = clause_id, axiom_name = axiom_name,th = th, kind = kind, literals = lits, types_sorts = types_sorts} - | _ => Clause {clause_id = clause_id, axiom_name = axiom_name,th = th, kind = kind, literals = lits, types_sorts = types_sorts} - end; + let val term = prop_of th + val (lits,types_sorts) = literals_of_term term + in if forall isFalse lits + then error "Problem too trivial for resolution (empty clause)" + else if kind=Axiom andalso forall too_general_lit lits + then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); + raise MAKE_CLAUSE) + else Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, + kind = kind, literals = lits, types_sorts = types_sorts} + end; fun get_tvar_strs [] = [] | get_tvar_strs ((FOLTVar indx,s)::tss) = @@ -585,7 +572,7 @@ if pname = "equal" then preds (*equality is built-in and requires no declaration*) else Symtab.update (pname, length tys + length tms) preds -fun add_literal_preds (Literal(_,pred,_), preds) = add_predicate_preds (pred,preds) +fun add_literal_preds (Literal(_,pred), preds) = add_predicate_preds (pred,preds) fun add_type_sort_preds ((FOLTVar indx,s), preds) = update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s))) @@ -629,7 +616,7 @@ fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys; -fun add_literal_funcs (Literal(_,pred,_), funcs) = add_predicate_funcs (pred,funcs) +fun add_literal_funcs (Literal(_,pred), funcs) = add_predicate_funcs (pred,funcs) fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) = let val TConsLit(_, (_, tcons, tvars)) = conclLit @@ -691,7 +678,7 @@ fun dfg_sign true s = s | dfg_sign false s = "not(" ^ s ^ ")" -fun dfg_literal (Literal(pol,pred,tag)) = dfg_sign pol (string_of_predicate pred) +fun dfg_literal (Literal(pol,pred)) = dfg_sign pol (string_of_predicate pred) fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))" | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")"; @@ -716,7 +703,7 @@ (tvar_lits_strs @ lits, tfree_lits) end; -fun dfg_folterms (Literal(pol,pred,tag)) = +fun dfg_folterms (Literal(pol,pred)) = let val Predicate (_, _, folterms) = pred in folterms end @@ -821,14 +808,8 @@ fun tptp_sign true s = "++" ^ s | tptp_sign false s = "--" ^ s -fun tptp_literal (Literal(pol,pred,tag)) = (*FIXME REMOVE TAGGING*) - let val pred_string = string_of_predicate pred - val tagged_pol = - if (tag andalso !tagged) then (if pol then "+++" else "---") - else (if pol then "++" else "--") - in - tagged_pol ^ pred_string - end; +fun tptp_literal (Literal(pol,pred)) = + (if pol then "++" else "--") ^ string_of_predicate pred; fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")" | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")";