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.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
```