CVSfj
authorquigley
Mon Apr 04 18:39:45 2005 +0200 (2005-04-04)
changeset 15652a9d65894962e
parent 15651 4b393520846e
child 15653 3549ff7158f3
CVSfj


-------------------------------------------------------------------
---------------------------------------------------------------
Temporarily added until res_axioms.ML is altered.
src/HOL/Tools/ATP/myres_axioms.ML
src/HOL/Tools/ATP/watcher.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/ATP/myres_axioms.ML	Mon Apr 04 18:39:45 2005 +0200
     1.3 @@ -0,0 +1,444 @@
     1.4 +(*  Author: Jia Meng, Cambridge University Computer Laboratory
     1.5 +    ID: $Id$
     1.6 +    Copyright 2004 University of Cambridge
     1.7 +
     1.8 +Transformation of axiom rules (elim/intro/etc) into CNF forms.    
     1.9 +*)
    1.10 +
    1.11 +
    1.12 +
    1.13 +
    1.14 +(* a tactic used to prove an elim-rule. *)
    1.15 +fun elimRule_tac thm =
    1.16 +    ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
    1.17 +    REPEAT(Fast_tac 1);
    1.18 +
    1.19 +
    1.20 +(* This following version fails sometimes, need to investigate, do not use it now. *)
    1.21 +fun elimRule_tac' thm =
    1.22 +   ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
    1.23 +   REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); 
    1.24 +
    1.25 +
    1.26 +exception ELIMR2FOL of string;
    1.27 +
    1.28 +(* functions used to construct a formula *)
    1.29 +
    1.30 +fun make_imp (prem,concl) = Const("op -->", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ prem $ concl;
    1.31 +
    1.32 +
    1.33 +fun make_disjs [x] = x
    1.34 +  | make_disjs (x :: xs) = Const("op |",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_disjs xs)
    1.35 +
    1.36 +
    1.37 +fun make_conjs [x] = x
    1.38 +  | make_conjs (x :: xs) = Const("op &", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_conjs xs)
    1.39 +
    1.40 +
    1.41 +fun add_EX term [] = term
    1.42 +  | add_EX term ((x,xtp)::xs) = add_EX (Const ("Ex",Type("fun",[Type("fun",[xtp,Type("bool",[])]),Type("bool",[])])) $ Abs (x,xtp,term)) xs;
    1.43 +
    1.44 +
    1.45 +exception TRUEPROP of string; 
    1.46 +
    1.47 +fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P
    1.48 +  | strip_trueprop _ = raise TRUEPROP("not a prop!");
    1.49 +
    1.50 +
    1.51 +fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P;
    1.52 +
    1.53 +
    1.54 +fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_))= (p = q)
    1.55 +  | is_neg _ _ = false;
    1.56 +
    1.57 +
    1.58 +exception STRIP_CONCL;
    1.59 +
    1.60 +
    1.61 +fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
    1.62 +    let val P' = strip_trueprop P
    1.63 +	val prems' = P'::prems
    1.64 +    in
    1.65 +	strip_concl' prems' bvs  Q
    1.66 +    end
    1.67 +  | strip_concl' prems bvs P = 
    1.68 +    let val P' = neg (strip_trueprop P)
    1.69 +    in
    1.70 +	add_EX (make_conjs (P'::prems)) bvs
    1.71 +    end;
    1.72 +
    1.73 +
    1.74 +fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body))  = strip_concl prems ((x,xtp)::bvs) concl body
    1.75 +  | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
    1.76 +    if (is_neg P concl) then (strip_concl' prems bvs Q)
    1.77 +    else
    1.78 +	(let val P' = strip_trueprop P
    1.79 +	     val prems' = P'::prems
    1.80 +	 in
    1.81 +	     strip_concl prems' bvs  concl Q
    1.82 +	 end)
    1.83 +  | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
    1.84 + 
    1.85 +
    1.86 +
    1.87 +fun trans_elim (main,others,concl) =
    1.88 +    let val others' = map (strip_concl [] [] concl) others
    1.89 +	val disjs = make_disjs others'
    1.90 +    in
    1.91 +	make_imp(strip_trueprop main,disjs)
    1.92 +    end;
    1.93 +
    1.94 +
    1.95 +(* aux function of elim2Fol, take away predicate variable. *)
    1.96 +fun elimR2Fol_aux prems concl = 
    1.97 +    let val nprems = length prems
    1.98 +	val main = hd prems
    1.99 +    in
   1.100 +	if (nprems = 1) then neg (strip_trueprop main)
   1.101 +        else trans_elim (main, tl prems, concl)
   1.102 +    end;
   1.103 +
   1.104 +
   1.105 +fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term; 
   1.106 +	    
   1.107 +(* convert an elim rule into an equivalent formula, of type Term.term. *)
   1.108 +fun elimR2Fol elimR = 
   1.109 +    let val elimR' = Drule.freeze_all elimR
   1.110 +	val (prems,concl) = (prems_of elimR', concl_of elimR')
   1.111 +    in
   1.112 +	case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) 
   1.113 +		      => trueprop (elimR2Fol_aux prems concl)
   1.114 +                    | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems concl) 
   1.115 +		    | _ => raise ELIMR2FOL("Not an elimination rule!")
   1.116 +    end;
   1.117 +
   1.118 +
   1.119 +
   1.120 +(**** use prove_goalw_cterm to prove ****)
   1.121 +
   1.122 +(* convert an elim-rule into an equivalent theorem that does not have the predicate variable. *) 
   1.123 +fun transform_elim thm =
   1.124 +    let val tm = elimR2Fol thm
   1.125 +	val ctm = cterm_of (sign_of_thm thm) tm	
   1.126 +    in
   1.127 +	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac thm])
   1.128 +    end;	
   1.129 +
   1.130 +
   1.131 +
   1.132 +
   1.133 +(* some lemmas *)
   1.134 +
   1.135 +Goal "(P==True) ==> P";
   1.136 +by(Blast_tac 1);
   1.137 +qed "Eq_TrueD1";
   1.138 +
   1.139 +Goal "(P=True) ==> P";
   1.140 +by(Blast_tac 1);
   1.141 +qed "Eq_TrueD2";
   1.142 +
   1.143 +Goal "(P==False) ==> ~P";
   1.144 +by(Blast_tac 1);
   1.145 +qed "Eq_FalseD1";
   1.146 +
   1.147 +Goal "(P=False) ==> ~P";
   1.148 +by(Blast_tac 1);
   1.149 +qed "Eq_FalseD2";
   1.150 +
   1.151 +local 
   1.152 +
   1.153 +    fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]);
   1.154 +
   1.155 +val small_simps = 
   1.156 +  map prove 
   1.157 +   ["(P | True) == True", "(True | P) == True",
   1.158 +    "(P & True) == P", "(True & P) == P",
   1.159 +    "(False | P) == P", "(P | False) == P",
   1.160 +    "(False & P) == False", "(P & False) == False",
   1.161 +    "~True == False", "~False == True"];
   1.162 +in
   1.163 +
   1.164 +val small_simpset = empty_ss addsimps small_simps
   1.165 +
   1.166 +end;
   1.167 +
   1.168 +
   1.169 +(* to be fixed: cnf_intro, cnf_rule, is_introR *)
   1.170 +
   1.171 +(* check if a rule is an elim rule *)
   1.172 +fun is_elimR thm = 
   1.173 +    case (concl_of thm) of (Const ("Trueprop", _) $ Var (idx,_)) => true
   1.174 +			 | Var(indx,Type("prop",[])) => true
   1.175 +			 | _ => false;
   1.176 +
   1.177 +
   1.178 +(* repeated resolution *)
   1.179 +fun repeat_RS thm1 thm2 =
   1.180 +    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
   1.181 +    in
   1.182 +	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
   1.183 +    end;
   1.184 +
   1.185 +
   1.186 +
   1.187 +(* added this function to remove True/False in a theorem that is in NNF form. *)
   1.188 +fun rm_TF_nnf thm = simplify small_simpset thm;
   1.189 +
   1.190 +
   1.191 +(* convert a theorem into NNF and also skolemize it. *)
   1.192 +fun skolem_axiom thm = 
   1.193 +    let val thm' = (skolemize o rm_TF_nnf o  make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm
   1.194 +    in 
   1.195 +	repeat_RS thm' someI_ex
   1.196 +    end;
   1.197 +
   1.198 +
   1.199 +fun isa_cls thm = make_clauses [skolem_axiom thm]
   1.200 +
   1.201 +fun cnf_elim thm = isa_cls (transform_elim thm);
   1.202 +
   1.203 +val cnf_rule = isa_cls;	
   1.204 +
   1.205 +
   1.206 +
   1.207 +(*Transfer a theorem in to theory Reconstruction.thy if it is not already
   1.208 +  inside that theory -- because it's needed for Skolemization *)
   1.209 +
   1.210 +val recon_thy = ThyInfo.get_theory"Reconstruction";
   1.211 +
   1.212 +fun transfer_to_Reconstruction thm =
   1.213 +    transfer recon_thy thm handle THM _ => thm;
   1.214 +
   1.215 +(* remove "True" clause *)
   1.216 +fun rm_redundant_cls [] = []
   1.217 +  | rm_redundant_cls (thm::thms) =
   1.218 +    let val t = prop_of thm
   1.219 +    in
   1.220 +	case t of (Const ("Trueprop", _) $ Const ("True", _)) => rm_redundant_cls thms
   1.221 +		| _ => thm::(rm_redundant_cls thms)
   1.222 +    end;
   1.223 +
   1.224 +(* transform an Isabelle thm into CNF *)
   1.225 +fun cnf_axiom thm =
   1.226 +    let val thm' = transfer_to_Reconstruction thm
   1.227 +	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
   1.228 +    in
   1.229 +	rm_redundant_cls thm''
   1.230 +    end;
   1.231 +
   1.232 +fun meta_cnf_axiom thm = 
   1.233 +    map (zero_var_indexes o Meson.make_meta_clause) (cnf_axiom thm);
   1.234 +
   1.235 +
   1.236 +(* changed: with one extra case added *)
   1.237 +fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars
   1.238 +  | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars (* EX x. body *)
   1.239 +  | univ_vars_of_aux (P $ Q) vars =
   1.240 +    let val vars' = univ_vars_of_aux P vars
   1.241 +    in
   1.242 +	univ_vars_of_aux Q vars'
   1.243 +    end
   1.244 +  | univ_vars_of_aux (t as Var(_,_)) vars = 
   1.245 +    if (t mem vars) then vars else (t::vars)
   1.246 +  | univ_vars_of_aux _ vars = vars;
   1.247 +  
   1.248 +
   1.249 +fun univ_vars_of t = univ_vars_of_aux t [];
   1.250 +
   1.251 +
   1.252 +fun get_new_skolem epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,tp,_)))  = 
   1.253 +    let val all_vars = univ_vars_of t
   1.254 +	val sk_term = ResSkolemFunction.gen_skolem all_vars tp
   1.255 +    in
   1.256 +	(sk_term,(t,sk_term)::epss)
   1.257 +    end;
   1.258 +
   1.259 +
   1.260 +fun sk_lookup [] t = NONE
   1.261 +  | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then SOME (sk_tm) else (sk_lookup tms t);
   1.262 +
   1.263 +
   1.264 +
   1.265 +(* get the proper skolem term to replace epsilon term *)
   1.266 +fun get_skolem epss t = 
   1.267 +    let val sk_fun = sk_lookup epss t
   1.268 +    in
   1.269 +	case sk_fun of NONE => get_new_skolem epss t
   1.270 +		     | SOME sk => (sk,epss)
   1.271 +    end;
   1.272 +
   1.273 +
   1.274 +fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t
   1.275 +  | rm_Eps_cls_aux epss (P $ Q) =
   1.276 +    let val (P',epss') = rm_Eps_cls_aux epss P
   1.277 +	val (Q',epss'') = rm_Eps_cls_aux epss' Q
   1.278 +    in
   1.279 +	(P' $ Q',epss'')
   1.280 +    end
   1.281 +  | rm_Eps_cls_aux epss t = (t,epss);
   1.282 +
   1.283 +
   1.284 +fun rm_Eps_cls epss thm =
   1.285 +    let val tm = prop_of thm
   1.286 +    in
   1.287 +	rm_Eps_cls_aux epss tm
   1.288 +    end;
   1.289 +
   1.290 +
   1.291 +(* remove the epsilon terms in a formula, by skolem terms. *)
   1.292 +fun rm_Eps _ [] = []
   1.293 +  | rm_Eps epss (thm::thms) = 
   1.294 +    let val (thm',epss') = rm_Eps_cls epss thm
   1.295 +    in
   1.296 +	thm' :: (rm_Eps epss' thms)
   1.297 +    end;
   1.298 +
   1.299 +
   1.300 +
   1.301 +(* changed, now it also finds out the name of the theorem. *)
   1.302 +(* convert a theorem into CNF and then into Clause.clause format. *)
   1.303 +fun clausify_axiom thm =
   1.304 +    let val isa_clauses = cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
   1.305 +        val isa_clauses' = rm_Eps [] isa_clauses
   1.306 +        val thm_name = Thm.name_of_thm thm
   1.307 +	val clauses_n = length isa_clauses
   1.308 +	fun make_axiom_clauses _ [] = []
   1.309 +	  | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss 
   1.310 +    in
   1.311 +	make_axiom_clauses 0 isa_clauses'
   1.312 +		
   1.313 +    end;
   1.314 +  
   1.315 +
   1.316 +(******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******)
   1.317 +
   1.318 +
   1.319 +local
   1.320 +
   1.321 +fun retr_thms ([]:MetaSimplifier.rrule list) = []
   1.322 +	  | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
   1.323 +
   1.324 +
   1.325 +fun snds [] = []
   1.326 +  |   snds ((x,y)::l) = y::(snds l);
   1.327 +
   1.328 +in
   1.329 +
   1.330 +
   1.331 +fun claset_rules_of_thy thy =
   1.332 +    let val clsset = rep_cs (claset_of thy)
   1.333 +	val safeEs = #safeEs clsset
   1.334 +	val safeIs = #safeIs clsset
   1.335 +	val hazEs = #hazEs clsset
   1.336 +	val hazIs = #hazIs clsset
   1.337 +    in
   1.338 +	safeEs @ safeIs @ hazEs @ hazIs
   1.339 +    end;
   1.340 +
   1.341 +fun simpset_rules_of_thy thy =
   1.342 +    let val simpset = simpset_of thy
   1.343 +	val rules = #rules(fst (rep_ss simpset))
   1.344 +	val thms = retr_thms (snds(Net.dest rules))
   1.345 +    in
   1.346 +	thms
   1.347 +    end;
   1.348 +
   1.349 +
   1.350 +
   1.351 +(**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****)
   1.352 +
   1.353 +(* classical rules *)
   1.354 +fun cnf_classical_rules [] err_list = ([],err_list)
   1.355 +  | cnf_classical_rules (thm::thms) err_list = 
   1.356 +    let val (ts,es) = cnf_classical_rules thms err_list
   1.357 +    in
   1.358 +	((cnf_axiom thm)::ts,es) handle  _ => (ts,(thm::es))
   1.359 +    end;
   1.360 +
   1.361 +
   1.362 +(* CNF all rules from a given theory's classical reasoner *)
   1.363 +fun cnf_classical_rules_thy thy = 
   1.364 +    let val rules = claset_rules_of_thy thy
   1.365 +    in
   1.366 +        cnf_classical_rules rules []
   1.367 +    end;
   1.368 +
   1.369 +
   1.370 +(* simplifier rules *)
   1.371 +fun cnf_simpset_rules [] err_list = ([],err_list)
   1.372 +  | cnf_simpset_rules (thm::thms) err_list =
   1.373 +    let val (ts,es) = cnf_simpset_rules thms err_list
   1.374 +    in
   1.375 +	((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es))
   1.376 +    end;
   1.377 +
   1.378 +
   1.379 +(* CNF all simplifier rules from a given theory's simpset *)
   1.380 +fun cnf_simpset_rules_thy thy =
   1.381 +    let val thms = simpset_rules_of_thy thy
   1.382 +    in
   1.383 +	cnf_simpset_rules thms []
   1.384 +    end;
   1.385 +
   1.386 +
   1.387 +
   1.388 +(**** Convert all theorems of a classical reason/simpset into clauses (ResClause.clause) ****)
   1.389 +
   1.390 +(* classical rules *)
   1.391 +fun clausify_classical_rules [] err_list = ([],err_list)
   1.392 +  | clausify_classical_rules (thm::thms) err_list =
   1.393 +    let val (ts,es) = clausify_classical_rules thms err_list
   1.394 +    in
   1.395 +	((clausify_axiom thm)::ts,es) handle  _ => (ts,(thm::es))
   1.396 +    end;
   1.397 +
   1.398 +
   1.399 +
   1.400 +(* convert all classical rules from a given theory's classical reasoner into Clause.clause format. *)
   1.401 +fun clausify_classical_rules_thy thy =
   1.402 +    let val rules = claset_rules_of_thy thy
   1.403 +    in
   1.404 +	clausify_classical_rules rules []
   1.405 +    end;
   1.406 +
   1.407 +
   1.408 +(* simplifier rules *)
   1.409 +fun clausify_simpset_rules [] err_list = ([],err_list)
   1.410 +  | clausify_simpset_rules (thm::thms) err_list =
   1.411 +    let val (ts,es) = clausify_simpset_rules thms err_list
   1.412 +    in
   1.413 +	((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es))
   1.414 +    end;
   1.415 +
   1.416 +
   1.417 +(* convert all simplifier rules from a given theory's simplifier into Clause.clause format. *)
   1.418 +fun clausify_simpset_rules_thy thy =
   1.419 +    let val thms = simpset_rules_of_thy thy
   1.420 +    in
   1.421 +	clausify_simpset_rules thms []
   1.422 +    end;
   1.423 +
   1.424 +(* lcp-modified code *)
   1.425 +(*
   1.426 +fun retr_thms ([]:MetaSimplifier.rrule list) = []
   1.427 +	  | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
   1.428 +
   1.429 +fun snds [] = []
   1.430 +   | snds ((x,y)::l) = y::(snds l);
   1.431 +
   1.432 +fun simpset_rules_of_thy thy =
   1.433 +     let val simpset = simpset_of thy
   1.434 +	val rules = #rules(fst (rep_ss simpset))
   1.435 +	val thms = retr_thms (snds(Net.dest rules))
   1.436 +     in	thms  end;
   1.437 +
   1.438 +print_depth 200;
   1.439 +simpset_rules_of_thy Main.thy;
   1.440 +
   1.441 +
   1.442 +
   1.443 +
   1.444 +
   1.445 +*)
   1.446 +
   1.447 +end;
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Sat Apr 02 00:33:51 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Apr 04 18:39:45 2005 +0200
     2.3 @@ -19,11 +19,11 @@
     2.4  use "modUnix";*)
     2.5  (*use "/homes/clq20/Jia_Code/TransStartIsar";*)
     2.6  
     2.7 -use "~~/VampireCommunication";
     2.8 -use "~~/SpassCommunication";
     2.9 +use "~~/src/HOL/Tools/ATP/VampireCommunication.ML";
    2.10 +use "~~/src/HOL/Tools/ATP/SpassCommunication.ML";
    2.11  
    2.12  
    2.13 -use "~~/modUnix";
    2.14 +use "~~/src/HOL/Tools/ATP/modUnix.ML";
    2.15  
    2.16  
    2.17  structure Watcher: WATCHER =
    2.18 @@ -34,7 +34,6 @@
    2.19  
    2.20  val goals_being_watched = ref 0;
    2.21  
    2.22 -
    2.23  fun remove y [] = []
    2.24  |   remove y (x::xs) = (if y = x 
    2.25                         then 
    2.26 @@ -98,7 +97,7 @@
    2.27                                                       let 
    2.28                                                          val dfg_dir = File.tmp_path (Path.basic "dfg");
    2.29                                                          (* need to check here if the directory exists and, if not, create it*)
    2.30 -                                                         val  outfile = TextIO.openAppend(" /thmstring_in_watcher");                                                                                    
    2.31 +                                                         val  outfile = TextIO.openAppend("thmstring_in_watcher");                                                                                    
    2.32                                                           val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    2.33                                                           val _ =  TextIO.closeOut outfile
    2.34                                                           val dfg_create =if File.exists dfg_dir 
    2.35 @@ -386,7 +385,7 @@
    2.36                                                           (childProc::(checkChildren (otherChildren, toParentStr)))
    2.37                                                   end
    2.38                                                 else
    2.39 -                                                   let val  outfile = TextIO.openOut("child_incoming");  
    2.40 +                                                   let val  outfile = TextIO.openAppend("child_incoming");  
    2.41                                                  val _ = TextIO.output (outfile,"No child output " )
    2.42                                                  val _ =  TextIO.closeOut outfile
    2.43                                                   in