1.1 --- a/src/HOL/Main.thy Thu Apr 28 17:08:08 2005 +0200
1.2 +++ b/src/HOL/Main.thy Thu Apr 28 17:56:58 2005 +0200
1.3 @@ -6,7 +6,7 @@
1.4 header {* Main HOL *}
1.5
1.6 theory Main
1.7 - imports Extraction Refute Reconstruction
1.8 + imports Refute Reconstruction
1.9
1.10 begin
1.11
2.1 --- a/src/HOL/Reconstruction.thy Thu Apr 28 17:08:08 2005 +0200
2.2 +++ b/src/HOL/Reconstruction.thy Thu Apr 28 17:56:58 2005 +0200
2.3 @@ -7,7 +7,7 @@
2.4 header{*Attributes for Reconstructing External Resolution Proofs*}
2.5
2.6 theory Reconstruction
2.7 - imports Hilbert_Choice Map Infinite_Set
2.8 + imports Hilbert_Choice Map Infinite_Set Extraction
2.9 files "Tools/res_lib.ML"
2.10 "Tools/res_clause.ML"
2.11 "Tools/res_skolem_function.ML"
3.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 28 17:08:08 2005 +0200
3.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 28 17:56:58 2005 +0200
3.3 @@ -170,9 +170,6 @@
3.4
3.5
3.6
3.7 -fun thm_is_fol (x, thm) = rule_is_fol thm
3.8 -
3.9 -
3.10 fun get_simp_metas [] = [[]]
3.11 | get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
3.12 in
3.13 @@ -208,7 +205,7 @@
3.14
3.15 val names_rules = ListPair.zip (good_names,name_fol_cs);
3.16
3.17 - val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
3.18 + val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
3.19
3.20 val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
3.21
3.22 @@ -251,11 +248,10 @@
3.23 val simp_names = map #1 named_simps;
3.24 val simp_rules = map #2 named_simps;
3.25
3.26 - val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
3.27 + val (simpset_cls,badthms) = ResAxioms.clausify_rules simp_rules [];
3.28 (* 1137 clausif simps *)
3.29 - val clausifiable_simps = remove_all_simps badthms named_simps;
3.30 + val name_fol_simps = remove_all_simps badthms named_simps;
3.31
3.32 - val name_fol_simps = List.filter thm_is_fol clausifiable_simps ;
3.33 val simp_names = map #1 name_fol_simps;
3.34 val simp_rules = map #2 name_fol_simps;
3.35
3.36 @@ -263,7 +259,7 @@
3.37 (* need to get names of claset_cluases so we can make sure we've*)
3.38 (* got the same ones (ie. the named ones ) as the claset rules *)
3.39 (* length 1374*)
3.40 - val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []);
3.41 + val new_simps = #1(ResAxioms.clausify_rules simp_rules []);
3.42 val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
3.43
3.44 val stick_strs = map stick simpset_tptp_strs;
4.1 --- a/src/HOL/Tools/meson.ML Thu Apr 28 17:08:08 2005 +0200
4.2 +++ b/src/HOL/Tools/meson.ML Thu Apr 28 17:56:58 2005 +0200
4.3 @@ -307,7 +307,11 @@
4.4 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
4.5 handle THM _ => th;
4.6
4.7 -fun make_nnf th = make_nnf1 (check_no_bool th);
4.8 +(*The simplification removes occurrences of True and False.*)
4.9 +val nnf_ss = HOL_basic_ss addsimps Ball_def::Bex_def::simp_thms;
4.10 +
4.11 +fun make_nnf th = th |> simplify nnf_ss
4.12 + |> check_no_bool |> make_nnf1
4.13
4.14 (*Pull existential quantifiers (Skolemization)*)
4.15 fun skolemize th =
5.1 --- a/src/HOL/Tools/res_axioms.ML Thu Apr 28 17:08:08 2005 +0200
5.2 +++ b/src/HOL/Tools/res_axioms.ML Thu Apr 28 17:56:58 2005 +0200
5.3 @@ -141,75 +141,6 @@
5.4 end;
5.5
5.6
5.7 -(* some lemmas *)
5.8 -
5.9 -Goal "(P==True) ==> P";
5.10 -by(Blast_tac 1);
5.11 -qed "Eq_TrueD1";
5.12 -
5.13 -Goal "(True==P) ==> P";
5.14 -by(Blast_tac 1);
5.15 -qed "Eq_TrueD2";
5.16 -
5.17 -Goal "(P=True) ==> P";
5.18 -by(Blast_tac 1);
5.19 -qed "Eq_TrueD3";
5.20 -
5.21 -Goal "(P==False) ==> ~P";
5.22 -by(Blast_tac 1);
5.23 -qed "Eq_FalseD1";
5.24 -
5.25 -Goal "(False==P) ==> ~P";
5.26 -by(Blast_tac 1);
5.27 -qed "Eq_FalseD2";
5.28 -
5.29 -Goal "(P=False) ==> ~P";
5.30 -by(Blast_tac 1);
5.31 -qed "Eq_FalseD3";
5.32 -
5.33 -
5.34 -Goal "[|u == (if P then x else y); P|] ==> u==x";
5.35 -by Auto_tac;
5.36 -qed "eq_if_elim1";
5.37 -
5.38 -
5.39 -Goal "[|u == (if P then x else y); ~P|] ==> u==y";
5.40 -by Auto_tac;
5.41 -qed"eq_if_elim2";
5.42 -
5.43 -
5.44 -
5.45 -fun resolve_or_id ths th =
5.46 - case [th] RL ths of
5.47 - [] => [th]
5.48 - | ths2 => ths2;
5.49 -
5.50 -
5.51 -
5.52 -val remove_bool_ths = [eq_if_elim1,eq_if_elim2,Eq_TrueD1,Eq_TrueD2,Eq_FalseD1,Eq_FalseD2];
5.53 -
5.54 -
5.55 -
5.56 -local
5.57 -
5.58 - fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]);
5.59 -
5.60 -val small_simps =
5.61 - map prove
5.62 - ["(P | True) == True", "(True | P) == True",
5.63 - "(P & True) == P", "(True & P) == P",
5.64 - "(False | P) == P", "(P | False) == P",
5.65 - "(False & P) == False", "(P & False) == False",
5.66 - "~True == False", "~False == True"(*,
5.67 - "(False = P) == ~P", "(P = False) == ~P",
5.68 - "(True = P) == P", "(P = True) == P"*)
5.69 - (*"(True ==> PROP P) == PROP P"*)];
5.70 -in
5.71 -
5.72 -val small_simpset = empty_ss addsimps small_simps
5.73 -
5.74 -end;
5.75 -
5.76
5.77 signature RES_AXIOMS =
5.78 sig
5.79 @@ -230,8 +161,7 @@
5.80 : (Term.term * Term.term) list -> Thm.thm list -> Term.term list
5.81 val claset_rules_of_thy : Theory.theory -> Thm.thm list
5.82 val simpset_rules_of_thy : Theory.theory -> (string * Thm.thm) list
5.83 -val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
5.84 -val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
5.85 +val clausify_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
5.86
5.87 end;
5.88
5.89 @@ -258,25 +188,19 @@
5.90 end;
5.91
5.92
5.93 -
5.94 -(* added this function to remove True/False in a theorem that is in NNF form. *)
5.95 -fun rm_TF_nnf thm = simplify small_simpset thm;
5.96 -
5.97 -
5.98 (* convert a theorem into NNF and also skolemize it. *)
5.99 fun skolem_axiom thm =
5.100 - let val thm' = (skolemize o rm_TF_nnf o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm
5.101 + if Term.is_first_order (prop_of thm) then
5.102 + let val thm' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm
5.103 in
5.104 repeat_RS thm' someI_ex
5.105 - end;
5.106 + end
5.107 + else raise THM ("skolem_axiom: not first-order", 0, [thm]);
5.108
5.109
5.110 -fun isa_cls thm = make_clauses [skolem_axiom thm]
5.111 +fun cnf_rule thm = make_clauses [skolem_axiom thm]
5.112
5.113 -fun cnf_elim thm = isa_cls (transform_elim thm);
5.114 -
5.115 -val cnf_rule = isa_cls;
5.116 -
5.117 +fun cnf_elim thm = cnf_rule (transform_elim thm);
5.118
5.119
5.120 (*Transfer a theorem in to theory Reconstruction.thy if it is not already
5.121 @@ -383,16 +307,11 @@
5.122 fun make_axiom_clauses _ [] = []
5.123 | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss
5.124 in
5.125 - make_axiom_clauses 0 isa_clauses'
5.126 -
5.127 + make_axiom_clauses 0 isa_clauses'
5.128 end;
5.129
5.130
5.131 -(******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******)
5.132 -
5.133 -
5.134 -fun retr_thms ([]:MetaSimplifier.rrule list) = []
5.135 - | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
5.136 +(**** Extract and Clausify theorems from a theory's claset and simpset ****)
5.137
5.138 fun claset_rules_of_thy thy =
5.139 let val clsset = rep_cs (claset_of thy)
5.140 @@ -405,89 +324,48 @@
5.141 end;
5.142
5.143 fun simpset_rules_of_thy thy =
5.144 - let val simpset = simpset_of thy
5.145 - val rules = #rules(fst (rep_ss simpset))
5.146 - val thms = retr_thms (map #2 (Net.dest rules))
5.147 + let val rules = #rules(fst (rep_ss (simpset_of thy)))
5.148 in
5.149 - thms
5.150 + map (fn (_,r) => (#name r, #thm r)) (Net.dest rules)
5.151 end;
5.152
5.153
5.154 -(**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****)
5.155 +(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)
5.156
5.157 (* classical rules *)
5.158 -fun cnf_classical_rules [] err_list = ([],err_list)
5.159 - | cnf_classical_rules (thm::thms) err_list =
5.160 - let val (ts,es) = cnf_classical_rules thms err_list
5.161 - in
5.162 - ((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es))
5.163 - end;
5.164 +fun cnf_rules [] err_list = ([],err_list)
5.165 + | cnf_rules (thm::thms) err_list =
5.166 + let val (ts,es) = cnf_rules thms err_list
5.167 + in (cnf_axiom thm :: ts,es) handle _ => (ts,(thm::es)) end;
5.168
5.169
5.170 (* CNF all rules from a given theory's classical reasoner *)
5.171 fun cnf_classical_rules_thy thy =
5.172 - let val rules = claset_rules_of_thy thy
5.173 - in
5.174 - cnf_classical_rules rules []
5.175 - end;
5.176 -
5.177 -
5.178 -(* simplifier rules *)
5.179 -fun cnf_simpset_rules [] err_list = ([],err_list)
5.180 - | cnf_simpset_rules (thm::thms) err_list =
5.181 - let val (ts,es) = cnf_simpset_rules thms err_list
5.182 - val thm' = resolve_or_id remove_bool_ths thm
5.183 - in
5.184 - ((map cnf_axiom thm')@ts,es) handle _ => (ts,(thm::es))
5.185 - end;
5.186 -
5.187 + cnf_rules (claset_rules_of_thy thy) [];
5.188
5.189 (* CNF all simplifier rules from a given theory's simpset *)
5.190 fun cnf_simpset_rules_thy thy =
5.191 - let val thms = map #2 (simpset_rules_of_thy thy)
5.192 - in
5.193 - cnf_simpset_rules thms []
5.194 - end;
5.195 + cnf_rules (map #2 (simpset_rules_of_thy thy)) [];
5.196
5.197
5.198 -
5.199 -(**** Convert all theorems of a classical reason/simpset into clauses (ResClause.clause) ****)
5.200 +(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
5.201
5.202 (* classical rules *)
5.203 -fun clausify_classical_rules [] err_list = ([],err_list)
5.204 - | clausify_classical_rules (thm::thms) err_list =
5.205 - let val (ts,es) = clausify_classical_rules thms err_list
5.206 +fun clausify_rules [] err_list = ([],err_list)
5.207 + | clausify_rules (thm::thms) err_list =
5.208 + let val (ts,es) = clausify_rules thms err_list
5.209 in
5.210 ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es))
5.211 end;
5.212
5.213
5.214 -
5.215 (* convert all classical rules from a given theory into Clause.clause format. *)
5.216 fun clausify_classical_rules_thy thy =
5.217 - let val rules = claset_rules_of_thy thy
5.218 - in
5.219 - clausify_classical_rules rules []
5.220 - end;
5.221 -
5.222 -
5.223 -(* simplifier rules *)
5.224 -fun clausify_simpset_rules [] err_list = ([],err_list)
5.225 - | clausify_simpset_rules (thm::thms) err_list =
5.226 - let val (ts,es) = clausify_simpset_rules thms err_list
5.227 - in
5.228 - ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es))
5.229 - end;
5.230 -
5.231 + clausify_rules (claset_rules_of_thy thy) [];
5.232
5.233 (* convert all simplifier rules from a given theory into Clause.clause format. *)
5.234 fun clausify_simpset_rules_thy thy =
5.235 - let val thms = map #2 (simpset_rules_of_thy thy)
5.236 - in
5.237 - clausify_simpset_rules thms []
5.238 - end;
5.239 -
5.240 -
5.241 + clausify_rules (map #2 (simpset_rules_of_thy thy)) [];
5.242
5.243
5.244 end;