# HG changeset patch # User paulson # Date 1101835555 -3600 # Node ID 14585bc8fa09380635fb393521e4d165b80bb1a0 # Parent ac272926fb771a1477e39d47444bfedfde8416a3 resolution package tools by Jia Meng diff -r ac272926fb77 -r 14585bc8fa09 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Nov 30 16:27:44 2004 +0100 +++ b/src/HOL/IsaMakefile Tue Nov 30 18:25:55 2004 +0100 @@ -102,14 +102,12 @@ Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \ Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \ Tools/meson.ML Tools/numeral_syntax.ML \ - Tools/primrec_package.ML \ - Tools/prop_logic.ML \ - Tools/recdef_package.ML Tools/recfun_codegen.ML \ - Tools/record_package.ML \ + Tools/primrec_package.ML Tools/prop_logic.ML \ + Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \ Tools/refute.ML Tools/refute_isar.ML \ - Tools/rewrite_hol_proof.ML \ - Tools/sat_solver.ML \ - Tools/specification_package.ML \ + Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\ + Tools/res_axioms.ML Tools/res_types_sorts.ML Tools/res_atp.ML\ + Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \ Tools/split_rule.ML Tools/typedef_package.ML \ Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \ diff -r ac272926fb77 -r 14585bc8fa09 src/HOL/Tools/res_atp.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/res_atp.ML Tue Nov 30 18:25:55 2004 +0100 @@ -0,0 +1,138 @@ +(* Author: Jia Meng, Cambridge University Computer Laboratory + ID: $Id$ + Copyright 2004 University of Cambridge + +ATPs with TPTP format input. +*) +signature RES_ATP = +sig + +val trace_res : bool ref +val axiom_file : Path.T +val hyps_file : Path.T +val isar_atp : Thm.thm list * Thm.thm -> unit +val prob_file : Path.T +val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic +val atp_tac : int -> Tactical.tactic + +end; + +structure ResAtp : RES_ATP = + +struct + +(* default value is false *) + +val trace_res = ref false; + +val skolem_tac = skolemize_tac; + + +val atomize_tac = + SUBGOAL + (fn (prop,_) => + let val ts = Logic.strip_assums_hyp prop + in EVERY1 + [METAHYPS + (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), + REPEAT_DETERM_N (length ts) o (etac thin_rl)] + end); + +(* temporarily use these files, which will be loaded by Vampire *) +val prob_file = File.tmp_path (Path.basic "prob"); +val axiom_file = File.tmp_path (Path.basic "axioms"); +val hyps_file = File.tmp_path (Path.basic "hyps"); +val dummy_tac = PRIMITIVE(fn thm => thm ); + + + +fun tptp_inputs thms = + let val clss = map (ResClause.make_conjecture_clause_thm) thms + val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss) + val probfile = File.sysify_path prob_file + val out = TextIO.openOut(probfile) + in + (ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ())) + end; + + +(**** for Isabelle/ML interface ****) + +fun call_atp_tac thms = (tptp_inputs thms; dummy_tac); + + +val atp_tac = SELECT_GOAL + (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac, + METAHYPS(fn negs => (call_atp_tac(make_clauses negs)))]); + + +fun atp_ax_tac axioms n = + let val axcls = ResLib.flat_noDup(map ResAxioms.clausify_axiom axioms) + val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup(map ResClause.tptp_clause axcls)) + val axiomfile = File.sysify_path axiom_file + val out = TextIO.openOut (axiomfile) + in + (TextIO.output(out,axcls_str);TextIO.closeOut out; if !trace_res then (warning axiomfile) else (); atp_tac n) + end; + + +fun atp thm = + let val prems = prems_of thm + in + case prems of [] => () + | _ => (atp_tac 1 thm; ()) + end; + + +(**** For running in Isar ****) + +(* same function as that in res_axioms.ML *) +fun repeat_RS thm1 thm2 = + let val thm1' = thm1 RS thm2 handle THM _ => thm1 + in + if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) + end; + +(* a special version of repeat_RS *) +fun repeat_someI_ex thm = repeat_RS thm someI_ex; + + + +fun isar_atp_h thms = + let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms + val prems' = map repeat_someI_ex prems + val prems'' = make_clauses prems' + val prems''' = ResAxioms.rm_Eps [] prems'' + val clss = map ResClause.make_hypothesis_clause prems''' + val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss) + val hypsfile = File.sysify_path hyps_file + val out = TextIO.openOut(hypsfile) + in + (ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; if !trace_res then (warning hypsfile) else ()) + end; + + + + +val isar_atp_g = atp_tac; + +fun isar_atp_aux thms thm = + (isar_atp_h thms; isar_atp_g 1 thm;()); + + + + + +(* called in Isar automatically *) +fun isar_atp (thms, thm) = + let val prems = prems_of thm + in + case prems of [] => () + | _ => (isar_atp_aux thms thm) + end; + +end; + +Proof.atp_hook := ResAtp.isar_atp; + + diff -r ac272926fb77 -r 14585bc8fa09 src/HOL/Tools/res_axioms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/res_axioms.ML Tue Nov 30 18:25:55 2004 +0100 @@ -0,0 +1,471 @@ +(* Author: Jia Meng, Cambridge University Computer Laboratory + ID: $Id$ + Copyright 2004 University of Cambridge + +Transformation of axiom rules (elim/intro/etc) into CNF forms. +*) + + + +signature RES_ELIM_RULE = +sig + +exception ELIMR2FOL of string +val elimRule_tac : Thm.thm -> Tactical.tactic +val elimR2Fol : Thm.thm -> Term.term +val transform_elim : Thm.thm -> Thm.thm + +end; + +structure ResElimRule: RES_ELIM_RULE = + +struct + + +fun elimRule_tac thm = + ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN + REPEAT(Blast_tac 1); + + +(* This following version fails sometimes, need to investigate, do not use it now. *) +fun elimRule_tac' thm = + ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN + REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); + + +exception ELIMR2FOL of string; + +fun make_imp (prem,concl) = Const("op -->", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ prem $ concl; + + +fun make_disjs [x] = x + | make_disjs (x :: xs) = Const("op |",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_disjs xs) + + +fun make_conjs [x] = x + | make_conjs (x :: xs) = Const("op &", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_conjs xs) + + +fun add_EX term [] = term + | add_EX term ((x,xtp)::xs) = add_EX (Const ("Ex",Type("fun",[Type("fun",[xtp,Type("bool",[])]),Type("bool",[])])) $ Abs (x,xtp,term)) xs; + + +exception TRUEPROP of string; + +fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P + | strip_trueprop _ = raise TRUEPROP("not a prop!"); + + + +exception STRIP_CONCL; + + +fun strip_concl prems bvs (Const ("all", _) $ Abs (x,xtp,body)) = strip_concl prems ((x,xtp)::bvs) body + | strip_concl prems bvs (Const ("==>",_) $ P $ Q) = + let val P' = strip_trueprop P + val prems' = P'::prems + in + strip_concl prems' bvs Q + end + | strip_concl prems bvs _ = add_EX (make_conjs prems) bvs; + + + +fun trans_elim (main,others) = + let val others' = map (strip_concl [] []) others + val disjs = make_disjs others' + in + make_imp(strip_trueprop main,disjs) + end; + + +fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P; + + +fun elimR2Fol_aux prems = + let val nprems = length prems + val main = hd prems + in + if (nprems = 1) then neg (strip_trueprop main) + else trans_elim (main, tl prems) + end; + + +fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term; + + +fun elimR2Fol elimR = + let val elimR' = Drule.freeze_all elimR + val (prems,concl) = (prems_of elimR', concl_of elimR') + in + case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) + => trueprop (elimR2Fol_aux prems) + | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems) + | _ => raise ELIMR2FOL("Not an elimination rule!") + end; + + + + +(**** use prove_goalw_cterm to prove ****) + +fun transform_elim thm = + let val tm = elimR2Fol thm + val ctm = cterm_of (sign_of_thm thm) tm + in + prove_goalw_cterm [] ctm (fn prems => [elimRule_tac thm]) + end; + + +end; + + +(* some lemmas *) + +(* TO BE FIXED: the names of these lemmas should be made local, to avoid confusion with external global lemmas. *) + +Goal "(P==True) ==> P"; +by(Blast_tac 1); +qed "Eq_TrueD1"; + +Goal "(P=True) ==> P"; +by(Blast_tac 1); +qed "Eq_TrueD2"; + + +Goal "(P==False) ==> ~P"; +by(Blast_tac 1); +qed "Eq_FalseD1"; + +Goal "(P=False) ==> ~P"; +by(Blast_tac 1); +qed "Eq_FalseD2"; + +Goal "(P | True) == True"; +by(Simp_tac 1); +qed "s1"; + +Goal "(True | P) == True"; +by(Simp_tac 1); +qed "s2"; + +Goal "(P & True) == P"; +by(Simp_tac 1); +qed "s3"; + +Goal "(True & P) == P"; +by(Simp_tac 1); +qed "s4"; + +Goal "(False | P) == P"; +by(Simp_tac 1); +qed "s5"; + + +Goal "(P | False) == P"; +by(Simp_tac 1); +qed "s6"; + +Goal "(False & P) == False"; +by(Simp_tac 1); +qed "s7"; + +Goal "(P & False) == False"; +by(Simp_tac 1); +qed "s8"; + +Goal "~True == False"; +by(Simp_tac 1); +qed "s9"; + +Goal "~False == True"; +by(Simp_tac 1); +qed "s10"; + + +val small_simpset = empty_ss addsimps [s1,s2,s3,s4,s5,s6,s7,s8,s9,s10]; + + + +signature RES_AXIOMS = +sig + +val clausify_axiom : Thm.thm -> ResClause.clause list +val cnf_axiom : Thm.thm -> Thm.thm list +val cnf_elim : Thm.thm -> Thm.thm list +val cnf_intro : Thm.thm -> Thm.thm list +val cnf_rule : Thm.thm -> Thm.thm list +val cnf_classical_rules_thy : Theory.theory -> Thm.thm list list * Thm.thm list +val clausify_classical_rules_thy +: Theory.theory -> ResClause.clause list list * Thm.thm list +val cnf_simpset_rules_thy +: Theory.theory -> Thm.thm list list * Thm.thm list +val clausify_simpset_rules_thy +: Theory.theory -> ResClause.clause list list * Thm.thm list +val rm_Eps +: (Term.term * Term.term) list -> Thm.thm list -> Term.term list +end; + +structure ResAxioms : RES_AXIOMS = + +struct + +open ResElimRule; + +(* to be fixed: cnf_intro, cnf_rule, is_introR *) + +fun is_elimR thm = + case (concl_of thm) of (Const ("Trueprop", _) $ Var (idx,_)) => true + | Var(indx,Type("prop",[])) => true + | _ => false; + + + +fun repeat_RS thm1 thm2 = + let val thm1' = thm1 RS thm2 handle THM _ => thm1 + in + if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) + end; + + + +(* added this function to remove True/False in a theorem that is in NNF form. *) +fun rm_TF_nnf thm = simplify small_simpset thm; + +fun skolem_axiom thm = + let val thm' = (skolemize o rm_TF_nnf o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm + in + repeat_RS thm' someI_ex + end; + + +fun isa_cls thm = + let val thm' = skolem_axiom thm + in + map standard (make_clauses [thm']) + end; + + +fun cnf_elim thm = + let val thm' = transform_elim thm; + in + isa_cls thm' + end; + + +val cnf_intro = isa_cls; +val cnf_rule = isa_cls; + + +fun is_introR thm = true; + + + +(* transfer a theorem in to theory Main.thy if it is not already inside Main.thy *) +fun transfer_to_Main thm = transfer Main.thy thm handle THM _ => thm; + +(* remove "True" clause *) +fun rm_redundant_cls [] = [] + | rm_redundant_cls (thm::thms) = + let val t = prop_of thm + in + case t of (Const ("Trueprop", _) $ Const ("True", _)) => rm_redundant_cls thms + | _ => thm::(rm_redundant_cls thms) + end; + +(* transform an Isabelle thm into CNF *) +fun cnf_axiom thm = + let val thm' = transfer_to_Main thm + val thm'' = if (is_elimR thm') then (cnf_elim thm') + else (if (is_introR thm') then cnf_intro thm' else cnf_rule thm') + in + rm_redundant_cls thm'' + end; + + +(* changed: with one extra case added *) +fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars + | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars (* EX x. body *) + | univ_vars_of_aux (P $ Q) vars = + let val vars' = univ_vars_of_aux P vars + in + univ_vars_of_aux Q vars' + end + | univ_vars_of_aux (t as Var(_,_)) vars = + if (t mem vars) then vars else (t::vars) + | univ_vars_of_aux _ vars = vars; + + +fun univ_vars_of t = univ_vars_of_aux t []; + + +fun get_new_skolem epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,tp,_))) = + let val all_vars = univ_vars_of t + val sk_term = ResSkolemFunction.gen_skolem all_vars tp + in + (sk_term,(t,sk_term)::epss) + end; + + +fun sk_lookup [] t = None + | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then Some (sk_tm) else (sk_lookup tms t); + + +fun get_skolem epss t = + let val sk_fun = sk_lookup epss t + in + case sk_fun of None => get_new_skolem epss t + | Some sk => (sk,epss) + end; + + +fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t + | rm_Eps_cls_aux epss (P $ Q) = + let val (P',epss') = rm_Eps_cls_aux epss P + val (Q',epss'') = rm_Eps_cls_aux epss' Q + in + (P' $ Q',epss'') + end + | rm_Eps_cls_aux epss t = (t,epss); + + +fun rm_Eps_cls epss thm = + let val tm = prop_of thm + in + rm_Eps_cls_aux epss tm + end; + + + +fun rm_Eps _ [] = [] + | rm_Eps epss (thm::thms) = + let val (thm',epss') = rm_Eps_cls epss thm + in + thm' :: (rm_Eps epss' thms) + end; + + + +(* changed, now it also finds out the name of the theorem. *) +fun clausify_axiom thm = + let val isa_clauses = cnf_axiom thm (*"isa_clauses" are already "standard"ed. *) + val isa_clauses' = rm_Eps [] isa_clauses + val thm_name = Thm.name_of_thm thm + val clauses_n = length isa_clauses + fun make_axiom_clauses _ [] = [] + | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss + in + make_axiom_clauses 0 isa_clauses' + + end; + + +(******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******) + + +local + +fun retr_thms ([]:MetaSimplifier.rrule list) = [] + | retr_thms (r::rs) = (#thm r)::(retr_thms rs); + + +fun snds [] = [] + | snds ((x,y)::l) = y::(snds l); + +in + + +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 + safeEs @ safeIs @ hazEs @ hazIs + end; + +fun simpset_rules_of_thy thy = + let val simpset = simpset_of thy + val rules = #rules(fst (rep_ss simpset)) + val thms = retr_thms (snds(Net.dest rules)) + in + thms + end; + +end; + + +(**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****) + +(* classical rules *) +fun cnf_classical_rules [] err_list = ([],err_list) + | cnf_classical_rules (thm::thms) err_list = + let val (ts,es) = cnf_classical_rules thms err_list + in + ((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es)) + end; + + +(* CNF all rules from a given theory's classical reasoner *) +fun cnf_classical_rules_thy thy = + let val rules = claset_rules_of_thy thy + in + cnf_classical_rules rules [] + end; + + +(* simplifier rules *) +fun cnf_simpset_rules [] err_list = ([],err_list) + | cnf_simpset_rules (thm::thms) err_list = + let val (ts,es) = cnf_simpset_rules thms err_list + in + ((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es)) + end; + + +(* CNF all simplifier rules from a given theory's simpset *) +fun cnf_simpset_rules_thy thy = + let val thms = simpset_rules_of_thy thy + in + cnf_simpset_rules thms [] + end; + + + +(**** Convert all theorems of a classical reason/simpset into clauses (ResClause.clause) ****) + +(* classical rules *) +fun clausify_classical_rules [] err_list = ([],err_list) + | clausify_classical_rules (thm::thms) err_list = + let val (ts,es) = clausify_classical_rules thms err_list + in + ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es)) + end; + +fun clausify_classical_rules_thy thy = + let val rules = claset_rules_of_thy thy + in + clausify_classical_rules rules [] + end; + + +(* simplifier rules *) +fun clausify_simpset_rules [] err_list = ([],err_list) + | clausify_simpset_rules (thm::thms) err_list = + let val (ts,es) = clausify_simpset_rules thms err_list + in + ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es)) + end; + + +fun clausify_simpset_rules_thy thy = + let val thms = simpset_rules_of_thy thy + in + clausify_simpset_rules thms [] + end; + + + + +end; diff -r ac272926fb77 -r 14585bc8fa09 src/HOL/Tools/res_clause.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/res_clause.ML Tue Nov 30 18:25:55 2004 +0100 @@ -0,0 +1,675 @@ +(* Author: Jia Meng, Cambridge University Computer Laboratory + ID: $Id$ + Copyright 2004 University of Cambridge + +ML data structure for storing/printing FOL clauses and arity clauses. +Typed equality is treated differently. +*) + +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 keep_types : bool ref + val make_axiom_arity_clause : + string * (string * string list list) -> arityClause + val make_axiom_classrelClause : + string * string Library.option -> classrelClause + val make_axiom_clause : Term.term -> string * int -> clause + val make_axiom_clause_thm : Thm.thm -> 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 make_hypothesis_clause_thm : Thm.thm -> clause + val special_equal : bool ref + val tptp_arity_clause : arityClause -> string + val tptp_classrelClause : classrelClause -> string + val tptp_clause : clause -> string list + val tptp_clauses2str : string list -> string + val typed : unit -> unit + val untyped : unit -> unit + end; + +structure ResClause : RES_CLAUSE = +struct + +(* Added for typed equality *) +val special_equal = ref false; (* by default,equality does not carry type information *) +val eq_typ_wrapper = "typeinfo"; (* default string *) + + +val schematic_var_prefix = "V_"; +val fixed_var_prefix = "v_"; + + +val tvar_prefix = "Typ_"; +val tfree_prefix = "typ_"; + + +val clause_prefix = "cls_"; + +val arclause_prefix = "arcls_" + +val const_prefix = "const_"; +val tconst_prefix = "tconst_"; + +val class_prefix = "clas_"; + + + +(**** some useful functions ****) + +val const_trans_table = + Symtab.make [("op =", "equal"), + ("op <=", "lessequals"), + ("op <", "less"), + ("op &", "and"), + ("op |", "or"), + ("op -->", "implies"), + ("op :", "in"), + ("op Un", "union"), + ("op Int", "inter")]; + + + +fun ascii_of_c c = + let val n = ord c + in + (if ((n < 48) orelse (n > 57 andalso n < 65) orelse + (n > 90 andalso n < 97) orelse (n > 122)) then ("_asc" ^ string_of_int n ^ "_") + else c) + end; + +fun ascii_of s = implode(map ascii_of_c (explode s)); + + +(* another version of above functions that remove chars that may not be allowed by Vampire *) +fun make_schematic_var v = schematic_var_prefix ^ (ascii_of v); +fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); + +fun make_schematic_type_var v = tvar_prefix ^ (ascii_of v); +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of x); + +fun make_fixed_const c = const_prefix ^ (ascii_of c); +fun make_fixed_type_const c = tconst_prefix ^ (ascii_of c); + +fun make_type_class clas = class_prefix ^ (ascii_of clas); + + + + +fun lookup_const c = + case Symtab.lookup (const_trans_table,c) of + Some c' => c' + | None => make_fixed_const c; + + + +(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****) + +val keep_types = ref true; (* default is true *) +fun untyped () = (keep_types := false); +fun typed () = (keep_types := true); + + +datatype kind = Axiom | Hypothesis | Conjecture; +fun name_of_kind Axiom = "axiom" + | name_of_kind Hypothesis = "hypothesis" + | name_of_kind Conjecture = "conjecture"; + +type clause_id = int; +type axiom_name = string; + + +type polarity = bool; + +type indexname = Term.indexname; + + +(* "tag" is used for vampire specific syntax *) +type tag = bool; + + + +fun string_of_indexname (name,index) = name ^ "_" ^ (string_of_int index); + + +val id_ref = ref 0; +fun generate_id () = + let val id = !id_ref + in + (id_ref:=id + 1; id) + end; + + + +(**** Isabelle FOL clauses ****) + +(* by default it is false *) +val tagged = ref false; + +type pred_name = string; +type sort = Term.sort; +type fol_type = string; + + +datatype type_literal = LTVar of string | LTFree of string; + + +datatype folTerm = UVar of string * fol_type| Fun of string * fol_type * folTerm list; +datatype predicate = Predicate of pred_name * fol_type * folTerm list; + + +datatype literal = Literal of polarity * predicate * tag; + + +datatype typ_var = FOLTVar of indexname | FOLTFree of string; + + +(* ML datatype used to repsent one single clause: disjunction of literals. *) +datatype clause = + Clause of {clause_id: clause_id, + axiom_name: axiom_name, + kind: kind, + literals: literal list, + types_sorts: (typ_var * sort) list, + tvar_type_literals: type_literal list, + tfree_type_literals: type_literal list }; + + +exception CLAUSE of string; + + + +(*** make clauses ***) + + +fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,tfree_type_literals) = + Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, literals = literals, types_sorts = types_sorts,tvar_type_literals = tvar_type_literals,tfree_type_literals = tfree_type_literals}; + + + +fun type_of (Type (a, [])) = (make_fixed_type_const a,[]) + | type_of (Type (a, Ts)) = + let val foltyps_ts = map type_of Ts + val (folTyps,ts) = ResLib.unzip foltyps_ts + val ts' = ResLib.flat_noDup ts + in + (((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)),ts') + end + | type_of (TFree (a, s)) = (make_fixed_type_var a, [((FOLTFree a),s)]) + | type_of (TVar (v, s)) = (make_schematic_type_var (string_of_indexname v), [((FOLTVar v),s)]); + + +fun pred_name_type (Const(c,T)) = (lookup_const c,type_of T) + | pred_name_type (Free(x,T)) = (make_fixed_var x,type_of T) + | pred_name_type (Var(_,_)) = raise CLAUSE("Predicate Not First Order") + | pred_name_type _ = raise CLAUSE("Predicate input unexpected"); + + +fun fun_name_type (Const(c,T)) = (lookup_const c,type_of T) + | fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T) + | fun_name_type _ = raise CLAUSE("Function Not First Order"); + + +fun term_of (Var(ind_nm,T)) = + let val (folType,ts) = type_of T + in + (UVar(make_schematic_var(string_of_indexname ind_nm),folType),ts) + end + | term_of (Free(x,T)) = + let val (folType,ts) = type_of T + in + (Fun(make_fixed_var x,folType,[]),ts) + end + | term_of (Const(c,T)) = + let val (folType,ts) = type_of T + in + (Fun(lookup_const c,folType,[]),ts) + end + | term_of (app as (t $ a)) = + let val (f,args) = strip_comb app + fun term_of_aux () = + let val (funName,(funType,ts1)) = fun_name_type f + val (args',ts2) = ResLib.unzip (map term_of args) + val ts3 = ResLib.flat_noDup (ts1::ts2) + in + (Fun(funName,funType,args'),ts3) + end + in + case f of Const(_,_) => term_of_aux () + | Free(_,_) => term_of_aux () + | _ => raise CLAUSE("Function Not First Order") + end + | term_of _ = raise CLAUSE("Function Not First Order"); + + + + +(* For type equality *) +(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) +(* Find type of equality arg *) +local + +fun eq_arg_type (Type("fun",[T,_])) = + let val (folT,_) = type_of T; + in + folT + end; + +in + +fun pred_of_eq ((Const ("op =", typ)),args) = + let val arg_typ = eq_arg_type typ + val (args',ts) = ResLib.unzip (map term_of args) + val equal_name = lookup_const "op =" + in + (Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts) + end; + +end; + +(* changed for non-equality predicate *) +(* The input "pred" cannot be an equality *) +fun pred_of_nonEq (pred,args) = + let val (predName,(predType,ts1)) = pred_name_type pred + val (args',ts2) = ResLib.unzip (map term_of args) + val ts3 = ResLib.flat_noDup (ts1::ts2) + in + (Predicate(predName,predType,args'),ts3) + 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; + + + +fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts) = literals_of_term(P,lits_ts) + | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts)) = + let val (lits',ts') = literals_of_term(P,(lits,ts)) + in + literals_of_term(Q,(lits',ts')) + end + | literals_of_term ((Const("Not",_) $ P),(lits,ts)) = + let val (pred,ts') = predicate_of P + val lits' = Literal(false,pred,false) :: lits + val ts'' = ResLib.no_rep_app ts ts' + in + (lits',ts'') + end + | literals_of_term (P,(lits,ts)) = + let val (pred,ts') = predicate_of P + val lits' = Literal(true,pred,false) :: lits + val ts'' = ResLib.no_rep_app ts ts' + in + (lits',ts'') + end + | literals_of_term _ = raise CLAUSE("Unexpected clause format"); + + +fun literals_of_thm thm = + let val term_of_thm = prop_of thm + + in + literals_of_term (term_of_thm,([],[])) + end; + + +fun sorts_on_typs (_, []) = [] + | sorts_on_typs ((FOLTVar(indx)), [s]) = [LTVar((make_type_class s) ^ "(" ^ (make_schematic_type_var(string_of_indexname indx)) ^ ")")] + | sorts_on_typs ((FOLTVar(indx)), (s::ss))= LTVar((make_type_class s) ^ "(" ^ (make_schematic_type_var(string_of_indexname indx)) ^ ")") :: (sorts_on_typs ((FOLTVar(indx)), ss)) + | sorts_on_typs ((FOLTFree(x)), [s]) = [LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")")] + | sorts_on_typs ((FOLTFree(x)), (s::ss)) = LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: (sorts_on_typs ((FOLTFree(x)), ss)); + + +fun add_typs_aux [] = ([],[]) + | add_typs_aux ((FOLTVar(indx),s)::tss) = + let val vs = sorts_on_typs (FOLTVar(indx),s) + val (vss,fss) = add_typs_aux tss + in + (ResLib.no_rep_app vs vss,fss) + end + | add_typs_aux ((FOLTFree(x),s)::tss) = + let val fs = sorts_on_typs (FOLTFree(x),s) + val (vss,fss) = add_typs_aux tss + in + (vss,ResLib.no_rep_app fs fss) + end; + + +fun add_typs (Clause cls) = + let val ts = #types_sorts cls + in + add_typs_aux ts + end; + + + + +(** make axiom clauses, hypothesis clauses and conjecture clauses. **) + +local + fun replace_dot "." = "_" + | replace_dot c = c; + +in + +fun proper_ax_name ax_name = + let val chars = explode ax_name + in + implode (map replace_dot chars) + end; +end; + +fun make_axiom_clause_thm thm (name,number)= + let val (lits,types_sorts) = literals_of_thm thm + val cls_id = number + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + val ax_name = proper_ax_name name + in + make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits) + end; + +fun make_hypothesis_clause_thm thm = + let val (lits,types_sorts) = literals_of_thm thm + val cls_id = generate_id() + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + in + make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits) + end; + + +fun make_conjecture_clause_thm thm = + let val (lits,types_sorts) = literals_of_thm thm + val cls_id = generate_id() + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + in + make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits) + end; + + +fun make_axiom_clause term (name,number)= + let val (lits,types_sorts) = literals_of_term (term,([],[])) + val cls_id = number + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + val ax_name = proper_ax_name name + in + make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits) + end; + + +fun make_hypothesis_clause term = + let val (lits,types_sorts) = literals_of_term (term,([],[])) + val cls_id = generate_id() + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + in + make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits) + end; + + +fun make_conjecture_clause term = + let val (lits,types_sorts) = literals_of_term (term,([],[])) + val cls_id = generate_id() + val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + in + make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits) + end; + + + +(**** Isabelle arities ****) + +exception ARCLAUSE of string; + + +type class = string; +type tcons = string; + + +datatype arLit = TConsLit of bool * (class * tcons * string list) | TVarLit of bool * (class * string); + +datatype arityClause = + ArityClause of {clause_id: clause_id, + kind: kind, + conclLit: arLit, + premLits: arLit list}; + + +fun get_TVars 0 = [] + | get_TVars n = ("T_" ^ (string_of_int n)) :: get_TVars (n-1); + + + +fun pack_sort(_,[]) = raise ARCLAUSE("Empty Sort Found") + | pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] + | pack_sort(tvar, cls::srt) = (make_type_class cls,tvar) :: (pack_sort(tvar, srt)); + + +fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str)); +fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars)); + + +fun make_arity_clause (clause_id,kind,conclLit,premLits) = + ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits}; + + +fun make_axiom_arity_clause (tcons,(res,args)) = + let val cls_id = generate_id() + val nargs = length args + val tvars = get_TVars nargs + val conclLit = make_TConsLit(true,(res,tcons,tvars)) + val tvars_srts = ResLib.zip tvars args + val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts) + val false_tvars_srts' = ResLib.pair_ins false tvars_srts' + val premLits = map make_TVarLit false_tvars_srts' + in + make_arity_clause (cls_id,Axiom,conclLit,premLits) + end; + + + +(**** Isabelle class relations ****) + + +datatype classrelClause = + ClassrelClause of {clause_id: clause_id, + subclass: class, + superclass: class Library.option}; + +fun make_classrelClause (clause_id,subclass,superclass) = + ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass}; + + +fun make_axiom_classrelClause (subclass,superclass) = + let val cls_id = generate_id() + val sub = make_type_class subclass + val sup = case superclass of None => None + | Some s => Some (make_type_class s) + in + make_classrelClause(cls_id,sub,sup) + end; + + + +fun classrelClauses_of_aux (sub,[]) = [] + | classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,Some sup) :: (classrelClauses_of_aux (sub,sups)); + + +fun classrelClauses_of (sub,sups) = + case sups of [] => [make_axiom_classrelClause (sub,None)] + | _ => classrelClauses_of_aux (sub, sups); + + + +(***** convert clauses to tptp format *****) + + +fun string_of_clauseID (Clause cls) = clause_prefix ^ (string_of_int (#clause_id cls)); + + +fun string_of_kind (Clause cls) = name_of_kind (#kind cls); + +fun string_of_axiomName (Clause cls) = #axiom_name cls; + +fun string_of_term (UVar(x,_)) = x + | string_of_term (Fun (name,typ,[])) = name + | string_of_term (Fun (name,typ,terms)) = + let val terms' = map string_of_term terms + in + if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms')) + else name ^ (ResLib.list_to_string terms') + end; + + + +(****!!!! Changed for typed equality !!!!****) +fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; + + +(****!!!! Changed for typed equality !!!!****) +(* Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed && if we specifically ask for types to be included. *) +fun string_of_equality (typ,terms) = + let val [tstr1,tstr2] = map string_of_term terms + in + if ((!keep_types) andalso (!special_equal)) then + "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ (wrap_eq_type typ tstr2) ^ ")" + else + "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" + end; + + + +(* Changed for typed equality *) +(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) +fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms) + | string_of_predicate (Predicate(name,_,[])) = name + | string_of_predicate (Predicate(name,typ,terms)) = + let val terms_as_strings = map string_of_term terms + in + if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms_as_strings)) + else name ^ (ResLib.list_to_string terms_as_strings) + end; + + + + +fun tptp_literal (Literal(pol,pred,tag)) = + 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_of_typeLit (LTVar x) = "--" ^ x + | tptp_of_typeLit (LTFree x) = "++" ^ x; + + +fun gen_tptp_cls (cls_id,ax_name,knd,lits) = + let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name)) + in + "input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")." + end; + + +fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "])."; + + +fun tptp_clause_aux (Clause cls) = + let val lits = map tptp_literal (#literals cls) + val tvar_lits_strs = if (!keep_types) then (map tptp_of_typeLit (#tvar_type_literals cls)) else [] + val tfree_lits = if (!keep_types) then (map tptp_of_typeLit (#tfree_type_literals cls)) else [] + in + (tvar_lits_strs @ lits,tfree_lits) + end; + + +fun tptp_clause cls = + let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*) + val cls_id = string_of_clauseID cls + val ax_name = string_of_axiomName cls + val knd = string_of_kind cls + val lits_str = ResLib.list_to_string' lits + val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) fun typ_clss k [] = [] + | typ_clss k (tfree :: tfrees) = + (gen_tptp_type_cls(cls_id,knd,tfree,k)) :: (typ_clss (k+1) tfrees) + in + cls_str :: (typ_clss 0 tfree_lits) + end; + + +val delim = "\n"; +val tptp_clauses2str = ResLib.list2str_sep delim; + + +fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls); + + +fun string_of_arLit (TConsLit(b,(c,t,args))) = + let val pol = if b then "++" else "--" + val arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args) + in + pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" + end + | string_of_arLit (TVarLit(b,(c,str))) = + let val pol = if b then "++" else "--" + in + pol ^ c ^ "(" ^ str ^ ")" + end; + + +fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls); + + +fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls); + + +fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls); + +fun tptp_arity_clause arcls = + let val arcls_id = string_of_arClauseID arcls + val concl_lit = string_of_conclLit arcls + val prems_lits = strings_of_premLits arcls + val knd = string_of_arKind arcls + val all_lits = concl_lit :: prems_lits + in + "input_clause(" ^ arcls_id ^ "," ^ knd ^ (ResLib.list_to_string' all_lits) ^ ")." + + end; + + +val clrelclause_prefix = "relcls_"; + + +fun tptp_classrelLits sub sup = + let val tvar = "(T)" + in + case sup of None => "[++" ^ sub ^ tvar ^ "]" + | (Some supcls) => "[++" ^ sub ^ tvar ^ ",--" ^ supcls ^ tvar ^ "]" + end; + + +fun tptp_classrelClause (ClassrelClause cls) = + let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls) + val sub = #subclass cls + val sup = #superclass cls + val lits = tptp_classrelLits sub sup + in + "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." + end; + +end; diff -r ac272926fb77 -r 14585bc8fa09 src/HOL/Tools/res_lib.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/res_lib.ML Tue Nov 30 18:25:55 2004 +0100 @@ -0,0 +1,124 @@ +(* Author: Jia Meng, Cambridge University Computer Laboratory + ID: $Id$ + Copyright 2004 University of Cambridge + +some frequently used functions by files in this directory. +*) + +signature RES_LIB = +sig + +val flat_noDup : ''a list list -> ''a list +val list2str_sep : string -> string list -> string +val list_to_string : string list -> string +val list_to_string' : string list -> string +val no_BDD : string -> string +val no_blanks : string -> string +val no_blanks_dots : string -> string +val no_blanks_dots_dashes : string -> string +val no_dots : string -> string +val no_rep_add : ''a -> ''a list -> ''a list +val no_rep_app : ''a list -> ''a list -> ''a list +val pair_ins : 'a -> 'b list -> ('a * 'b) list +val rm_rep : ''a list -> ''a list +val unzip : ('a * 'b) list -> 'a list * 'b list +val write_strs : TextIO.outstream -> TextIO.vector list -> unit +val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit +val zip : 'a list -> 'b list -> ('a * 'b) list + + +end; + + + +structure ResLib : RES_LIB = + +struct + +(*** convert a list of strings into one single string; surrounded by backets ***) +fun list_to_string strings = + let fun str_of [s] = s + | str_of (s1::ss) = s1 ^ "," ^ (str_of ss) + | str_of _ = "" + in + "(" ^ str_of strings ^ ")" + end; + +fun list_to_string' strings = + let fun str_of [s] = s + | str_of (s1::ss) = s1 ^ "," ^ (str_of ss) + | str_of _ = "" + in + "[" ^ str_of strings ^ "]" + end; + + + +(*** remove some chars (not allowed by TPTP format) from a string ***) +fun no_blanks " " = "_" + | no_blanks c = c; + + +fun no_dots "." = "_dot_" + | no_dots c = c; + + +fun no_blanks_dots " " = "_" + | no_blanks_dots "." = "_dot_" + | no_blanks_dots c = c; + +fun no_blanks_dots_dashes " " = "_" + | no_blanks_dots_dashes "." = "_dot_" + | no_blanks_dots_dashes "'" = "_da_" + | no_blanks_dots_dashes c = c; + +fun no_BDD cs = implode (map no_blanks_dots_dashes (explode cs)); + + + +fun no_rep_add x [] = [x] + | no_rep_add x (y :: z) = if (x = y) then (y :: z) + else y :: (no_rep_add x z); + + +fun no_rep_app l1 [] = l1 + | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y; + + +fun rm_rep [] = [] + | rm_rep (x::y) = if (x mem y) then rm_rep y else x::(rm_rep y); + + +fun unzip [] = ([],[]) + | unzip ((x1,y1)::zs) = + let val (xs,ys) = unzip zs + in + (x1::xs,y1::ys) + end; + +fun zip [] [] = [] + | zip(x::xs) (y::ys) = (x,y)::(zip xs ys); + + +fun flat_noDup [] = [] + | flat_noDup (x::y) = no_rep_app x (flat_noDup y); + + + +fun list2str_sep delim [] = delim + | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss); + + + +fun write_strs _ [] = () + | write_strs out (s::ss) = (TextIO.output(out,s);write_strs out ss); + +fun writeln_strs _ [] = () + | writeln_strs out (s::ss) = (TextIO.output(out,s);TextIO.output(out,"\n");writeln_strs out ss); + +(* pair the first argument with each of the element in the second input list *) +fun pair_ins x [] = [] + | pair_ins x (y::ys) = (x,y) :: (pair_ins x ys); + + +end; \ No newline at end of file diff -r ac272926fb77 -r 14585bc8fa09 src/HOL/Tools/res_skolem_function.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/res_skolem_function.ML Tue Nov 30 18:25:55 2004 +0100 @@ -0,0 +1,56 @@ +(* Author: Jia Meng, Cambridge University Computer Laboratory + ID: $Id$ + Copyright 2004 University of Cambridge + +Generation of unique Skolem functions (with types) as Term.term. +*) + +signature RES_SKOLEM_FUNCTION = +sig + +val gen_skolem: Term.term list -> Term.typ -> Term.term + +end; + +structure ResSkolemFunction: RES_SKOLEM_FUNCTION = + +struct + +val skolem_prefix = "sk_"; + +(* internal reference starting from 0. *) +val skolem_id = ref 0; + + +fun gen_skolem_name () = + let val new_id = !skolem_id + val sk_fun = skolem_prefix ^ (string_of_int new_id) + in + (skolem_id := new_id + 1; sk_fun) (* increment id by 1. *) + end; + +fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp]) + | sk_type_of_aux (Var(_,tp1)::vars) tp = + let val tp' = sk_type_of_aux vars tp + in + Type("fun",[tp1,tp']) + end; + + +fun sk_type_of [] tp = tp + | sk_type_of vars tp = sk_type_of_aux vars tp; + + + +fun gen_skolem univ_vars tp = + let val new_sk_name = gen_skolem_name () + val new_sk_type = sk_type_of univ_vars tp + val skolem_term = Const(new_sk_name,new_sk_type) + fun app [] sf = sf + | app (var::vars) sf= app vars (sf $ var) + in + app univ_vars skolem_term + end; + + +end; \ No newline at end of file diff -r ac272926fb77 -r 14585bc8fa09 src/HOL/Tools/res_types_sorts.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/res_types_sorts.ML Tue Nov 30 18:25:55 2004 +0100 @@ -0,0 +1,132 @@ +(* Author: Jia Meng, Cambridge University Computer Laboratory + ID: $Id$ + Copyright 2004 University of Cambridge + +transformation of Isabelle arities and class relations into clauses (defined in the structure Clause). +*) + +signature RES_TYPES_SORTS = +sig + +exception ARITIES of string +val arity_clause : + string * (string * string list list) list -> ResClause.arityClause list +val arity_clause_sig : + Sign.sg -> ResClause.arityClause list list * (string * 'a list) list +val arity_clause_thy : + Theory.theory -> + ResClause.arityClause list list * (string * 'a list) list +type classrelClauses +val classrel_clause : string * string list -> ResClause.classrelClause list +val classrel_clauses_classrel : + 'a Graph.T -> ResClause.classrelClause list list +val classrel_clauses_sg : Sign.sg -> ResClause.classrelClause list list +val classrel_clauses_thy : + Theory.theory -> ResClause.classrelClause list list +val classrel_of_sg : Sign.sg -> Sorts.classes +val multi_arity_clause : + (string * (string * string list list) list) list -> + (string * 'a list) list -> + ResClause.arityClause list list * (string * 'a list) list +val tptp_arity_clause_thy : Theory.theory -> string list list +val tptp_classrel_clauses_sg : Sign.sg -> string list list +val tsig_of : Theory.theory -> Type.tsig +val tsig_of_sg : Sign.sg -> Type.tsig + +end; + +structure ResTypesSorts : RES_TYPES_SORTS = + +struct + +(**** Isabelle arities ****) + +exception ARITIES of string; + + +fun arity_clause (tcons, []) = raise ARITIES(tcons) + | arity_clause (tcons,[ar]) = [ResClause.make_axiom_arity_clause (tcons,ar)] + | arity_clause (tcons,ar1::ars) = (ResClause.make_axiom_arity_clause (tcons,ar1)) :: (arity_clause (tcons,ars)); + + +fun multi_arity_clause [] expts = ([], expts) + | multi_arity_clause ((tcon,[])::tcons_ars) expts = + multi_arity_clause tcons_ars ((tcon,[])::expts) + | multi_arity_clause (tcon_ar::tcons_ars) expts = + let val result = multi_arity_clause tcons_ars expts + in + (((arity_clause tcon_ar) :: (fst result)),snd result) + end; + + +fun tsig_of thy = #tsig(Sign.rep_sg (sign_of thy)); + +fun tsig_of_sg sg = #tsig(Sign.rep_sg sg); + + +(* Isabelle arities *) +fun arity_clause_thy thy = + let val tsig = tsig_of thy + val arities = #arities (Type.rep_tsig tsig) + val entries = Symtab.dest arities + in + multi_arity_clause entries [] + end; + +fun arity_clause_sig sg = + let val tsig = #tsig(Sign.rep_sg sg) + val arities = #arities (Type.rep_tsig tsig) + val entries = Symtab.dest arities + in + multi_arity_clause entries [] + end; + + +fun tptp_arity_clause_thy thy = + let val (arclss,_) = arity_clause_thy thy + in + map (map ResClause.tptp_arity_clause) arclss + end; + + + +(**** Isabelle classrel ****) + +type classrelClauses = (ResClause.classrelClause list) Symtab.table; + + + +(* The new version of finding class relations from a signature *) +fun classrel_of_sg sg = #classes (Type.rep_tsig (tsig_of_sg sg)); + +fun classrel_clause (sub, sups) = ResClause.classrelClauses_of (sub,sups); + + + +(* new version of classrel_clauses_classrel *) +fun classrel_clauses_classrel classrel = + let val entries = Graph.dest classrel + in + map classrel_clause entries + end; + +fun classrel_clauses_sg sg = + let val classrel = classrel_of_sg sg + in + classrel_clauses_classrel classrel + end; + + +val classrel_clauses_thy = classrel_clauses_sg o sign_of; + + +fun tptp_classrel_clauses_sg sg = + let val relclss = classrel_clauses_sg sg + in + map (map ResClause.tptp_classrelClause) relclss + end; + + + + +end;