src/HOL/Tools/cnf_funcs.ML
author wenzelm
Thu Aug 03 17:30:36 2006 +0200 (2006-08-03)
changeset 20328 5b240a4216b0
parent 19236 150e8b0fb991
child 20440 e6fe74eebda3
permissions -rw-r--r--
RuleInsts.bires_inst_tac;
webertj@17618
     1
(*  Title:      HOL/Tools/cnf_funcs.ML
webertj@17618
     2
    ID:         $Id$
webertj@17618
     3
    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
webertj@17809
     4
    Author:     Tjark Weber
webertj@19236
     5
    Copyright   2005-2006
webertj@17618
     6
webertj@17618
     7
  Description:
webertj@17809
     8
  This file contains functions and tactics to transform a formula into
webertj@17809
     9
  Conjunctive Normal Form (CNF).
webertj@17618
    10
  A formula in CNF is of the following form:
webertj@17618
    11
webertj@19236
    12
      (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
webertj@17809
    13
      False
webertj@17809
    14
      True
webertj@17618
    15
webertj@17809
    16
  where each xij is a literal (a positive or negative atomic Boolean term),
webertj@17809
    17
  i.e. the formula is a conjunction of disjunctions of literals, or
webertj@17809
    18
  "False", or "True".
webertj@17809
    19
webertj@17809
    20
  A (non-empty) disjunction of literals is referred to as "clause".
webertj@17618
    21
webertj@17618
    22
  For the purpose of SAT proof reconstruction, we also make use of another
webertj@17618
    23
  representation of clauses, which we call the "raw clauses".
webertj@17618
    24
  Raw clauses are of the form
webertj@17618
    25
webertj@19236
    26
      x1', x2', ..., xn', ~ (x1 | x2 | ... | xn) ==> False |- False ,
webertj@19236
    27
webertj@19236
    28
  where each xi is a literal, and each xi' is the negation normal form of ~xi.
webertj@17618
    29
webertj@19236
    30
  Raw clauses may contain further hyps of the form "~ clause ==> False".
webertj@19236
    31
  Literals are successively removed from the hyps of raw clauses by resolution
webertj@19236
    32
  during SAT proof reconstruction.
webertj@17618
    33
*)
webertj@17618
    34
webertj@17618
    35
signature CNF =
webertj@17618
    36
sig
webertj@17809
    37
	val is_atom           : Term.term -> bool
webertj@17809
    38
	val is_literal        : Term.term -> bool
webertj@17809
    39
	val is_clause         : Term.term -> bool
webertj@17809
    40
	val clause_is_trivial : Term.term -> bool
webertj@17809
    41
webertj@19236
    42
	val clause2raw_thm         : Thm.thm -> Thm.thm
webertj@19236
    43
	val rawhyps2clausehyps_thm : Thm.thm -> Thm.thm
webertj@17618
    44
webertj@17809
    45
	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
webertj@17618
    46
webertj@17809
    47
	val make_cnf_thm  : Theory.theory -> Term.term -> Thm.thm
webertj@17809
    48
	val make_cnfx_thm : Theory.theory -> Term.term ->  Thm.thm
webertj@17809
    49
	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
webertj@17809
    50
	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
webertj@17809
    51
end;
webertj@17618
    52
webertj@17618
    53
structure cnf : CNF =
webertj@17618
    54
struct
webertj@17618
    55
webertj@17809
    56
(* string -> Thm.thm *)
webertj@17618
    57
fun thm_by_auto G =
webertj@17809
    58
	prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
webertj@17618
    59
webertj@17809
    60
(* Thm.thm *)
webertj@17809
    61
val clause2raw_notE      = thm_by_auto "[| P; ~P |] ==> False";
webertj@17809
    62
val clause2raw_not_disj  = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)";
webertj@17809
    63
val clause2raw_not_not   = thm_by_auto "P ==> ~~P";
webertj@17618
    64
webertj@17809
    65
val iff_refl             = thm_by_auto "(P::bool) = P";
webertj@17809
    66
val iff_trans            = thm_by_auto "[| (P::bool) = Q; Q = R |] ==> P = R";
webertj@17809
    67
val conj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')";
webertj@17809
    68
val disj_cong            = thm_by_auto "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')";
webertj@17618
    69
webertj@17809
    70
val make_nnf_imp         = thm_by_auto "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')";
webertj@17809
    71
val make_nnf_iff         = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))";
webertj@17809
    72
val make_nnf_not_false   = thm_by_auto "(~False) = True";
webertj@17809
    73
val make_nnf_not_true    = thm_by_auto "(~True) = False";
webertj@17809
    74
val make_nnf_not_conj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')";
webertj@17809
    75
val make_nnf_not_disj    = thm_by_auto "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')";
webertj@17809
    76
val make_nnf_not_imp     = thm_by_auto "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')";
webertj@17809
    77
val make_nnf_not_iff     = thm_by_auto "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))";
webertj@17809
    78
val make_nnf_not_not     = thm_by_auto "P = P' ==> (~~P) = P'";
webertj@17618
    79
webertj@17809
    80
val simp_TF_conj_True_l  = thm_by_auto "[| P = True; Q = Q' |] ==> (P & Q) = Q'";
webertj@17809
    81
val simp_TF_conj_True_r  = thm_by_auto "[| P = P'; Q = True |] ==> (P & Q) = P'";
webertj@17809
    82
val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False";
webertj@17809
    83
val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False";
webertj@17809
    84
val simp_TF_disj_True_l  = thm_by_auto "P = True ==> (P | Q) = True";
webertj@17809
    85
val simp_TF_disj_True_r  = thm_by_auto "Q = True ==> (P | Q) = True";
webertj@17809
    86
val simp_TF_disj_False_l = thm_by_auto "[| P = False; Q = Q' |] ==> (P | Q) = Q'";
webertj@17809
    87
val simp_TF_disj_False_r = thm_by_auto "[| P = P'; Q = False |] ==> (P | Q) = P'";
webertj@17618
    88
webertj@17809
    89
val make_cnf_disj_conj_l = thm_by_auto "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)";
webertj@17809
    90
val make_cnf_disj_conj_r = thm_by_auto "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)";
webertj@17618
    91
webertj@17809
    92
val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x) | Q) = (EX x. P x | Q)";
webertj@17809
    93
val make_cnfx_disj_ex_r = thm_by_auto "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)";
webertj@17809
    94
val make_cnfx_newlit    = thm_by_auto "(P | Q) = (EX x. (P | x) & (Q | ~x))";
webertj@17809
    95
val make_cnfx_ex_cong   = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)";
webertj@17618
    96
webertj@17809
    97
val weakening_thm        = thm_by_auto "[| P; Q |] ==> Q";
webertj@17618
    98
webertj@17809
    99
val cnftac_eq_imp        = thm_by_auto "[| P = Q; P |] ==> Q";
webertj@17618
   100
webertj@17809
   101
(* Term.term -> bool *)
webertj@17809
   102
fun is_atom (Const ("False", _))                                           = false
webertj@17809
   103
  | is_atom (Const ("True", _))                                            = false
webertj@17809
   104
  | is_atom (Const ("op &", _) $ _ $ _)                                    = false
webertj@17809
   105
  | is_atom (Const ("op |", _) $ _ $ _)                                    = false
webertj@17809
   106
  | is_atom (Const ("op -->", _) $ _ $ _)                                  = false
webertj@17809
   107
  | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
webertj@17809
   108
  | is_atom (Const ("Not", _) $ _)                                         = false
webertj@17809
   109
  | is_atom _                                                              = true;
webertj@17618
   110
webertj@17809
   111
(* Term.term -> bool *)
webertj@17809
   112
fun is_literal (Const ("Not", _) $ x) = is_atom x
webertj@17809
   113
  | is_literal x                      = is_atom x;
webertj@17618
   114
webertj@17809
   115
(* Term.term -> bool *)
webertj@17809
   116
fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
webertj@17809
   117
  | is_clause x                           = is_literal x;
webertj@17618
   118
webertj@17809
   119
(* ------------------------------------------------------------------------- *)
webertj@17809
   120
(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
webertj@17809
   121
(*      and the atom's negation                                              *)
webertj@17809
   122
(* ------------------------------------------------------------------------- *)
webertj@17809
   123
webertj@17809
   124
(* Term.term -> bool *)
webertj@17618
   125
webertj@17809
   126
fun clause_is_trivial c =
webertj@17809
   127
	let
webertj@17809
   128
		(* Term.term -> Term.term list -> Term.term list *)
webertj@17809
   129
		fun collect_literals (Const ("op |", _) $ x $ y) ls = collect_literals x (collect_literals y ls)
webertj@17809
   130
		  | collect_literals x                           ls = x :: ls
webertj@17809
   131
		(* Term.term -> Term.term *)
webertj@17809
   132
		fun dual (Const ("Not", _) $ x) = x
webertj@17809
   133
		  | dual x                      = HOLogic.Not $ x
webertj@17809
   134
		(* Term.term list -> bool *)
webertj@17809
   135
		fun has_duals []      = false
webertj@17809
   136
		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
webertj@17809
   137
	in
webertj@17809
   138
		has_duals (collect_literals c [])
webertj@17809
   139
	end;
webertj@17618
   140
webertj@17809
   141
(* ------------------------------------------------------------------------- *)
webertj@17809
   142
(* clause2raw_thm: translates a clause into a raw clause, i.e.               *)
webertj@19236
   143
(*        ... |- x1 | ... | xn                                               *)
webertj@17809
   144
(*      (where each xi is a literal) is translated to                        *)
webertj@19236
   145
(*        ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False ,               *)
webertj@17809
   146
(*      where each xi' is the negation normal form of ~xi.                   *)
webertj@17809
   147
(* ------------------------------------------------------------------------- *)
webertj@17618
   148
webertj@17809
   149
(* Thm.thm -> Thm.thm *)
webertj@17618
   150
webertj@17809
   151
fun clause2raw_thm c =
webertj@17809
   152
let
webertj@19236
   153
	val disj               = HOLogic.dest_Trueprop (prop_of c)
webertj@19236
   154
	val not_disj_imp_false = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_not disj), HOLogic.mk_Trueprop HOLogic.false_const)
webertj@19236
   155
	val thm1 = Thm.assume (cterm_of (theory_of_thm c) not_disj_imp_false)  (* ~(x1 | ... | xn) ==> False |- ~(x1 | ... | xn) ==> False *)
webertj@17809
   156
	(* eliminates negated disjunctions from the i-th premise, possibly *)
webertj@17809
   157
	(* adding new premises, then continues with the (i+1)-th premise   *)
webertj@17809
   158
	(* Thm.thm -> int -> Thm.thm *)
webertj@17809
   159
	fun not_disj_to_prem thm i =
webertj@17809
   160
		if i > nprems_of thm then
webertj@17809
   161
			thm
webertj@17809
   162
		else
webertj@17809
   163
			not_disj_to_prem (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) (i+1)
webertj@19236
   164
	val thm2 = not_disj_to_prem thm1 1  (* ~(x1 | ... | xn) ==> False |- ~x1 ==> ... ==> ~xn ==> False *)
webertj@19236
   165
	val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2)  (* ~(x1 | ... | xn) ==> False |- x1' ==> ... ==> xn' ==> False *)
webertj@19236
   166
	val thy3 = theory_of_thm thm3
webertj@19236
   167
	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 *)
webertj@17809
   168
in
webertj@19236
   169
	thm4
webertj@17809
   170
end;
webertj@17618
   171
webertj@17809
   172
(* ------------------------------------------------------------------------- *)
webertj@19236
   173
(* rawhyps2clausehyps_thm: translates all hyps of the form "~P ==> False" to *)
webertj@19236
   174
(*      hyps of the form "P"                                                 *)
webertj@19236
   175
(* ------------------------------------------------------------------------- *)
webertj@19236
   176
webertj@19236
   177
(* Thm.thm -> Thm.thm *)
webertj@19236
   178
webertj@19236
   179
fun rawhyps2clausehyps_thm c =
webertj@19236
   180
	fold (fn hyp => fn thm =>
webertj@19236
   181
		case hyp of Const ("==>", _) $ (Const ("Trueprop", _) $ (Const ("Not", _) $ P)) $ (Const ("Trueprop", _) $ Const ("False", _)) =>
webertj@19236
   182
			let
webertj@19236
   183
				val cterm = cterm_of (theory_of_thm thm)
webertj@19236
   184
				val thm1  = Thm.implies_intr (cterm hyp) thm  (* hyps |- (~P ==> False) ==> goal *)
webertj@19236
   185
				val varP  = Var (("P", 0), HOLogic.boolT)
webertj@19236
   186
				val notE  = Thm.instantiate ([], [(cterm varP, cterm P)]) clause2raw_notE  (* P ==> ~P ==> False *)
webertj@19236
   187
				val notE' = Thm.implies_elim notE (Thm.assume (cterm (HOLogic.mk_Trueprop P)))  (* P |- ~P ==> False *)
webertj@19236
   188
				val thm2  = Thm.implies_elim thm1 notE'  (* hyps, P |- goal *)
webertj@19236
   189
			in
webertj@19236
   190
				thm2
webertj@19236
   191
			end
webertj@19236
   192
		          | _                                                                                                                  =>
webertj@19236
   193
			thm) (#hyps (rep_thm c)) c;
webertj@19236
   194
webertj@19236
   195
(* ------------------------------------------------------------------------- *)
webertj@17809
   196
(* inst_thm: instantiates a theorem with a list of terms                     *)
webertj@17809
   197
(* ------------------------------------------------------------------------- *)
webertj@17618
   198
webertj@17809
   199
(* Theory.theory -> Term.term list -> Thm.thm -> Thm.thm *)
webertj@17618
   200
webertj@17809
   201
fun inst_thm thy ts thm =
webertj@17809
   202
	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
webertj@17618
   203
webertj@17809
   204
(* ------------------------------------------------------------------------- *)
webertj@17809
   205
(*                         Naive CNF transformation                          *)
webertj@17809
   206
(* ------------------------------------------------------------------------- *)
webertj@17618
   207
webertj@17809
   208
(* ------------------------------------------------------------------------- *)
webertj@17809
   209
(* make_nnf_thm: produces a theorem of the form t = t', where t' is the      *)
webertj@17809
   210
(*      negation normal form (i.e. negation only occurs in front of atoms)   *)
webertj@17809
   211
(*      of t; implications ("-->") and equivalences ("=" on bool) are        *)
webertj@17809
   212
(*      eliminated (possibly causing an exponential blowup)                  *)
webertj@17809
   213
(* ------------------------------------------------------------------------- *)
webertj@17809
   214
webertj@17809
   215
(* Theory.theory -> Term.term -> Thm.thm *)
webertj@17618
   216
webertj@17809
   217
fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
webertj@17809
   218
	let
webertj@17809
   219
		val thm1 = make_nnf_thm thy x
webertj@17809
   220
		val thm2 = make_nnf_thm thy y
webertj@17809
   221
	in
webertj@17809
   222
		conj_cong OF [thm1, thm2]
webertj@17809
   223
	end
webertj@17809
   224
  | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
webertj@17809
   225
	let
webertj@17809
   226
		val thm1 = make_nnf_thm thy x
webertj@17809
   227
		val thm2 = make_nnf_thm thy y
webertj@17809
   228
	in
webertj@17809
   229
		disj_cong OF [thm1, thm2]
webertj@17809
   230
	end
webertj@17809
   231
  | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
webertj@17809
   232
	let
webertj@17809
   233
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
webertj@17809
   234
		val thm2 = make_nnf_thm thy y
webertj@17809
   235
	in
webertj@17809
   236
		make_nnf_imp OF [thm1, thm2]
webertj@17809
   237
	end
webertj@17809
   238
  | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
webertj@17809
   239
	let
webertj@17809
   240
		val thm1 = make_nnf_thm thy x
webertj@17809
   241
		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
webertj@17809
   242
		val thm3 = make_nnf_thm thy y
webertj@17809
   243
		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
webertj@17809
   244
	in
webertj@17809
   245
		make_nnf_iff OF [thm1, thm2, thm3, thm4]
webertj@17809
   246
	end
webertj@17809
   247
  | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
webertj@17809
   248
	make_nnf_not_false
webertj@17809
   249
  | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
webertj@17809
   250
	make_nnf_not_true
webertj@17809
   251
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
webertj@17809
   252
	let
webertj@17809
   253
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
webertj@17809
   254
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
webertj@17809
   255
	in
webertj@17809
   256
		make_nnf_not_conj OF [thm1, thm2]
webertj@17809
   257
	end
webertj@17809
   258
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
webertj@17809
   259
	let
webertj@17809
   260
		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
webertj@17809
   261
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
webertj@17809
   262
	in
webertj@17809
   263
		make_nnf_not_disj OF [thm1, thm2]
webertj@17809
   264
	end
webertj@17809
   265
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
webertj@17809
   266
	let
webertj@17809
   267
		val thm1 = make_nnf_thm thy x
webertj@17809
   268
		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
webertj@17809
   269
	in
webertj@17809
   270
		make_nnf_not_imp OF [thm1, thm2]
webertj@17809
   271
	end
webertj@17809
   272
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
webertj@17809
   273
	let
webertj@17809
   274
		val thm1 = make_nnf_thm thy x
webertj@17809
   275
		val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
webertj@17809
   276
		val thm3 = make_nnf_thm thy y
webertj@17809
   277
		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
webertj@17809
   278
	in
webertj@17809
   279
		make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
webertj@17809
   280
	end
webertj@17809
   281
  | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
webertj@17809
   282
	let
webertj@17809
   283
		val thm1 = make_nnf_thm thy x
webertj@17809
   284
	in
webertj@17809
   285
		make_nnf_not_not OF [thm1]
webertj@17809
   286
	end
webertj@17809
   287
  | make_nnf_thm thy t =
webertj@17809
   288
	inst_thm thy [t] iff_refl;
webertj@17618
   289
webertj@17809
   290
(* ------------------------------------------------------------------------- *)
webertj@17809
   291
(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
webertj@17809
   292
(*      t, but simplified wrt. the following theorems:                       *)
webertj@17809
   293
(*        (True & x) = x                                                     *)
webertj@17809
   294
(*        (x & True) = x                                                     *)
webertj@17809
   295
(*        (False & x) = False                                                *)
webertj@17809
   296
(*        (x & False) = False                                                *)
webertj@17809
   297
(*        (True | x) = True                                                  *)
webertj@17809
   298
(*        (x | True) = True                                                  *)
webertj@17809
   299
(*        (False | x) = x                                                    *)
webertj@17809
   300
(*        (x | False) = x                                                    *)
webertj@17809
   301
(*      No simplification is performed below connectives other than & and |. *)
webertj@17809
   302
(*      Optimization: The right-hand side of a conjunction (disjunction) is  *)
webertj@17809
   303
(*      simplified only if the left-hand side does not simplify to False     *)
webertj@17809
   304
(*      (True, respectively).                                                *)
webertj@17809
   305
(* ------------------------------------------------------------------------- *)
webertj@17618
   306
webertj@17809
   307
(* Theory.theory -> Term.term -> Thm.thm *)
webertj@17618
   308
webertj@17809
   309
fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
webertj@17809
   310
	let
webertj@17809
   311
		val thm1 = simp_True_False_thm thy x
webertj@17809
   312
		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
webertj@17809
   313
	in
webertj@17809
   314
		if x' = HOLogic.false_const then
webertj@17809
   315
			simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
webertj@17809
   316
		else
webertj@17809
   317
			let
webertj@17809
   318
				val thm2 = simp_True_False_thm thy y
webertj@17809
   319
				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
webertj@17809
   320
			in
webertj@17809
   321
				if x' = HOLogic.true_const then
webertj@17809
   322
					simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
webertj@17809
   323
				else if y' = HOLogic.false_const then
webertj@17809
   324
					simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
webertj@17809
   325
				else if y' = HOLogic.true_const then
webertj@17809
   326
					simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
webertj@17809
   327
				else
webertj@17809
   328
					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
webertj@17809
   329
			end
webertj@17809
   330
	end
webertj@17809
   331
  | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
webertj@17809
   332
	let
webertj@17809
   333
		val thm1 = simp_True_False_thm thy x
webertj@17809
   334
		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
webertj@17809
   335
	in
webertj@17809
   336
		if x' = HOLogic.true_const then
webertj@17809
   337
			simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
webertj@17809
   338
		else
webertj@17809
   339
			let
webertj@17809
   340
				val thm2 = simp_True_False_thm thy y
webertj@17809
   341
				val y'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
webertj@17809
   342
			in
webertj@17809
   343
				if x' = HOLogic.false_const then
webertj@17809
   344
					simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
webertj@17809
   345
				else if y' = HOLogic.true_const then
webertj@17809
   346
					simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
webertj@17809
   347
				else if y' = HOLogic.false_const then
webertj@17809
   348
					simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
webertj@17809
   349
				else
webertj@17809
   350
					disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
webertj@17809
   351
			end
webertj@17809
   352
	end
webertj@17809
   353
  | simp_True_False_thm thy t =
webertj@17809
   354
	inst_thm thy [t] iff_refl;  (* t = t *)
webertj@17618
   355
webertj@17809
   356
(* ------------------------------------------------------------------------- *)
webertj@17809
   357
(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
webertj@17809
   358
(*      is in conjunction normal form.  May cause an exponential blowup      *)
webertj@17809
   359
(*      in the length of the term.                                           *)
webertj@17809
   360
(* ------------------------------------------------------------------------- *)
webertj@17618
   361
webertj@17809
   362
(* Theory.theory -> Term.term -> Thm.thm *)
webertj@17618
   363
webertj@17809
   364
fun make_cnf_thm thy t =
webertj@17809
   365
let
webertj@17809
   366
	(* Term.term -> Thm.thm *)
webertj@17809
   367
	fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
webertj@17809
   368
		let
webertj@17809
   369
			val thm1 = make_cnf_thm_from_nnf x
webertj@17809
   370
			val thm2 = make_cnf_thm_from_nnf y
webertj@17809
   371
		in
webertj@17809
   372
			conj_cong OF [thm1, thm2]
webertj@17809
   373
		end
webertj@17809
   374
	  | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
webertj@17809
   375
		let
webertj@17809
   376
			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
webertj@17809
   377
			fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
webertj@17809
   378
				let
webertj@17809
   379
					val thm1 = make_cnf_disj_thm x1 y'
webertj@17809
   380
					val thm2 = make_cnf_disj_thm x2 y'
webertj@17809
   381
				in
webertj@17809
   382
					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
webertj@17809
   383
				end
webertj@17809
   384
			  | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
webertj@17809
   385
				let
webertj@17809
   386
					val thm1 = make_cnf_disj_thm x' y1
webertj@17809
   387
					val thm2 = make_cnf_disj_thm x' y2
webertj@17809
   388
				in
webertj@17809
   389
					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
webertj@17809
   390
				end
webertj@17809
   391
			  | make_cnf_disj_thm x' y' =
webertj@17809
   392
				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
webertj@17809
   393
			val thm1     = make_cnf_thm_from_nnf x
webertj@17809
   394
			val thm2     = make_cnf_thm_from_nnf y
webertj@17809
   395
			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
webertj@17809
   396
			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
webertj@17809
   397
			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
webertj@17809
   398
		in
webertj@17809
   399
			iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
webertj@17809
   400
		end
webertj@17809
   401
	  | make_cnf_thm_from_nnf t =
webertj@17809
   402
		inst_thm thy [t] iff_refl
webertj@17809
   403
	(* convert 't' to NNF first *)
webertj@17809
   404
	val nnf_thm  = make_nnf_thm thy t
webertj@17809
   405
	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
webertj@17809
   406
	(* then simplify wrt. True/False (this should preserve NNF) *)
webertj@17809
   407
	val simp_thm = simp_True_False_thm thy nnf
webertj@17809
   408
	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
webertj@17809
   409
	(* finally, convert to CNF (this should preserve the simplification) *)
webertj@17809
   410
	val cnf_thm  = make_cnf_thm_from_nnf simp
webertj@17618
   411
in
webertj@17809
   412
	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
webertj@17809
   413
end;
webertj@17618
   414
webertj@17809
   415
(* ------------------------------------------------------------------------- *)
webertj@17809
   416
(*            CNF transformation by introducing new literals                 *)
webertj@17809
   417
(* ------------------------------------------------------------------------- *)
webertj@17618
   418
webertj@17809
   419
(* ------------------------------------------------------------------------- *)
webertj@17809
   420
(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where   *)
webertj@17809
   421
(*      t' is almost in conjunction normal form, except that conjunctions    *)
webertj@17809
   422
(*      and existential quantifiers may be nested.  (Use e.g. 'REPEAT_DETERM *)
webertj@17809
   423
(*      (etac exE i ORELSE etac conjE i)' afterwards to normalize.)  May     *)
webertj@17809
   424
(*      introduce new (existentially bound) literals.  Note: the current     *)
webertj@17809
   425
(*      implementation calls 'make_nnf_thm', causing an exponential blowup   *)
webertj@17809
   426
(*      in the case of nested equivalences.                                  *)
webertj@17809
   427
(* ------------------------------------------------------------------------- *)
webertj@17618
   428
webertj@17809
   429
(* Theory.theory -> Term.term -> Thm.thm *)
webertj@17618
   430
webertj@17809
   431
fun make_cnfx_thm thy t =
webertj@17809
   432
let
webertj@17809
   433
	val var_id = ref 0  (* properly initialized below *)
webertj@17809
   434
	(* unit -> Term.term *)
webertj@17809
   435
	fun new_free () =
webertj@17809
   436
		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
webertj@17809
   437
	(* Term.term -> Thm.thm *)
webertj@17809
   438
	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
webertj@17809
   439
		let
webertj@17809
   440
			val thm1 = make_cnfx_thm_from_nnf x
webertj@17809
   441
			val thm2 = make_cnfx_thm_from_nnf y
webertj@17809
   442
		in
webertj@17809
   443
			conj_cong OF [thm1, thm2]
webertj@17809
   444
		end
webertj@17809
   445
	  | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
webertj@17809
   446
		if is_clause x andalso is_clause y then
webertj@17809
   447
			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
webertj@17809
   448
		else if is_literal y orelse is_literal x then let
webertj@17809
   449
			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
webertj@17809
   450
			(* almost in CNF, and x' or y' is a literal                      *)
webertj@17809
   451
			fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
webertj@17809
   452
				let
webertj@17809
   453
					val thm1 = make_cnfx_disj_thm x1 y'
webertj@17809
   454
					val thm2 = make_cnfx_disj_thm x2 y'
webertj@17809
   455
				in
webertj@17809
   456
					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
webertj@17809
   457
				end
webertj@17809
   458
			  | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
webertj@17809
   459
				let
webertj@17809
   460
					val thm1 = make_cnfx_disj_thm x' y1
webertj@17809
   461
					val thm2 = make_cnfx_disj_thm x' y2
webertj@17809
   462
				in
webertj@17809
   463
					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
webertj@17809
   464
				end
webertj@17809
   465
			  | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
webertj@17809
   466
				let
webertj@17809
   467
					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l   (* ((Ex x') | y') = (Ex (x' | y')) *)
webertj@17809
   468
					val var  = new_free ()
webertj@17809
   469
					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
webertj@17809
   470
					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
webertj@17809
   471
					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
webertj@17809
   472
					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
webertj@17809
   473
				in
webertj@17809
   474
					iff_trans OF [thm1, thm5]  (* ((Ex x') | y') = (Ex v. body') *)
webertj@17809
   475
				end
webertj@17809
   476
			  | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
webertj@17809
   477
				let
webertj@17809
   478
					val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r   (* (x' | (Ex y')) = (Ex (x' | y')) *)
webertj@17809
   479
					val var  = new_free ()
webertj@17809
   480
					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
webertj@17809
   481
					val thm3 = forall_intr (cterm_of thy var) thm2         (* !!v. (x' | y') = body' *)
webertj@17809
   482
					val thm4 = strip_shyps (thm3 COMP allI)                (* ALL v. (x' | y') = body' *)
webertj@17809
   483
					val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)     (* (EX v. (x' | y')) = (EX v. body') *)
webertj@17809
   484
				in
webertj@17809
   485
					iff_trans OF [thm1, thm5]  (* (x' | (Ex y')) = (EX v. body') *)
webertj@17809
   486
				end
webertj@17809
   487
			  | make_cnfx_disj_thm x' y' =
webertj@17809
   488
				inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl  (* (x' | y') = (x' | y') *)
webertj@17809
   489
			val thm1     = make_cnfx_thm_from_nnf x
webertj@17809
   490
			val thm2     = make_cnfx_thm_from_nnf y
webertj@17809
   491
			val x'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
webertj@17809
   492
			val y'       = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
webertj@17809
   493
			val disj_thm = disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
webertj@17809
   494
		in
webertj@17809
   495
			iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
webertj@17809
   496
		end else let  (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
webertj@17809
   497
			val thm1 = inst_thm thy [x, y] make_cnfx_newlit     (* (x | y) = EX v. (x | v) & (y | ~v) *)
webertj@17809
   498
			val var  = new_free ()
webertj@17809
   499
			val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
webertj@17809
   500
			val thm2 = make_cnfx_thm_from_nnf body              (* (x | v) & (y | ~v) = body' *)
webertj@17809
   501
			val thm3 = forall_intr (cterm_of thy var) thm2      (* !!v. (x | v) & (y | ~v) = body' *)
webertj@17809
   502
			val thm4 = strip_shyps (thm3 COMP allI)             (* ALL v. (x | v) & (y | ~v) = body' *)
webertj@17809
   503
			val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong)  (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
webertj@17809
   504
		in
webertj@17809
   505
			iff_trans OF [thm1, thm5]
webertj@17809
   506
		end
webertj@17809
   507
	  | make_cnfx_thm_from_nnf t =
webertj@17809
   508
		inst_thm thy [t] iff_refl
webertj@17809
   509
	(* convert 't' to NNF first *)
webertj@17809
   510
	val nnf_thm  = make_nnf_thm thy t
webertj@17809
   511
	val nnf      = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
webertj@17809
   512
	(* then simplify wrt. True/False (this should preserve NNF) *)
webertj@17809
   513
	val simp_thm = simp_True_False_thm thy nnf
webertj@17809
   514
	val simp     = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
webertj@17809
   515
	(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
webertj@17809
   516
	val _        = (var_id := fold (fn free => fn max =>
webertj@17809
   517
		let
webertj@17809
   518
			val (name, _) = dest_Free free
webertj@17809
   519
			val idx       = if String.isPrefix "cnfx_" name then
webertj@17809
   520
					(Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
webertj@17809
   521
				else
webertj@17809
   522
					NONE
webertj@17809
   523
		in
webertj@17809
   524
			Int.max (max, getOpt (idx, 0))
webertj@17809
   525
		end) (term_frees simp) 0)
webertj@17809
   526
	(* finally, convert to definitional CNF (this should preserve the simplification) *)
webertj@17809
   527
	val cnfx_thm = make_cnfx_thm_from_nnf simp
webertj@17809
   528
in
webertj@17809
   529
	iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
webertj@17809
   530
end;
webertj@17618
   531
webertj@17809
   532
(* ------------------------------------------------------------------------- *)
webertj@17809
   533
(*                                  Tactics                                  *)
webertj@17809
   534
(* ------------------------------------------------------------------------- *)
webertj@17618
   535
webertj@17809
   536
(* ------------------------------------------------------------------------- *)
webertj@17809
   537
(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
webertj@17809
   538
(* ------------------------------------------------------------------------- *)
webertj@17618
   539
webertj@17809
   540
(* int -> Tactical.tactic *)
webertj@17618
   541
webertj@17809
   542
fun weakening_tac i =
webertj@17809
   543
	dtac weakening_thm i THEN atac (i+1);
webertj@17618
   544
webertj@17809
   545
(* ------------------------------------------------------------------------- *)
webertj@17809
   546
(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
webertj@17809
   547
(*      (possibly causing an exponential blowup in the length of each        *)
webertj@17809
   548
(*      premise)                                                             *)
webertj@17809
   549
(* ------------------------------------------------------------------------- *)
webertj@17618
   550
webertj@17809
   551
(* int -> Tactical.tactic *)
webertj@17618
   552
webertj@17809
   553
fun cnf_rewrite_tac i =
webertj@17809
   554
	(* cut the CNF formulas as new premises *)
webertj@17809
   555
	METAHYPS (fn prems =>
webertj@17809
   556
		let
webertj@17809
   557
			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
webertj@17809
   558
			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
webertj@17809
   559
		in
webertj@17809
   560
			cut_facts_tac cut_thms 1
webertj@17809
   561
		end) i
webertj@17809
   562
	(* remove the original premises *)
webertj@17809
   563
	THEN SELECT_GOAL (fn thm =>
webertj@17809
   564
		let
webertj@17809
   565
			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
webertj@17809
   566
		in
webertj@17809
   567
			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
webertj@17809
   568
		end) i;
webertj@17618
   569
webertj@17809
   570
(* ------------------------------------------------------------------------- *)
webertj@17809
   571
(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF      *)
webertj@17809
   572
(*      (possibly introducing new literals)                                  *)
webertj@17809
   573
(* ------------------------------------------------------------------------- *)
webertj@17809
   574
webertj@17809
   575
(* int -> Tactical.tactic *)
webertj@17618
   576
webertj@17809
   577
fun cnfx_rewrite_tac i =
webertj@17809
   578
	(* cut the CNF formulas as new premises *)
webertj@17809
   579
	METAHYPS (fn prems =>
webertj@17809
   580
		let
webertj@17809
   581
			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
webertj@17809
   582
			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
webertj@17809
   583
		in
webertj@17809
   584
			cut_facts_tac cut_thms 1
webertj@17809
   585
		end) i
webertj@17809
   586
	(* remove the original premises *)
webertj@17809
   587
	THEN SELECT_GOAL (fn thm =>
webertj@17809
   588
		let
webertj@17809
   589
			val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm, 0)
webertj@17809
   590
		in
webertj@17809
   591
			PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
webertj@17809
   592
		end) i;
webertj@17618
   593
webertj@17809
   594
end;  (* of structure *)