1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu May 12 15:42:58 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu May 12 18:24:42 2005 +0200
1.3 @@ -11,8 +11,6 @@
1.4 structure ResClasimp : RES_CLASIMP =
1.5 struct
1.6
1.7 -fun has_name th = not((Thm.name_of_thm th)= "")
1.8 -
1.9 fun has_name_pair (a,b) = not_equal a "";
1.10
1.11 fun stick [] = []
1.12 @@ -21,10 +19,10 @@
1.13 (* changed, now it also finds out the name of the theorem. *)
1.14 (* convert a theorem into CNF and then into Clause.clause format. *)
1.15 fun clausify_axiom_pairs thm =
1.16 - let val isa_clauses = ResAxioms.cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
1.17 + let val thm_name = Thm.name_of_thm thm
1.18 + val isa_clauses = ResAxioms.cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
1.19 val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
1.20 - val thm_name = Thm.name_of_thm thm
1.21 - val clauses_n = length isa_clauses
1.22 + val clauses_n = length isa_clauses
1.23 fun make_axiom_clauses _ [] []= []
1.24 | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
1.25 in
1.26 @@ -39,9 +37,14 @@
1.27 ((clausify_axiom_pairs thm)::ts,es) handle _ => (ts,(thm::es))
1.28 end;
1.29
1.30 +
1.31 +(*Insert th into the result provided the name is not "".*)
1.32 +fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
1.33 +
1.34 +
1.35 fun write_out_clasimp filename = let
1.36 val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
1.37 - val named_claset = List.filter has_name claset_rules;
1.38 + val named_claset = List.foldr add_nonempty [] claset_rules;
1.39 val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
1.40
1.41 val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
2.1 --- a/src/HOL/Tools/res_axioms.ML Thu May 12 15:42:58 2005 +0200
2.2 +++ b/src/HOL/Tools/res_axioms.ML Thu May 12 18:24:42 2005 +0200
2.3 @@ -11,9 +11,9 @@
2.4 sig
2.5
2.6 exception ELIMR2FOL of string
2.7 -val elimRule_tac : Thm.thm -> Tactical.tactic
2.8 -val elimR2Fol : Thm.thm -> Term.term
2.9 -val transform_elim : Thm.thm -> Thm.thm
2.10 +val elimRule_tac : thm -> Tactical.tactic
2.11 +val elimR2Fol : thm -> Term.term
2.12 +val transform_elim : thm -> thm
2.13
2.14 end;
2.15
2.16 @@ -37,31 +37,18 @@
2.17
2.18 (* functions used to construct a formula *)
2.19
2.20 -fun make_imp (prem,concl) = Const("op -->", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ prem $ concl;
2.21 -
2.22 -
2.23 fun make_disjs [x] = x
2.24 - | make_disjs (x :: xs) = Const("op |",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_disjs xs)
2.25 -
2.26 + | make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs)
2.27
2.28 fun make_conjs [x] = x
2.29 - | make_conjs (x :: xs) = Const("op &", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_conjs xs)
2.30 + | make_conjs (x :: xs) = HOLogic.mk_conj(x, make_conjs xs)
2.31
2.32 +fun add_EX tm [] = tm
2.33 + | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
2.34
2.35 -fun add_EX term [] = term
2.36 - | add_EX term ((x,xtp)::xs) = add_EX (Const ("Ex",Type("fun",[Type("fun",[xtp,Type("bool",[])]),Type("bool",[])])) $ Abs (x,xtp,term)) xs;
2.37
2.38
2.39 -exception TRUEPROP of string;
2.40 -
2.41 -fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P
2.42 - | strip_trueprop _ = raise TRUEPROP("not a prop!");
2.43 -
2.44 -
2.45 -fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P;
2.46 -
2.47 -
2.48 -fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_))= (p = q)
2.49 +fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q)
2.50 | is_neg _ _ = false;
2.51
2.52
2.53 @@ -69,23 +56,23 @@
2.54
2.55
2.56 fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
2.57 - let val P' = strip_trueprop P
2.58 - val prems' = P'::prems
2.59 - in
2.60 + let val P' = HOLogic.dest_Trueprop P
2.61 + val prems' = P'::prems
2.62 + in
2.63 strip_concl' prems' bvs Q
2.64 - end
2.65 + end
2.66 | strip_concl' prems bvs P =
2.67 - let val P' = neg (strip_trueprop P)
2.68 - in
2.69 + let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
2.70 + in
2.71 add_EX (make_conjs (P'::prems)) bvs
2.72 - end;
2.73 + end;
2.74
2.75
2.76 fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = strip_concl prems ((x,xtp)::bvs) concl body
2.77 | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
2.78 if (is_neg P concl) then (strip_concl' prems bvs Q)
2.79 else
2.80 - (let val P' = strip_trueprop P
2.81 + (let val P' = HOLogic.dest_Trueprop P
2.82 val prems' = P'::prems
2.83 in
2.84 strip_concl prems' bvs concl Q
2.85 @@ -98,7 +85,7 @@
2.86 let val others' = map (strip_concl [] [] concl) others
2.87 val disjs = make_disjs others'
2.88 in
2.89 - make_imp(strip_trueprop main,disjs)
2.90 + HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs)
2.91 end;
2.92
2.93
2.94 @@ -107,21 +94,19 @@
2.95 let val nprems = length prems
2.96 val main = hd prems
2.97 in
2.98 - if (nprems = 1) then neg (strip_trueprop main)
2.99 + if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main)
2.100 else trans_elim (main, tl prems, concl)
2.101 end;
2.102
2.103 -
2.104 -fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term;
2.105 -
2.106 +
2.107 (* convert an elim rule into an equivalent formula, of type Term.term. *)
2.108 fun elimR2Fol elimR =
2.109 let val elimR' = Drule.freeze_all elimR
2.110 val (prems,concl) = (prems_of elimR', concl_of elimR')
2.111 in
2.112 case concl of Const("Trueprop",_) $ Free(_,Type("bool",[]))
2.113 - => trueprop (elimR2Fol_aux prems concl)
2.114 - | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems concl)
2.115 + => HOLogic.mk_Trueprop (elimR2Fol_aux prems concl)
2.116 + | Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl)
2.117 | _ => raise ELIMR2FOL("Not an elimination rule!")
2.118 end;
2.119
2.120 @@ -145,23 +130,20 @@
2.121 signature RES_AXIOMS =
2.122 sig
2.123
2.124 -val clausify_axiom : Thm.thm -> ResClause.clause list
2.125 -val cnf_axiom : Thm.thm -> Thm.thm list
2.126 -val meta_cnf_axiom : Thm.thm -> Thm.thm list
2.127 -val cnf_elim : Thm.thm -> Thm.thm list
2.128 -val cnf_rule : Thm.thm -> Thm.thm list
2.129 -val cnf_classical_rules_thy : Theory.theory -> Thm.thm list list * Thm.thm list
2.130 -val clausify_classical_rules_thy
2.131 -: Theory.theory -> ResClause.clause list list * Thm.thm list
2.132 -val cnf_simpset_rules_thy
2.133 -: Theory.theory -> Thm.thm list list * Thm.thm list
2.134 -val clausify_simpset_rules_thy
2.135 -: Theory.theory -> ResClause.clause list list * Thm.thm list
2.136 +val clausify_axiom : thm -> ResClause.clause list
2.137 +val cnf_axiom : (string * thm) -> thm list
2.138 +val meta_cnf_axiom : thm -> thm list
2.139 +val cnf_elim : thm -> thm list
2.140 +val cnf_rule : thm -> thm list
2.141 +val cnf_classical_rules_thy : theory -> thm list list * thm list
2.142 +val clausify_classical_rules_thy : theory -> ResClause.clause list list * thm list
2.143 +val cnf_simpset_rules_thy : theory -> thm list list * thm list
2.144 +val clausify_simpset_rules_thy : theory -> ResClause.clause list list * thm list
2.145 val rm_Eps
2.146 -: (Term.term * Term.term) list -> Thm.thm list -> Term.term list
2.147 -val claset_rules_of_thy : Theory.theory -> Thm.thm list
2.148 -val simpset_rules_of_thy : Theory.theory -> (string * Thm.thm) list
2.149 -val clausify_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
2.150 +: (Term.term * Term.term) list -> thm list -> Term.term list
2.151 +val claset_rules_of_thy : theory -> (string * thm) list
2.152 +val simpset_rules_of_thy : theory -> (string * thm) list
2.153 +val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list
2.154
2.155 end;
2.156
2.157 @@ -230,8 +212,8 @@
2.158 (*Cache for clauses: could be a hash table if we provided them.*)
2.159 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
2.160
2.161 -fun cnf_axiom th =
2.162 - case Thm.name_of_thm th of
2.163 +fun cnf_axiom (name,th) =
2.164 + case name of
2.165 "" => cnf_axiom_aux th (*no name, so can't cache*)
2.166 | s => case Symtab.lookup (!clause_cache,s) of
2.167 NONE =>
2.168 @@ -245,23 +227,23 @@
2.169 in clause_cache := Symtab.update ((s, (th,cls)), !clause_cache); cls
2.170 end;
2.171
2.172 -fun meta_cnf_axiom thm =
2.173 - map Meson.make_meta_clause (cnf_axiom thm);
2.174 +fun pairname th = (Thm.name_of_thm th, th);
2.175 +
2.176 +fun meta_cnf_axiom th =
2.177 + map Meson.make_meta_clause (cnf_axiom (pairname th));
2.178
2.179
2.180 (* changed: with one extra case added *)
2.181 -fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars
2.182 - | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars (* EX x. body *)
2.183 +fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars =
2.184 + univ_vars_of_aux body vars
2.185 + | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars =
2.186 + univ_vars_of_aux body vars (* EX x. body *)
2.187 | univ_vars_of_aux (P $ Q) vars =
2.188 - let val vars' = univ_vars_of_aux P vars
2.189 - in
2.190 - univ_vars_of_aux Q vars'
2.191 - end
2.192 + univ_vars_of_aux Q (univ_vars_of_aux P vars)
2.193 | univ_vars_of_aux (t as Var(_,_)) vars =
2.194 - if (t mem vars) then vars else (t::vars)
2.195 + if (t mem vars) then vars else (t::vars)
2.196 | univ_vars_of_aux _ vars = vars;
2.197
2.198 -
2.199 fun univ_vars_of t = univ_vars_of_aux t [];
2.200
2.201
2.202 @@ -280,11 +262,8 @@
2.203
2.204 (* get the proper skolem term to replace epsilon term *)
2.205 fun get_skolem epss t =
2.206 - let val sk_fun = sk_lookup epss t
2.207 - in
2.208 - case sk_fun of NONE => get_new_skolem epss t
2.209 - | SOME sk => (sk,epss)
2.210 - end;
2.211 + case (sk_lookup epss t) of NONE => get_new_skolem epss t
2.212 + | SOME sk => (sk,epss);
2.213
2.214
2.215 fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t
2.216 @@ -297,32 +276,27 @@
2.217 | rm_Eps_cls_aux epss t = (t,epss);
2.218
2.219
2.220 -fun rm_Eps_cls epss thm =
2.221 - let val tm = prop_of thm
2.222 - in
2.223 - rm_Eps_cls_aux epss tm
2.224 - end;
2.225 +fun rm_Eps_cls epss thm = rm_Eps_cls_aux epss (prop_of thm);
2.226
2.227
2.228 (* remove the epsilon terms in a formula, by skolem terms. *)
2.229 fun rm_Eps _ [] = []
2.230 | rm_Eps epss (thm::thms) =
2.231 - let val (thm',epss') = rm_Eps_cls epss thm
2.232 - in
2.233 + let val (thm',epss') = rm_Eps_cls epss thm
2.234 + in
2.235 thm' :: (rm_Eps epss' thms)
2.236 - end;
2.237 + end;
2.238
2.239
2.240 -
2.241 -(* changed, now it also finds out the name of the theorem. *)
2.242 (* convert a theorem into CNF and then into Clause.clause format. *)
2.243 fun clausify_axiom thm =
2.244 - let val isa_clauses = cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
2.245 + let val name = Thm.name_of_thm thm
2.246 + val isa_clauses = cnf_axiom (name, thm)
2.247 + (*"isa_clauses" are already "standard"ed. *)
2.248 val isa_clauses' = rm_Eps [] isa_clauses
2.249 - val thm_name = Thm.name_of_thm thm
2.250 - val clauses_n = length isa_clauses
2.251 + val clauses_n = length isa_clauses
2.252 fun make_axiom_clauses _ [] = []
2.253 - | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss
2.254 + | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (name,i)) :: make_axiom_clauses (i+1) clss
2.255 in
2.256 make_axiom_clauses 0 isa_clauses'
2.257 end;
2.258 @@ -337,7 +311,7 @@
2.259 val hazEs = #hazEs clsset
2.260 val hazIs = #hazIs clsset
2.261 in
2.262 - safeEs @ safeIs @ hazEs @ hazIs
2.263 + map pairname (safeEs @ safeIs @ hazEs @ hazIs)
2.264 end;
2.265
2.266 fun simpset_rules_of_thy thy =
2.267 @@ -351,10 +325,9 @@
2.268
2.269 (* classical rules *)
2.270 fun cnf_rules [] err_list = ([],err_list)
2.271 - | cnf_rules (thm::thms) err_list =
2.272 + | cnf_rules ((name,thm) :: thms) err_list =
2.273 let val (ts,es) = cnf_rules thms err_list
2.274 - in (cnf_axiom thm :: ts,es) handle _ => (ts,(thm::es)) end;
2.275 -
2.276 + in (cnf_axiom (name,thm) :: ts,es) handle _ => (ts, (thm::es)) end;
2.277
2.278 (* CNF all rules from a given theory's classical reasoner *)
2.279 fun cnf_classical_rules_thy thy =
2.280 @@ -362,7 +335,7 @@
2.281
2.282 (* CNF all simplifier rules from a given theory's simpset *)
2.283 fun cnf_simpset_rules_thy thy =
2.284 - cnf_rules (map #2 (simpset_rules_of_thy thy)) [];
2.285 + cnf_rules (simpset_rules_of_thy thy) [];
2.286
2.287
2.288 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
2.289 @@ -378,7 +351,7 @@
2.290
2.291 (* convert all classical rules from a given theory into Clause.clause format. *)
2.292 fun clausify_classical_rules_thy thy =
2.293 - clausify_rules (claset_rules_of_thy thy) [];
2.294 + clausify_rules (map #2 (claset_rules_of_thy thy)) [];
2.295
2.296 (* convert all simplifier rules from a given theory into Clause.clause format. *)
2.297 fun clausify_simpset_rules_thy thy =
3.1 --- a/src/HOL/Tools/res_clause.ML Thu May 12 15:42:58 2005 +0200
3.2 +++ b/src/HOL/Tools/res_clause.ML Thu May 12 18:24:42 2005 +0200
3.3 @@ -352,16 +352,10 @@
3.4 val ts'' = ResLib.no_rep_app ts ts'
3.5 in
3.6 (lits',ts'')
3.7 - end
3.8 - | literals_of_term _ = raise CLAUSE("Unexpected clause format");
3.9 + end;
3.10
3.11
3.12 -fun literals_of_thm thm =
3.13 - let val term_of_thm = prop_of thm
3.14 -
3.15 - in
3.16 - literals_of_term (term_of_thm,([],[]))
3.17 - end;
3.18 +fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]));
3.19
3.20
3.21 fun sorts_on_typs (_, []) = []