src/HOL/Tools/cnf_funcs.ML
changeset 19236 150e8b0fb991
parent 17809 195045659c06
child 20440 e6fe74eebda3
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Fri Mar 10 16:21:49 2006 +0100
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Mar 10 16:31:50 2006 +0100
     1.3 @@ -2,14 +2,14 @@
     1.4      ID:         $Id$
     1.5      Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     1.6      Author:     Tjark Weber
     1.7 -    Copyright   2005
     1.8 +    Copyright   2005-2006
     1.9  
    1.10    Description:
    1.11    This file contains functions and tactics to transform a formula into
    1.12    Conjunctive Normal Form (CNF).
    1.13    A formula in CNF is of the following form:
    1.14  
    1.15 -      (x11 | x12 | .. x1n) & ... & (xm1 | xm2 | ... | xmk)
    1.16 +      (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
    1.17        False
    1.18        True
    1.19  
    1.20 @@ -23,11 +23,13 @@
    1.21    representation of clauses, which we call the "raw clauses".
    1.22    Raw clauses are of the form
    1.23  
    1.24 -      x1 ==> x2 ==> .. ==> xn ==> False ,
    1.25 +      x1', x2', ..., xn', ~ (x1 | x2 | ... | xn) ==> False |- False ,
    1.26 +
    1.27 +  where each xi is a literal, and each xi' is the negation normal form of ~xi.
    1.28  
    1.29 -  where each xi is a literal. Note that the above raw clause corresponds
    1.30 -  to the clause (x1' | ... | xn'), where each xi' is the negation normal
    1.31 -  form of ~xi.
    1.32 +  Raw clauses may contain further hyps of the form "~ clause ==> False".
    1.33 +  Literals are successively removed from the hyps of raw clauses by resolution
    1.34 +  during SAT proof reconstruction.
    1.35  *)
    1.36  
    1.37  signature CNF =
    1.38 @@ -37,8 +39,8 @@
    1.39  	val is_clause         : Term.term -> bool
    1.40  	val clause_is_trivial : Term.term -> bool
    1.41  
    1.42 -	val is_raw_clause  : Term.term -> bool
    1.43 -	val clause2raw_thm : Thm.thm -> Thm.thm
    1.44 +	val clause2raw_thm         : Thm.thm -> Thm.thm
    1.45 +	val rawhyps2clausehyps_thm : Thm.thm -> Thm.thm
    1.46  
    1.47  	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
    1.48  
    1.49 @@ -137,24 +139,10 @@
    1.50  	end;
    1.51  
    1.52  (* ------------------------------------------------------------------------- *)
    1.53 -(* is_raw_clause: returns true iff the term is of the form                   *)
    1.54 -(*        x1 ==> ... ==> xn ==> False ,                                      *)
    1.55 -(*      with n >= 1, where each xi is a literal                              *)
    1.56 -(* ------------------------------------------------------------------------- *)
    1.57 -
    1.58 -(* Term.term -> bool *)
    1.59 -
    1.60 -fun is_raw_clause (Const ("==>", _) $ x $ y) =
    1.61 -	is_literal x andalso
    1.62 -		(y = HOLogic.mk_Trueprop HOLogic.false_const orelse is_raw_clause y)
    1.63 -  | is_raw_clause _                          =
    1.64 -	false;
    1.65 -
    1.66 -(* ------------------------------------------------------------------------- *)
    1.67  (* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
    1.68 -(*        x1 | ... | xn                                                      *)
    1.69 +(*        ... |- x1 | ... | xn                                               *)
    1.70  (*      (where each xi is a literal) is translated to                        *)
    1.71 -(*        x1' ==> ... ==> xn' ==> False ,                                    *)
    1.72 +(*        ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False ,               *)
    1.73  (*      where each xi' is the negation normal form of ~xi.                   *)
    1.74  (* ------------------------------------------------------------------------- *)
    1.75  
    1.76 @@ -162,7 +150,9 @@
    1.77  
    1.78  fun clause2raw_thm c =
    1.79  let
    1.80 -	val thm1 = c RS clause2raw_notE  (* ~(x1 | ... | xn) ==> False *)
    1.81 +	val disj               = HOLogic.dest_Trueprop (prop_of c)
    1.82 +	val not_disj_imp_false = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_not disj), HOLogic.mk_Trueprop HOLogic.false_const)
    1.83 +	val thm1 = Thm.assume (cterm_of (theory_of_thm c) not_disj_imp_false)  (* ~(x1 | ... | xn) ==> False |- ~(x1 | ... | xn) ==> False *)
    1.84  	(* eliminates negated disjunctions from the i-th premise, possibly *)
    1.85  	(* adding new premises, then continues with the (i+1)-th premise   *)
    1.86  	(* Thm.thm -> int -> Thm.thm *)
    1.87 @@ -171,13 +161,38 @@
    1.88  			thm
    1.89  		else
    1.90  			not_disj_to_prem (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) (i+1)
    1.91 -	val thm2 = not_disj_to_prem thm1 1  (* ~x1 ==> ... ==> ~xn ==> False *)
    1.92 -	val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2)  (* x1' ==> ... ==> xn' ==> False *)
    1.93 +	val thm2 = not_disj_to_prem thm1 1  (* ~(x1 | ... | xn) ==> False |- ~x1 ==> ... ==> ~xn ==> False *)
    1.94 +	val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2)  (* ~(x1 | ... | xn) ==> False |- x1' ==> ... ==> xn' ==> False *)
    1.95 +	val thy3 = theory_of_thm thm3
    1.96 +	val thm4 = fold (fn prem => fn thm => Thm.implies_elim thm (Thm.assume (cterm_of thy3 prem))) (prems_of thm3) thm3  (* ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False *)
    1.97  in
    1.98 -	thm3
    1.99 +	thm4
   1.100  end;
   1.101  
   1.102  (* ------------------------------------------------------------------------- *)
   1.103 +(* rawhyps2clausehyps_thm: translates all hyps of the form "~P ==> False" to *)
   1.104 +(*      hyps of the form "P"                                                 *)
   1.105 +(* ------------------------------------------------------------------------- *)
   1.106 +
   1.107 +(* Thm.thm -> Thm.thm *)
   1.108 +
   1.109 +fun rawhyps2clausehyps_thm c =
   1.110 +	fold (fn hyp => fn thm =>
   1.111 +		case hyp of Const ("==>", _) $ (Const ("Trueprop", _) $ (Const ("Not", _) $ P)) $ (Const ("Trueprop", _) $ Const ("False", _)) =>
   1.112 +			let
   1.113 +				val cterm = cterm_of (theory_of_thm thm)
   1.114 +				val thm1  = Thm.implies_intr (cterm hyp) thm  (* hyps |- (~P ==> False) ==> goal *)
   1.115 +				val varP  = Var (("P", 0), HOLogic.boolT)
   1.116 +				val notE  = Thm.instantiate ([], [(cterm varP, cterm P)]) clause2raw_notE  (* P ==> ~P ==> False *)
   1.117 +				val notE' = Thm.implies_elim notE (Thm.assume (cterm (HOLogic.mk_Trueprop P)))  (* P |- ~P ==> False *)
   1.118 +				val thm2  = Thm.implies_elim thm1 notE'  (* hyps, P |- goal *)
   1.119 +			in
   1.120 +				thm2
   1.121 +			end
   1.122 +		          | _                                                                                                                  =>
   1.123 +			thm) (#hyps (rep_thm c)) c;
   1.124 +
   1.125 +(* ------------------------------------------------------------------------- *)
   1.126  (* inst_thm: instantiates a theorem with a list of terms                     *)
   1.127  (* ------------------------------------------------------------------------- *)
   1.128