src/HOL/Tools/res_axioms.ML
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15684 5ec4d21889d6
child 15736 1bb0399a9517
permissions -rw-r--r--
*** empty log message ***
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 Transformation of axiom rules (elim/intro/etc) into CNF forms.    
     6 *)
     7 
     8 
     9 
    10 signature RES_ELIM_RULE =
    11 sig
    12 
    13 exception ELIMR2FOL of string
    14 val elimRule_tac : Thm.thm -> Tactical.tactic
    15 val elimR2Fol : Thm.thm -> Term.term
    16 val transform_elim : Thm.thm -> Thm.thm
    17 
    18 end;
    19 
    20 structure ResElimRule: RES_ELIM_RULE =
    21 
    22 struct
    23 
    24 (* a tactic used to prove an elim-rule. *)
    25 fun elimRule_tac thm =
    26     ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
    27     REPEAT(Fast_tac 1);
    28 
    29 
    30 (* This following version fails sometimes, need to investigate, do not use it now. *)
    31 fun elimRule_tac' thm =
    32    ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
    33    REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); 
    34 
    35 
    36 exception ELIMR2FOL of string;
    37 
    38 (* functions used to construct a formula *)
    39 
    40 fun make_imp (prem,concl) = Const("op -->", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ prem $ concl;
    41 
    42 
    43 fun make_disjs [x] = x
    44   | make_disjs (x :: xs) = Const("op |",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_disjs xs)
    45 
    46 
    47 fun make_conjs [x] = x
    48   | make_conjs (x :: xs) = Const("op &", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_conjs xs)
    49 
    50 
    51 fun add_EX term [] = term
    52   | add_EX term ((x,xtp)::xs) = add_EX (Const ("Ex",Type("fun",[Type("fun",[xtp,Type("bool",[])]),Type("bool",[])])) $ Abs (x,xtp,term)) xs;
    53 
    54 
    55 exception TRUEPROP of string; 
    56 
    57 fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P
    58   | strip_trueprop _ = raise TRUEPROP("not a prop!");
    59 
    60 
    61 fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P;
    62 
    63 
    64 fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_))= (p = q)
    65   | is_neg _ _ = false;
    66 
    67 
    68 exception STRIP_CONCL;
    69 
    70 
    71 fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
    72     let val P' = strip_trueprop P
    73 	val prems' = P'::prems
    74     in
    75 	strip_concl' prems' bvs  Q
    76     end
    77   | strip_concl' prems bvs P = 
    78     let val P' = neg (strip_trueprop P)
    79     in
    80 	add_EX (make_conjs (P'::prems)) bvs
    81     end;
    82 
    83 
    84 fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body))  = strip_concl prems ((x,xtp)::bvs) concl body
    85   | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
    86     if (is_neg P concl) then (strip_concl' prems bvs Q)
    87     else
    88 	(let val P' = strip_trueprop P
    89 	     val prems' = P'::prems
    90 	 in
    91 	     strip_concl prems' bvs  concl Q
    92 	 end)
    93   | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
    94  
    95 
    96 
    97 fun trans_elim (main,others,concl) =
    98     let val others' = map (strip_concl [] [] concl) others
    99 	val disjs = make_disjs others'
   100     in
   101 	make_imp(strip_trueprop main,disjs)
   102     end;
   103 
   104 
   105 (* aux function of elim2Fol, take away predicate variable. *)
   106 fun elimR2Fol_aux prems concl = 
   107     let val nprems = length prems
   108 	val main = hd prems
   109     in
   110 	if (nprems = 1) then neg (strip_trueprop main)
   111         else trans_elim (main, tl prems, concl)
   112     end;
   113 
   114 
   115 fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term; 
   116 	    
   117 (* convert an elim rule into an equivalent formula, of type Term.term. *)
   118 fun elimR2Fol elimR = 
   119     let val elimR' = Drule.freeze_all elimR
   120 	val (prems,concl) = (prems_of elimR', concl_of elimR')
   121     in
   122 	case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) 
   123 		      => trueprop (elimR2Fol_aux prems concl)
   124                     | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems concl) 
   125 		    | _ => raise ELIMR2FOL("Not an elimination rule!")
   126     end;
   127 
   128 
   129 
   130 (**** use prove_goalw_cterm to prove ****)
   131 
   132 (* convert an elim-rule into an equivalent theorem that does not have the predicate variable. *) 
   133 fun transform_elim thm =
   134     let val tm = elimR2Fol thm
   135 	val ctm = cterm_of (sign_of_thm thm) tm	
   136     in
   137 	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac thm])
   138     end;	
   139 
   140 
   141 end;
   142 
   143 
   144 (* some lemmas *)
   145 
   146 Goal "(P==True) ==> P";
   147 by(Blast_tac 1);
   148 qed "Eq_TrueD1";
   149 
   150 Goal "(True==P) ==> P";
   151 by(Blast_tac 1);
   152 qed "Eq_TrueD2";
   153 
   154 Goal "(P=True) ==> P";
   155 by(Blast_tac 1);
   156 qed "Eq_TrueD3";
   157 
   158 Goal "(P==False) ==> ~P";
   159 by(Blast_tac 1);
   160 qed "Eq_FalseD1";
   161 
   162 Goal "(False==P) ==> ~P";
   163 by(Blast_tac 1);
   164 qed "Eq_FalseD2";
   165 
   166 Goal "(P=False) ==> ~P";
   167 by(Blast_tac 1);
   168 qed "Eq_FalseD3";
   169 
   170 
   171 Goal "[|u == (if P then x else y); P|] ==> u==x";
   172 by Auto_tac;
   173 qed "eq_if_elim1";
   174 
   175 
   176 Goal "[|u == (if P then x else y); ~P|] ==> u==y";
   177 by Auto_tac;
   178 qed"eq_if_elim2";
   179 
   180 
   181 
   182 fun resolve_or_id ths th =
   183      case [th] RL ths of
   184          []   => [th]
   185        | ths2 => ths2;
   186 
   187 
   188 
   189 val remove_bool_ths = [eq_if_elim1,eq_if_elim2,Eq_TrueD1,Eq_TrueD2,Eq_FalseD1,Eq_FalseD2];
   190 
   191 
   192 
   193 local 
   194 
   195     fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]);
   196 
   197 val small_simps = 
   198   map prove 
   199    ["(P | True) == True", "(True | P) == True",
   200     "(P & True) == P", "(True & P) == P",
   201     "(False | P) == P", "(P | False) == P",
   202     "(False & P) == False", "(P & False) == False",
   203     "~True == False", "~False == True"(*,
   204     "(False = P) == ~P", "(P = False) == ~P",
   205     "(True = P) == P",  "(P = True) == P"*)
   206     (*"(True ==> PROP P) == PROP P"*)];
   207 in
   208 
   209 val small_simpset = empty_ss addsimps small_simps
   210 
   211 end;
   212 
   213 
   214 signature RES_AXIOMS =
   215 sig
   216 
   217 val clausify_axiom : Thm.thm -> ResClause.clause list
   218 val cnf_axiom : Thm.thm -> Thm.thm list
   219 val meta_cnf_axiom : Thm.thm -> Thm.thm list
   220 val cnf_elim : Thm.thm -> Thm.thm list
   221 val cnf_rule : Thm.thm -> Thm.thm list
   222 val cnf_classical_rules_thy : Theory.theory -> Thm.thm list list * Thm.thm list
   223 val clausify_classical_rules_thy 
   224 : Theory.theory -> ResClause.clause list list * Thm.thm list
   225 val cnf_simpset_rules_thy 
   226 : Theory.theory -> Thm.thm list list * Thm.thm list
   227 val clausify_simpset_rules_thy 
   228 : Theory.theory -> ResClause.clause list list * Thm.thm list
   229 val rm_Eps 
   230 : (Term.term * Term.term) list -> Thm.thm list -> Term.term list
   231 val claset_rules_of_thy : Theory.theory -> Thm.thm list
   232 val simpset_rules_of_thy : Theory.theory -> Thm.thm list
   233 val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
   234 val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
   235 
   236 end;
   237 
   238 structure ResAxioms : RES_AXIOMS =
   239  
   240 struct
   241 
   242 open ResElimRule;
   243 
   244 (* to be fixed: cnf_intro, cnf_rule, is_introR *)
   245 
   246 (* check if a rule is an elim rule *)
   247 fun is_elimR thm = 
   248     case (concl_of thm) of (Const ("Trueprop", _) $ Var (idx,_)) => true
   249 			 | Var(indx,Type("prop",[])) => true
   250 			 | _ => false;
   251 
   252 
   253 (* repeated resolution *)
   254 fun repeat_RS thm1 thm2 =
   255     let val thm1' =  thm1 RS thm2 handle THM _ => thm1
   256     in
   257 	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
   258     end;
   259 
   260 
   261 
   262 (* added this function to remove True/False in a theorem that is in NNF form. *)
   263 fun rm_TF_nnf thm = simplify small_simpset thm;
   264 
   265 
   266 (* convert a theorem into NNF and also skolemize it. *)
   267 fun skolem_axiom thm = 
   268     let val thm' = (skolemize o rm_TF_nnf o  make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm
   269     in 
   270 	repeat_RS thm' someI_ex
   271     end;
   272 
   273 
   274 fun isa_cls thm = make_clauses [skolem_axiom thm]
   275 
   276 fun cnf_elim thm = isa_cls (transform_elim thm);
   277 
   278 val cnf_rule = isa_cls;	
   279 
   280 
   281 
   282 (*Transfer a theorem in to theory Reconstruction.thy if it is not already
   283   inside that theory -- because it's needed for Skolemization *)
   284 
   285 val recon_thy = ThyInfo.get_theory"Reconstruction";
   286 
   287 fun transfer_to_Reconstruction thm =
   288     transfer recon_thy thm handle THM _ => thm;
   289 
   290 (* remove "True" clause *)
   291 fun rm_redundant_cls [] = []
   292   | rm_redundant_cls (thm::thms) =
   293     let val t = prop_of thm
   294     in
   295 	case t of (Const ("Trueprop", _) $ Const ("True", _)) => rm_redundant_cls thms
   296 		| _ => thm::(rm_redundant_cls thms)
   297     end;
   298 
   299 (* transform an Isabelle thm into CNF *)
   300 fun cnf_axiom thm =
   301     let val thm' = transfer_to_Reconstruction thm
   302 	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
   303     in
   304 	map Thm.varifyT (rm_redundant_cls thm'')
   305     end;
   306 
   307 fun meta_cnf_axiom thm = 
   308     map (zero_var_indexes o Meson.make_meta_clause) (cnf_axiom thm);
   309 
   310 
   311 (* changed: with one extra case added *)
   312 fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars
   313   | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars (* EX x. body *)
   314   | univ_vars_of_aux (P $ Q) vars =
   315     let val vars' = univ_vars_of_aux P vars
   316     in
   317 	univ_vars_of_aux Q vars'
   318     end
   319   | univ_vars_of_aux (t as Var(_,_)) vars = 
   320     if (t mem vars) then vars else (t::vars)
   321   | univ_vars_of_aux _ vars = vars;
   322   
   323 
   324 fun univ_vars_of t = univ_vars_of_aux t [];
   325 
   326 
   327 fun get_new_skolem epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,tp,_)))  = 
   328     let val all_vars = univ_vars_of t
   329 	val sk_term = ResSkolemFunction.gen_skolem all_vars tp
   330     in
   331 	(sk_term,(t,sk_term)::epss)
   332     end;
   333 
   334 
   335 fun sk_lookup [] t = NONE
   336   | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then SOME (sk_tm) else (sk_lookup tms t);
   337 
   338 
   339 
   340 (* get the proper skolem term to replace epsilon term *)
   341 fun get_skolem epss t = 
   342     let val sk_fun = sk_lookup epss t
   343     in
   344 	case sk_fun of NONE => get_new_skolem epss t
   345 		     | SOME sk => (sk,epss)
   346     end;
   347 
   348 
   349 fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t
   350   | rm_Eps_cls_aux epss (P $ Q) =
   351     let val (P',epss') = rm_Eps_cls_aux epss P
   352 	val (Q',epss'') = rm_Eps_cls_aux epss' Q
   353     in
   354 	(P' $ Q',epss'')
   355     end
   356   | rm_Eps_cls_aux epss t = (t,epss);
   357 
   358 
   359 fun rm_Eps_cls epss thm =
   360     let val tm = prop_of thm
   361     in
   362 	rm_Eps_cls_aux epss tm
   363     end;
   364 
   365 
   366 (* remove the epsilon terms in a formula, by skolem terms. *)
   367 fun rm_Eps _ [] = []
   368   | rm_Eps epss (thm::thms) = 
   369     let val (thm',epss') = rm_Eps_cls epss thm
   370     in
   371 	thm' :: (rm_Eps epss' thms)
   372     end;
   373 
   374 
   375 
   376 (* changed, now it also finds out the name of the theorem. *)
   377 (* convert a theorem into CNF and then into Clause.clause format. *)
   378 fun clausify_axiom thm =
   379     let val isa_clauses = cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
   380         val isa_clauses' = rm_Eps [] isa_clauses
   381         val thm_name = Thm.name_of_thm thm
   382 	val clauses_n = length isa_clauses
   383 	fun make_axiom_clauses _ [] = []
   384 	  | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss 
   385     in
   386 	make_axiom_clauses 0 isa_clauses'
   387 		
   388     end;
   389   
   390 
   391 (******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******)
   392 
   393 
   394 local
   395 
   396 fun retr_thms ([]:MetaSimplifier.rrule list) = []
   397 	  | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
   398 
   399 
   400 fun snds [] = []
   401   |   snds ((x,y)::l) = y::(snds l);
   402 
   403 in
   404 
   405 
   406 fun claset_rules_of_thy thy =
   407     let val clsset = rep_cs (claset_of thy)
   408 	val safeEs = #safeEs clsset
   409 	val safeIs = #safeIs clsset
   410 	val hazEs = #hazEs clsset
   411 	val hazIs = #hazIs clsset
   412     in
   413 	safeEs @ safeIs @ hazEs @ hazIs
   414     end;
   415 
   416 fun simpset_rules_of_thy thy =
   417     let val simpset = simpset_of thy
   418 	val rules = #rules(fst (rep_ss simpset))
   419 	val thms = retr_thms (snds(Net.dest rules))
   420     in
   421 	thms
   422     end;
   423 
   424 end;
   425 
   426 
   427 (**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****)
   428 
   429 (* classical rules *)
   430 fun cnf_classical_rules [] err_list = ([],err_list)
   431   | cnf_classical_rules (thm::thms) err_list = 
   432     let val (ts,es) = cnf_classical_rules thms err_list
   433     in
   434 	((cnf_axiom thm)::ts,es) handle  _ => (ts,(thm::es))
   435     end;
   436 
   437 
   438 (* CNF all rules from a given theory's classical reasoner *)
   439 fun cnf_classical_rules_thy thy = 
   440     let val rules = claset_rules_of_thy thy
   441     in
   442         cnf_classical_rules rules []
   443     end;
   444 
   445 
   446 (* simplifier rules *)
   447 fun cnf_simpset_rules [] err_list = ([],err_list)
   448   | cnf_simpset_rules (thm::thms) err_list =
   449     let val (ts,es) = cnf_simpset_rules thms err_list
   450 	val thm' = resolve_or_id remove_bool_ths thm
   451     in
   452 	((map cnf_axiom thm')@ts,es) handle _ => (ts,(thm::es))
   453     end;
   454 
   455 
   456 (* CNF all simplifier rules from a given theory's simpset *)
   457 fun cnf_simpset_rules_thy thy =
   458     let val thms = simpset_rules_of_thy thy
   459     in
   460 	cnf_simpset_rules thms []
   461     end;
   462 
   463 
   464 
   465 (**** Convert all theorems of a classical reason/simpset into clauses (ResClause.clause) ****)
   466 
   467 (* classical rules *)
   468 fun clausify_classical_rules [] err_list = ([],err_list)
   469   | clausify_classical_rules (thm::thms) err_list =
   470     let val (ts,es) = clausify_classical_rules thms err_list
   471     in
   472 	((clausify_axiom thm)::ts,es) handle  _ => (ts,(thm::es))
   473     end;
   474 
   475 
   476 
   477 (* convert all classical rules from a given theory's classical reasoner into Clause.clause format. *)
   478 fun clausify_classical_rules_thy thy =
   479     let val rules = claset_rules_of_thy thy
   480     in
   481 	clausify_classical_rules rules []
   482     end;
   483 
   484 
   485 (* simplifier rules *)
   486 fun clausify_simpset_rules [] err_list = ([],err_list)
   487   | clausify_simpset_rules (thm::thms) err_list =
   488     let val (ts,es) = clausify_simpset_rules thms err_list
   489     in
   490 	((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es))
   491     end;
   492 
   493 
   494 (* convert all simplifier rules from a given theory's simplifier into Clause.clause format. *)
   495 fun clausify_simpset_rules_thy thy =
   496     let val thms = simpset_rules_of_thy thy
   497     in
   498 	clausify_simpset_rules thms []
   499     end;
   500 
   501 
   502 
   503 
   504 end;