--- a/src/HOL/Tools/res_axioms.ML Thu Sep 15 10:33:35 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Thu Sep 15 11:15:52 2005 +0200
@@ -8,18 +8,17 @@
signature RES_AXIOMS =
sig
exception ELIMR2FOL of string
+ val tagging_enabled : bool
val elimRule_tac : thm -> Tactical.tactic
val elimR2Fol : thm -> term
val transform_elim : thm -> thm
val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
val cnf_axiom : (string * thm) -> thm list
val meta_cnf_axiom : thm -> thm list
- val cnf_rule : thm -> thm list
- val cnf_rules : (string*thm) list -> thm list -> thm list list * thm list
val rm_Eps : (term * term) list -> thm list -> term list
val claset_rules_of_thy : theory -> (string * thm) list
val simpset_rules_of_thy : theory -> (string * thm) list
- val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list
+ val clausify_rules_pairs : (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list
val clause_setup : (theory -> theory) list
val meson_method_setup : (theory -> theory) list
end;
@@ -28,6 +27,8 @@
struct
+val tagging_enabled = false (*compile_time option*)
+
(**** Transformation of Elimination Rules into First-Order Formulas****)
(* a tactic used to prove an elim-rule. *)
@@ -133,8 +134,6 @@
(**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
-(* to be fixed: cnf_intro, cnf_rule, is_introR *)
-
(* repeated resolution *)
fun repeat_RS thm1 thm2 =
let val thm1' = thm1 RS thm2 handle THM _ => thm1
@@ -182,7 +181,7 @@
(*Traverse a term, accumulating Skolem function definitions.*)
fun declare_skofuns s t thy =
- let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, thy) =
+ let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val cname = s ^ "_" ^ Int.toString n
val args = term_frees xtp (*get the formal parameter list*)
@@ -194,20 +193,25 @@
val def = equals cT $ c $ rhs
val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
(*Theory is augmented with the constant, then its def*)
- val thy'' = Theory.add_defs_i false [(cname ^ "_def", def)] thy'
- in dec_sko (subst_bound (list_comb(c,args), p)) (n+1, thy'') end
- | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thy) =
+ val cdef = cname ^ "_def"
+ val thy'' = Theory.add_defs_i false [(cdef, def)] thy'
+ in dec_sko (subst_bound (list_comb(c,args), p))
+ (n+1, (thy'', get_axiom thy'' cdef :: axs))
+ end
+ | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
(*Universal quant: insert a free variable into body and continue*)
let val fname = variant (add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) (n, thy) end
+ in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
| dec_sko (Const ("op &", _) $ p $ q) nthy =
dec_sko q (dec_sko p nthy)
| dec_sko (Const ("op |", _) $ p $ q) nthy =
dec_sko q (dec_sko p nthy)
+ | dec_sko (Const ("HOL.tag", _) $ p) nthy =
+ dec_sko p nthy
| dec_sko (Const ("Trueprop", _) $ p) nthy =
dec_sko p nthy
- | dec_sko t (n,thy) = (n,thy) (*Do nothing otherwise*)
- in #2 (dec_sko t (1,thy)) end;
+ | dec_sko t nthx = nthx (*Do nothing otherwise*)
+ in #2 (dec_sko t (1, (thy,[]))) end;
(*cterms are used throughout for efficiency*)
val cTrueprop = Thm.cterm_of (Theory.sign_of HOL.thy) HOLogic.Trueprop;
@@ -251,8 +255,8 @@
(*Declare Skolem functions for a theorem, supplied in nnf and with its name*)
fun skolem thy (name,th) =
let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)
- val thy' = declare_skofuns cname (#prop (rep_thm th)) thy
- in (map (skolem_of_def o #2) (axioms_of thy'), thy') end;
+ val (thy',axs) = declare_skofuns cname (#prop (rep_thm th)) thy
+ in (map skolem_of_def axs, thy') end;
(*Populate the clause cache using the supplied theorems*)
fun skolemlist [] thy = thy
@@ -313,18 +317,15 @@
(sk_term,(t,sk_term)::epss)
end;
-
+(*FIXME: use a-list lookup!!*)
fun sk_lookup [] t = NONE
| sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then SOME (sk_tm) else (sk_lookup tms t);
-
-
(* get the proper skolem term to replace epsilon term *)
fun get_skolem epss t =
case (sk_lookup epss t) of NONE => get_new_skolem epss t
| SOME sk => (sk,epss);
-
fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) =
get_skolem epss t
| rm_Eps_cls_aux epss (P $ Q) =
@@ -333,11 +334,9 @@
in (P' $ Q',epss'') end
| rm_Eps_cls_aux epss t = (t,epss);
-
fun rm_Eps_cls epss th = rm_Eps_cls_aux epss (prop_of th);
-
-(* remove the epsilon terms in a formula, by skolem terms. *)
+(* replace the epsilon terms in a formula by skolem terms. *)
fun rm_Eps _ [] = []
| rm_Eps epss (th::thms) =
let val (th',epss') = rm_Eps_cls epss th
@@ -347,15 +346,26 @@
(**** Extract and Clausify theorems from a theory's claset and simpset ****)
+(*Preserve the name of "th" after the transformation "f"*)
+fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th);
+
+(*Tags identify the major premise or conclusion, as hints to resolution provers.
+ However, they don't appear to help in recent tests, and they complicate the code.*)
+val tagI = thm "tagI";
+val tagD = thm "tagD";
+
+val tag_intro = preserve_name (fn th => th RS tagI);
+val tag_elim = preserve_name (fn th => tagD RS th);
+
fun claset_rules_of_thy thy =
- let val clsset = rep_cs (claset_of thy)
- val safeEs = #safeEs clsset
- val safeIs = #safeIs clsset
- val hazEs = #hazEs clsset
- val hazIs = #hazIs clsset
- in
- map pairname (safeEs @ safeIs @ hazEs @ hazIs)
- end;
+ let val cs = rep_cs (claset_of thy)
+ val intros = (#safeIs cs) @ (#hazIs cs)
+ val elims = (#safeEs cs) @ (#hazEs cs)
+ in
+ if tagging_enabled
+ then map pairname (map tag_intro intros @ map tag_elim elims)
+ else map pairname (intros @ elims)
+ end;
fun simpset_rules_of_thy thy =
let val rules = #rules (fst (rep_ss (simpset_of thy)))
@@ -368,31 +378,40 @@
fun cnf_rules [] err_list = ([],err_list)
| cnf_rules ((name,th) :: thms) err_list =
let val (ts,es) = cnf_rules thms err_list
- in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; (* FIXME avoid handle _ *)
+ in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end;
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
+fun addclause (c,th) l =
+ if ResClause.isTaut c then l else (c,th) :: l;
+
(* outputs a list of (clause,thm) pairs *)
fun clausify_axiom_pairs (thm_name,thm) =
- let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
+ let val isa_clauses = cnf_axiom (thm_name,thm)
val isa_clauses' = rm_Eps [] isa_clauses
val clauses_n = length isa_clauses
- val thy = theory_of_thm thm
fun make_axiom_clauses _ [] []= []
| make_axiom_clauses i (cls::clss) (cls'::clss') =
- (ResClause.make_axiom_clause cls (thm_name,i), cls') ::
- make_axiom_clauses (i+1) clss clss'
+ addclause (ResClause.make_axiom_clause cls (thm_name,i), cls')
+ (make_axiom_clauses (i+1) clss clss')
in
make_axiom_clauses 0 isa_clauses' isa_clauses
- end;
+ end
fun clausify_rules_pairs [] err_list = ([],err_list)
| clausify_rules_pairs ((name,thm)::thms) err_list =
let val (ts,es) = clausify_rules_pairs thms err_list
in
((clausify_axiom_pairs (name,thm))::ts, es)
- handle _ => (ts, (thm::es)) (* FIXME avoid handle _ *)
+ handle THM (msg,_,_) =>
+ (debug ("Cannot clausify " ^ name ^ ": " ^ msg);
+ (ts, (thm::es)))
+ | ResClause.CLAUSE (msg,t) =>
+ (debug ("Cannot clausify " ^ name ^ ": " ^ msg ^
+ ": " ^ TermLib.string_of_term t);
+ (ts, (thm::es)))
+
end;
--- a/src/HOL/Tools/res_clause.ML Thu Sep 15 10:33:35 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Thu Sep 15 11:15:52 2005 +0200
@@ -10,49 +10,49 @@
(* works for writeoutclasimp on typed *)
signature RES_CLAUSE =
sig
- exception ARCLAUSE of string
- exception CLAUSE of string
- type arityClause
- type classrelClause
- val classrelClauses_of : string * string list -> classrelClause list
- type clause
- val init : theory -> unit
- val keep_types : bool ref
- val make_axiom_arity_clause :
- string * (string * string list list) -> arityClause
- val make_axiom_classrelClause :
- string * string option -> classrelClause
- val make_axiom_clause : Term.term -> string * int -> clause
- val make_conjecture_clause : Term.term -> clause
- val make_conjecture_clause_thm : Thm.thm -> clause
- val make_hypothesis_clause : Term.term -> clause
- val special_equal : bool ref
- val get_axiomName : clause -> string
- val typed : unit -> unit
- val untyped : unit -> unit
- val num_of_clauses : clause -> int
+ val keep_types : bool ref
+ val special_equal : bool ref
+ val tagged : bool ref
+
+ exception ARCLAUSE of string
+ exception CLAUSE of string * term
+ type arityClause
+ type classrelClause
+ val classrelClauses_of : string * string list -> classrelClause list
+ type clause
+ val init : theory -> unit
+ val make_axiom_arity_clause :
+ string * (string * string list list) -> arityClause
+ val make_axiom_classrelClause : string * string option -> classrelClause
+ val make_axiom_clause : Term.term -> string * int -> clause
+ val make_conjecture_clause : Term.term -> clause
+ val make_conjecture_clause_thm : Thm.thm -> clause
+ val make_hypothesis_clause : Term.term -> clause
+ val get_axiomName : clause -> string
+ val isTaut : clause -> bool
+ val num_of_clauses : clause -> int
- val dfg_clauses2str : string list -> string
- val clause2dfg : clause -> string * string list
- val clauses2dfg : clause list -> string -> clause list -> clause list ->
- (string * int) list -> (string * int) list -> string list -> string
- val tfree_dfg_clause : string -> string
+ val dfg_clauses2str : string list -> string
+ val clause2dfg : clause -> string * string list
+ val clauses2dfg : clause list -> string -> clause list -> clause list ->
+ (string * int) list -> (string * int) list -> string list -> string
+ val tfree_dfg_clause : string -> string
- val tptp_arity_clause : arityClause -> string
- val tptp_classrelClause : classrelClause -> string
- val tptp_clause : clause -> string list
- val tptp_clauses2str : string list -> string
- val clause2tptp : clause -> string * string list
- val tfree_clause : string -> string
- val schematic_var_prefix : string
- val fixed_var_prefix : string
- val tvar_prefix : string
- val tfree_prefix : string
- val clause_prefix : string
- val arclause_prefix : string
- val const_prefix : string
- val tconst_prefix : string
- val class_prefix : string
+ val tptp_arity_clause : arityClause -> string
+ val tptp_classrelClause : classrelClause -> string
+ val tptp_clause : clause -> string list
+ val tptp_clauses2str : string list -> string
+ val clause2tptp : clause -> string * string list
+ val tfree_clause : string -> string
+ val schematic_var_prefix : string
+ val fixed_var_prefix : string
+ val tvar_prefix : string
+ val tfree_prefix : string
+ val clause_prefix : string
+ val arclause_prefix : string
+ val const_prefix : string
+ val tconst_prefix : string
+ val class_prefix : string
end;
structure ResClause: RES_CLAUSE =
@@ -157,9 +157,6 @@
(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****)
val keep_types = ref true;
-fun untyped () = (keep_types := false);
-fun typed () = (keep_types := true);
-
datatype kind = Axiom | Hypothesis | Conjecture;
fun name_of_kind Axiom = "axiom"
@@ -189,7 +186,6 @@
(**** Isabelle FOL clauses ****)
-(* by default it is false *)
val tagged = ref false;
type pred_name = string;
@@ -223,7 +219,7 @@
functions: (string*int) list};
-exception CLAUSE of string;
+exception CLAUSE of string * term;
(*** make clauses ***)
@@ -233,6 +229,13 @@
(not pol andalso a = "c_True")
| isFalse _ = false;
+fun isTrue (Literal (pol,Predicate(a,_,[]),_)) =
+ (pol andalso a = "c_True") orelse
+ (not pol andalso a = "c_False")
+ | isTrue _ = false;
+
+fun isTaut (Clause {literals,...}) = exists isTrue literals;
+
fun make_clause (clause_id,axiom_name,kind,literals,
types_sorts,tvar_type_literals,
tfree_type_literals,tvars, predicates, functions) =
@@ -303,10 +306,10 @@
let val (typof,(folTyps,funcs)) = maybe_type_of c T
in (make_fixed_const c, (typof,folTyps), funcs) end
| pred_name_type (Free(x,T)) =
- if isMeta x then raise CLAUSE("Predicate Not First Order")
+ if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T))
else (make_fixed_var x, ("",[]), [])
- | pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order")
- | pred_name_type _ = raise CLAUSE("Predicate input unexpected");
+ | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v)
+ | pred_name_type t = raise CLAUSE("Predicate input unexpected", t);
(* For type equality *)
@@ -330,7 +333,7 @@
in
(t, ("",[]), [(t, length args)])
end
- | fun_name_type _ args = raise CLAUSE("Function Not First Order");
+ | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f);
fun term_of (Var(ind_nm,T)) =
@@ -339,17 +342,19 @@
(UVar(make_schematic_var ind_nm, folType), (ts, funcs))
end
| term_of (Free(x,T)) =
- let val (folType,(ts, funcs)) = type_of T
+ let val (folType, (ts,funcs)) = type_of T
in
if isMeta x then (UVar(make_schematic_var(x,0),folType),
(ts, ((make_schematic_var(x,0)),0)::funcs))
else
- (Fun(make_fixed_var x,folType,[]), (ts, ((make_fixed_var x),0)::funcs))
+ (Fun(make_fixed_var x, folType, []),
+ (ts, ((make_fixed_var x),0)::funcs))
end
| term_of (Const(c,T)) = (* impossible to be equality *)
let val (folType,(ts,funcs)) = type_of T
- in
- (Fun(make_fixed_const c,folType,[]),(ts, ((make_fixed_const c),0)::funcs))
+ in
+ (Fun(make_fixed_const c, folType, []),
+ (ts, ((make_fixed_const c),0)::funcs))
end
| term_of (app as (t $ a)) =
let val (f,args) = strip_comb app
@@ -360,7 +365,7 @@
val ts3 = ResLib.flat_noDup (ts1::ts2)
val funcs'' = ResLib.flat_noDup((funcs::funcs'))
in
- (Fun(funName,funType,args'),(ts3,funcs''))
+ (Fun(funName,funType,args'), (ts3,funcs''))
end
fun term_of_eq ((Const ("op =", typ)),args) =
let val arg_typ = eq_arg_type typ
@@ -370,60 +375,58 @@
in
(Fun(equal_name,arg_typ,args'),
(ResLib.flat_noDup ts,
- (((make_fixed_var equal_name),2):: ResLib.flat_noDup funcs)))
+ (make_fixed_var equal_name, 2):: ResLib.flat_noDup funcs))
end
in
- case f of Const ("op =", typ) => term_of_eq (f,args)
- | Const(_,_) => term_of_aux ()
- | Free(s,_) => if isMeta s
- then raise CLAUSE("Function Not First Order")
- else term_of_aux()
- | _ => raise CLAUSE("Function Not First Order")
+ case f of Const ("op =", typ) => term_of_eq (f,args)
+ | Const(_,_) => term_of_aux ()
+ | Free(s,_) =>
+ if isMeta s
+ then raise CLAUSE("Function Not First Order 2", f)
+ else term_of_aux()
+ | _ => raise CLAUSE("Function Not First Order 3", f)
end
- | term_of _ = raise CLAUSE("Function Not First Order");
+ | term_of t = raise CLAUSE("Function Not First Order 4", t);
-fun pred_of_eq ((Const ("op =", typ)),args) =
- let val arg_typ = eq_arg_type typ
- val (args',ts_funcs) = ListPair.unzip (map term_of args)
- val (ts,funcs) = ListPair.unzip ts_funcs
- val equal_name = make_fixed_const "op ="
- in
- (Predicate(equal_name,arg_typ,args'),
- ResLib.flat_noDup ts,
- [((make_fixed_var equal_name), 2)],
- (ResLib.flat_noDup funcs))
- end;
-
-(* The input "pred" cannot be an equality *)
-fun pred_of_nonEq (pred,args) =
- let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
- val (args',ts_funcs) = ListPair.unzip (map term_of args)
- val (ts2,ffuncs) = ListPair.unzip ts_funcs
- val ts3 = ResLib.flat_noDup (ts1::ts2)
- val ffuncs' = (ResLib.flat_noDup ffuncs)
- val newfuncs = distinct (pfuncs@ffuncs')
- val arity =
- case pred of
- Const (c,_) =>
- if !keep_types andalso not (no_types_needed c)
- then 1 + length args
- else length args
- | _ => length args
- in
- (Predicate(predName,predType,args'), ts3,
- [(predName, arity)], newfuncs)
- end;
+fun pred_of (Const("op =", typ), args) =
+ let val arg_typ = eq_arg_type typ
+ val (args',ts_funcs) = ListPair.unzip (map term_of args)
+ val (ts,funcs) = ListPair.unzip ts_funcs
+ val equal_name = make_fixed_const "op ="
+ in
+ (Predicate(equal_name,arg_typ,args'),
+ ResLib.flat_noDup ts,
+ [((make_fixed_var equal_name), 2)],
+ (ResLib.flat_noDup funcs))
+ end
+ | pred_of (pred,args) =
+ let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
+ val (args',ts_funcs) = ListPair.unzip (map term_of args)
+ val (ts2,ffuncs) = ListPair.unzip ts_funcs
+ val ts3 = ResLib.flat_noDup (ts1::ts2)
+ val ffuncs' = (ResLib.flat_noDup ffuncs)
+ val newfuncs = distinct (pfuncs@ffuncs')
+ val arity =
+ case pred of
+ Const (c,_) =>
+ if !keep_types andalso not (no_types_needed c)
+ then 1 + length args
+ else length args
+ | _ => length args
+ in
+ (Predicate(predName,predType,args'), ts3,
+ [(predName, arity)], newfuncs)
+ end;
-(* Changed for typed equality *)
-(* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *)
-fun predicate_of term =
- let val (pred,args) = strip_comb term
- in
- case pred of (Const ("op =", _)) => pred_of_eq (pred,args)
- | _ => pred_of_nonEq (pred,args)
- 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);
fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) =
literals_of_term(P,lits_ts, preds, funcs)
@@ -434,16 +437,10 @@
literals_of_term(Q, (lits',ts'), distinct(preds'@preds),
distinct(funcs'@funcs))
end
- | literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) =
- let val (pred,ts', preds', funcs') = predicate_of P
- val lits' = Literal(false,pred,false) :: lits
- val ts'' = ResLib.no_rep_app ts ts'
- in
- (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
- end
| literals_of_term (P,(lits,ts), preds, funcs) =
- let val (pred,ts', preds', funcs') = predicate_of P
- val lits' = Literal(true,pred,false) :: lits
+ let val ((pred,ts', preds', funcs'), pol, tag) =
+ predicate_of (P,true,false)
+ val lits' = Literal(pol,pred,tag) :: lits
val ts'' = ResLib.no_rep_app ts ts'
in
(lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
@@ -759,27 +756,24 @@
end
-fun get_uvars (UVar(str,typ)) = [str]
-| get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
-
-
-fun is_uvar (UVar(str,typ)) = true
-| is_uvar (Fun (str,typ,tlist)) = false;
-
-fun uvar_name (UVar(str,typ)) = str
-| uvar_name _ = (raise CLAUSE("Not a variable"));
+fun get_uvars (UVar(a,typ)) = [a]
+| get_uvars (Fun (_,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
+fun is_uvar (UVar _) = true
+| is_uvar (Fun _) = false;
+
+fun uvar_name (UVar(a,_)) = a
+| uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
+
fun mergelist [] = []
-| mergelist (x::xs ) = x@(mergelist xs)
-
+| mergelist (x::xs ) = x @ mergelist xs
fun dfg_vars (Clause cls) =
- let val lits = (#literals cls)
+ let val lits = #literals cls
val folterms = mergelist(map dfg_folterms lits)
- val vars = ResLib.flat_noDup(map get_uvars folterms)
in
- vars
+ ResLib.flat_noDup(map get_uvars folterms)
end