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