fixed treatment of higher-order simprules
authorpaulson
Thu Apr 28 17:56:58 2005 +0200 (2005-04-28)
changeset 158728336ff711d80
parent 15871 e524119dbf19
child 15873 02d9f110ecc1
fixed treatment of higher-order simprules
src/HOL/Main.thy
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/res_axioms.ML
     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 -
   5.196 +    cnf_rules (map #2 (simpset_rules_of_thy thy)) [];
   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;