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