src/HOL/Tools/cnf_funcs.ML
author webertj
Fri Sep 23 22:58:50 2005 +0200 (2005-09-23)
changeset 17618 1330157e156a
child 17809 195045659c06
permissions -rw-r--r--
new sat tactic imports resolution proofs from zChaff
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@17618
     4
    Copyright   2005
webertj@17618
     5
webertj@17618
     6
  Description:
webertj@17618
     7
  This file contains functions and tactics to transform a formula into 
webertj@17618
     8
  Conjunctive Normal Forms (CNF). 
webertj@17618
     9
  A formula in CNF is of the following form:
webertj@17618
    10
webertj@17618
    11
      (x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
webertj@17618
    12
webertj@17618
    13
  where each xij is a literal (i.e., positive or negative propositional
webertj@17618
    14
  variables).
webertj@17618
    15
  This kind of formula will simply be referred to as CNF.
webertj@17618
    16
  A disjunction of literals is referred to as "clause".
webertj@17618
    17
webertj@17618
    18
  For the purpose of SAT proof reconstruction, we also make use of another
webertj@17618
    19
  representation of clauses, which we call the "raw clauses".
webertj@17618
    20
  Raw clauses are of the form
webertj@17618
    21
webertj@17618
    22
      (x1 ==> x2 ==> .. ==> xn ==> False)
webertj@17618
    23
webertj@17618
    24
  where each xi is a literal. Note that the above raw clause corresponds
webertj@17618
    25
  to the clause (x1' | ... | xn'), where each xi' is the negation normal
webertj@17618
    26
  form of ~xi.
webertj@17618
    27
webertj@17618
    28
  Notes for current revision:
webertj@17618
    29
  - the "definitional CNF transformation" (anything with prefix cnfx_ )
webertj@17618
    30
    introduces new literals of the form (lit_i) where i is an integer.
webertj@17618
    31
    For these functions to work, it is necessary that no free variables
webertj@17618
    32
    which names are of the form lit_i appears in the formula being
webertj@17618
    33
    transformed.
webertj@17618
    34
*)
webertj@17618
    35
webertj@17618
    36
webertj@17618
    37
(***************************************************************************)
webertj@17618
    38
webertj@17618
    39
signature CNF =
webertj@17618
    40
sig
webertj@17618
    41
  val cnf_tac : Tactical.tactic
webertj@17618
    42
  val cnf_thin_tac : Tactical.tactic
webertj@17618
    43
  val cnfx_thin_tac : Tactical.tactic
webertj@17618
    44
  val cnf_concl_tac : Tactical.tactic
webertj@17618
    45
  val weakening_tac : int -> Tactical.tactic
webertj@17618
    46
  val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
webertj@17618
    47
  val mk_cnfx_thm : Sign.sg -> Term.term ->  Thm.thm
webertj@17618
    48
  val is_atm : Term.term -> bool
webertj@17618
    49
  val is_lit : Term.term -> bool
webertj@17618
    50
  val is_clause : Term.term -> bool
webertj@17618
    51
  val is_raw_clause : Term.term -> bool
webertj@17618
    52
  val cnf2raw_thm : Thm.thm -> Thm.thm
webertj@17618
    53
  val cnf2raw_thms : Thm.thm list -> Thm.thm list
webertj@17618
    54
  val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
webertj@17618
    55
end
webertj@17618
    56
webertj@17618
    57
webertj@17618
    58
(***************************************************************************)
webertj@17618
    59
webertj@17618
    60
structure cnf : CNF =
webertj@17618
    61
struct
webertj@17618
    62
webertj@17618
    63
val cur_thy = the_context();
webertj@17618
    64
val mk_disj = HOLogic.mk_disj;
webertj@17618
    65
val mk_conj = HOLogic.mk_conj;
webertj@17618
    66
val mk_imp  = HOLogic.mk_imp;
webertj@17618
    67
val Not = HOLogic.Not;
webertj@17618
    68
val false_const = HOLogic.false_const;
webertj@17618
    69
val true_const = HOLogic.true_const;
webertj@17618
    70
webertj@17618
    71
webertj@17618
    72
(* Index for new literals *)
webertj@17618
    73
val lit_id = ref 0;
webertj@17618
    74
webertj@17618
    75
fun thm_by_auto G =
webertj@17618
    76
    prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
webertj@17618
    77
webertj@17618
    78
(***************************************************************************)
webertj@17618
    79
webertj@17618
    80
webertj@17618
    81
val cnf_eq_id = thm_by_auto "(P :: bool) = P";
webertj@17618
    82
webertj@17618
    83
val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
webertj@17618
    84
webertj@17618
    85
val cnf_not_true_false = thm_by_auto "~True = False";
webertj@17618
    86
webertj@17618
    87
val cnf_not_false_true = thm_by_auto "~False = True";
webertj@17618
    88
webertj@17618
    89
val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
webertj@17618
    90
webertj@17618
    91
val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
webertj@17618
    92
webertj@17618
    93
val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
webertj@17618
    94
webertj@17618
    95
val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
webertj@17618
    96
webertj@17618
    97
val cnf_double_neg = thm_by_auto "(~~P) = P";
webertj@17618
    98
 
webertj@17618
    99
val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
webertj@17618
   100
webertj@17618
   101
val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
webertj@17618
   102
webertj@17618
   103
val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
webertj@17618
   104
webertj@17618
   105
val cnf_disj_false = thm_by_auto "(False | P) = P";
webertj@17618
   106
webertj@17618
   107
val cnf_disj_true = thm_by_auto "(True | P) = True";
webertj@17618
   108
webertj@17618
   109
val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
webertj@17618
   110
webertj@17618
   111
val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
webertj@17618
   112
webertj@17618
   113
val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
webertj@17618
   114
webertj@17618
   115
val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
webertj@17618
   116
webertj@17618
   117
val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
webertj@17618
   118
webertj@17618
   119
val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
webertj@17618
   120
webertj@17618
   121
val icnf_elim_disj1 = thm_by_auto "Q = R  ==> (~P | Q) = (P --> R)";
webertj@17618
   122
webertj@17618
   123
val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
webertj@17618
   124
webertj@17618
   125
val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
webertj@17618
   126
webertj@17618
   127
val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
webertj@17618
   128
webertj@17618
   129
val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
webertj@17618
   130
webertj@17618
   131
val cnf_newlit = thm_by_auto 
webertj@17618
   132
    "((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
webertj@17618
   133
webertj@17618
   134
val cnf_all_ex = thm_by_auto 
webertj@17618
   135
    "(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
webertj@17618
   136
webertj@17618
   137
(* [| P ; ~P |] ==> False *)
webertj@17618
   138
val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
webertj@17618
   139
webertj@17618
   140
val cnf_dneg = thm_by_auto "P ==> ~~P";
webertj@17618
   141
webertj@17618
   142
val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
webertj@17618
   143
webertj@17618
   144
val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
webertj@17618
   145
webertj@17618
   146
(***************************************************************************)
webertj@17618
   147
webertj@17618
   148
fun is_atm (Const("Trueprop",_) $ x) = is_atm x
webertj@17618
   149
  | is_atm (Const("==>",_) $ x $ y) = false
webertj@17618
   150
  | is_atm (Const("False",_)) = false
webertj@17618
   151
  | is_atm (Const("True", _)) = false
webertj@17618
   152
  | is_atm (Const("op &",_) $ x $ y) = false
webertj@17618
   153
  | is_atm (Const("op |",_) $ x $ y) = false
webertj@17618
   154
  | is_atm (Const("op -->",_) $ x $ y) = false
webertj@17618
   155
  | is_atm (Const("Not",_) $ x) = false
webertj@17618
   156
  | is_atm t = true
webertj@17618
   157
webertj@17618
   158
webertj@17618
   159
fun is_lit (Const("Trueprop",_) $ x) = is_lit x
webertj@17618
   160
  | is_lit (Const("Not", _) $ x) = is_atm x
webertj@17618
   161
  | is_lit t = is_atm t
webertj@17618
   162
webertj@17618
   163
fun is_clause (Const("Trueprop",_) $ x) = is_clause x
webertj@17618
   164
  | is_clause (Const("op |", _) $ x $ y) = 
webertj@17618
   165
          (is_clause x) andalso (is_clause y)
webertj@17618
   166
  | is_clause t = is_lit t
webertj@17618
   167
webertj@17618
   168
fun is_cnf (Const("Trueprop", _) $ x) = is_cnf x
webertj@17618
   169
  | is_cnf (Const("op &",_) $ x $ y) = (is_cnf x) andalso (is_cnf y)
webertj@17618
   170
  | is_cnf t = is_clause t
webertj@17618
   171
webertj@17618
   172
webertj@17618
   173
(* Checking for raw clauses *)
webertj@17618
   174
fun is_raw_clause (Const("Trueprop",_) $ x) = is_raw_clause x
webertj@17618
   175
  | is_raw_clause (Const("==>",_) $ x $ 
webertj@17618
   176
                   (Const("Trueprop",_) $ Const("False",_))) = is_lit x
webertj@17618
   177
  | is_raw_clause (Const("==>",_) $ x $ y) = 
webertj@17618
   178
        (is_lit x) andalso (is_raw_clause y)
webertj@17618
   179
  | is_raw_clause t = false
webertj@17618
   180
webertj@17618
   181
webertj@17618
   182
webertj@17618
   183
(* Translate a CNF clause into a raw clause *)
webertj@17618
   184
fun cnf2raw_thm c =
webertj@17618
   185
let val nc = c RS cnf_notE
webertj@17618
   186
in
webertj@17618
   187
rule_by_tactic (REPEAT_SOME (fn i => 
webertj@17618
   188
               rtac cnf_dneg i 
webertj@17618
   189
               ORELSE rtac cnf_neg_disjI i)) nc
webertj@17618
   190
handle THM _ => nc
webertj@17618
   191
end
webertj@17618
   192
webertj@17618
   193
fun cnf2raw_thms nil = nil
webertj@17618
   194
  | cnf2raw_thms (c::l) =
webertj@17618
   195
    let val t = term_of (cprop_of c)
webertj@17618
   196
    in
webertj@17618
   197
       if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
webertj@17618
   198
       else cnf2raw_thms l
webertj@17618
   199
    end
webertj@17618
   200
webertj@17618
   201
webertj@17618
   202
(* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
webertj@17618
   203
   association list, relating literals to their indices *)
webertj@17618
   204
webertj@17618
   205
local
webertj@17618
   206
  (* maps atomic formulas to variable numbers *)
webertj@17618
   207
  val dictionary : ((Term.term * int) list) ref = ref nil;
webertj@17618
   208
  val var_count = ref 0;
webertj@17618
   209
  val pAnd = PropLogic.And;
webertj@17618
   210
  val pOr = PropLogic.Or;
webertj@17618
   211
  val pNot = PropLogic.Not;
webertj@17618
   212
  val pFalse = PropLogic.False;
webertj@17618
   213
  val pTrue = PropLogic.True;
webertj@17618
   214
  val pVar = PropLogic.BoolVar;
webertj@17618
   215
webertj@17618
   216
  fun mk_clause (Const("Trueprop",_) $ x) = mk_clause x
webertj@17618
   217
    | mk_clause (Const("op |",_) $ x $ y) = pOr(mk_clause x, mk_clause y)
webertj@17618
   218
    | mk_clause (Const("Not", _) $ x) = pNot (mk_clause x)
webertj@17618
   219
    | mk_clause (Const("True",_)) = pTrue
webertj@17618
   220
    | mk_clause (Const("False",_)) = pFalse
webertj@17618
   221
    | mk_clause t =
webertj@17618
   222
      let
webertj@17618
   223
         val idx = AList.lookup op= (!dictionary) t
webertj@17618
   224
      in
webertj@17618
   225
         case idx of
webertj@17618
   226
            (SOME x) => pVar x
webertj@17618
   227
           | NONE =>
webertj@17618
   228
             let
webertj@17618
   229
                val new_var = inc var_count
webertj@17618
   230
             in
webertj@17618
   231
                dictionary := (t, new_var) :: (!dictionary);
webertj@17618
   232
                pVar new_var
webertj@17618
   233
             end
webertj@17618
   234
      end
webertj@17618
   235
webertj@17618
   236
   fun mk_clauses nil = pTrue
webertj@17618
   237
     | mk_clauses (x::nil) = mk_clause x
webertj@17618
   238
     | mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
webertj@17618
   239
webertj@17618
   240
in
webertj@17618
   241
   fun cnf2prop thms =
webertj@17618
   242
   (
webertj@17618
   243
     var_count := 0;
webertj@17618
   244
     dictionary := nil;
webertj@17618
   245
     (mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
webertj@17618
   246
   )
webertj@17618
   247
end
webertj@17618
   248
webertj@17618
   249
webertj@17618
   250
webertj@17618
   251
(* Instantiate a theorem with a list of terms *)
webertj@17618
   252
fun inst_thm sign l thm = 
webertj@17618
   253
  instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
webertj@17618
   254
webertj@17618
   255
(* Tactic to remove the first hypothesis of the first subgoal. *) 
webertj@17618
   256
fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
webertj@17618
   257
webertj@17618
   258
(* Tactic for removing the n first hypotheses of the first subgoal. *)
webertj@17618
   259
fun weakenings_tac 0 state = all_tac state
webertj@17618
   260
  | weakenings_tac n state = ((weakening_tac  1) THEN (weakenings_tac (n-1))) state
webertj@17618
   261
webertj@17618
   262
webertj@17618
   263
(* 
webertj@17618
   264
  Transform a formula into a "head" negation normal form, that is, 
webertj@17618
   265
  the top level connective is not a negation, with the exception
webertj@17618
   266
  of negative literals. Returns the pair of the head normal term with
webertj@17618
   267
  the theorem corresponding to the transformation.
webertj@17618
   268
*)
webertj@17618
   269
fun head_nnf sign (Const("Not",_)  $ (Const("op &",_) $ x $ y)) =
webertj@17618
   270
    let val t = mk_disj(Not $ x, Not $ y)
webertj@17618
   271
        val neg_thm = inst_thm sign [x, y] cnf_neg_conj 
webertj@17618
   272
    in
webertj@17618
   273
        (t, neg_thm)
webertj@17618
   274
    end
webertj@17618
   275
webertj@17618
   276
  | head_nnf sign (Const("Not", _) $ (Const("op |",_) $ x $ y)) =
webertj@17618
   277
    let val t = mk_conj(Not $ x, Not $ y)
webertj@17618
   278
        val neg_thm =  inst_thm sign [x, y] cnf_neg_disj; 
webertj@17618
   279
    in
webertj@17618
   280
        (t, neg_thm)
webertj@17618
   281
    end
webertj@17618
   282
webertj@17618
   283
  | head_nnf sign (Const("Not", _) $ (Const("op -->",_) $ x $ y)) = 
webertj@17618
   284
    let val t = mk_conj(x, Not $ y)
webertj@17618
   285
        val neg_thm = inst_thm sign [x, y] cnf_neg_imp
webertj@17618
   286
    in
webertj@17618
   287
        (t, neg_thm)
webertj@17618
   288
    end
webertj@17618
   289
webertj@17618
   290
  | head_nnf sign (Const("Not",_) $ (Const("Not",_) $ x)) =
webertj@17618
   291
    (x, inst_thm sign [x] cnf_double_neg)
webertj@17618
   292
webertj@17618
   293
  | head_nnf sign (Const("Not",_) $ Const("True",_)) = 
webertj@17618
   294
      (false_const, cnf_not_true_false)
webertj@17618
   295
webertj@17618
   296
  | head_nnf sign (Const("Not",_) $ Const("False",_)) = 
webertj@17618
   297
      (true_const, cnf_not_false_true)  
webertj@17618
   298
webertj@17618
   299
  | head_nnf sign t = 
webertj@17618
   300
    (t, inst_thm sign [t] cnf_eq_id)
webertj@17618
   301
webertj@17618
   302
webertj@17618
   303
(***************************************************************************)
webertj@17618
   304
(*                  Tactics for simple CNF transformation                  *)
webertj@17618
   305
webertj@17618
   306
(* A naive procedure for CNF transformation:
webertj@17618
   307
   Given any t, produce a theorem t = t', where t' is in
webertj@17618
   308
   conjunction normal form 
webertj@17618
   309
*)
webertj@17618
   310
fun mk_cnf_thm sign (Const("Trueprop",_) $ x) = mk_cnf_thm sign x
webertj@17618
   311
  | mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
webertj@17618
   312
  | mk_cnf_thm sign (t as (Free(_,_))) =  inst_thm sign [t] cnf_eq_id
webertj@17618
   313
 
webertj@17618
   314
  | mk_cnf_thm sign (Const("op -->", _) $ x $ y) =
webertj@17618
   315
       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
webertj@17618
   316
           val thm2 = mk_cnf_thm sign (mk_disj(Not $ x, y));
webertj@17618
   317
       in
webertj@17618
   318
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   319
       end
webertj@17618
   320
webertj@17618
   321
  | mk_cnf_thm sign (Const("op &", _) $ x $ y) = 
webertj@17618
   322
       let val cnf1 = mk_cnf_thm sign x;
webertj@17618
   323
           val cnf2 = mk_cnf_thm sign y;
webertj@17618
   324
       in
webertj@17618
   325
           cnf_comb2eq OF [cnf1, cnf2]
webertj@17618
   326
       end
webertj@17618
   327
webertj@17618
   328
  | mk_cnf_thm sign (Const("Not",_) $ Const("True",_)) = 
webertj@17618
   329
        cnf_not_true_false
webertj@17618
   330
webertj@17618
   331
  | mk_cnf_thm sign (Const("Not",_) $ Const("False",_)) = 
webertj@17618
   332
        cnf_not_false_true
webertj@17618
   333
webertj@17618
   334
  | mk_cnf_thm sign (t as (Const("Not", _) $ x)) =
webertj@17618
   335
      ( 
webertj@17618
   336
       if (is_atm x) then inst_thm sign [t] cnf_eq_id
webertj@17618
   337
       else
webertj@17618
   338
         let val (t1, hn_thm) = head_nnf sign t
webertj@17618
   339
             val cnf_thm = mk_cnf_thm sign t1
webertj@17618
   340
         in
webertj@17618
   341
             cnf_eq_trans OF [hn_thm, cnf_thm]
webertj@17618
   342
         end
webertj@17618
   343
       ) 
webertj@17618
   344
webertj@17618
   345
  | mk_cnf_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
webertj@17618
   346
       let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
webertj@17618
   347
           val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
webertj@17618
   348
       in
webertj@17618
   349
          cnf_eq_trans OF [thm1, thm2]
webertj@17618
   350
       end
webertj@17618
   351
webertj@17618
   352
  | mk_cnf_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
webertj@17618
   353
       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
webertj@17618
   354
           val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
webertj@17618
   355
       in
webertj@17618
   356
          cnf_eq_trans OF [thm1, thm2]
webertj@17618
   357
       end
webertj@17618
   358
webertj@17618
   359
  | mk_cnf_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
webertj@17618
   360
       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
webertj@17618
   361
           val thm2 = mk_cnf_thm sign (mk_disj(Not $ p, mk_disj(q, r)));
webertj@17618
   362
       in
webertj@17618
   363
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   364
       end
webertj@17618
   365
webertj@17618
   366
  | mk_cnf_thm sign (Const("op |",_) $ Const("False",_) $ p) =
webertj@17618
   367
       let val thm1 = inst_thm sign [p] cnf_disj_false;
webertj@17618
   368
           val thm2 = mk_cnf_thm sign p
webertj@17618
   369
       in
webertj@17618
   370
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   371
       end
webertj@17618
   372
webertj@17618
   373
  | mk_cnf_thm sign (Const("op |",_) $ Const("True",_) $ p) =
webertj@17618
   374
       inst_thm sign [p] cnf_disj_true
webertj@17618
   375
webertj@17618
   376
  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
webertj@17618
   377
       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
webertj@17618
   378
           val thm2 = mk_cnf_thm sign p
webertj@17618
   379
       in
webertj@17618
   380
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   381
       end
webertj@17618
   382
webertj@17618
   383
  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
webertj@17618
   384
       inst_thm sign [p] cnf_disj_not_false
webertj@17618
   385
webertj@17618
   386
  | mk_cnf_thm sign (t as (Const("op |",_) $ p $ q)) = 
webertj@17618
   387
       if (is_lit p) then
webertj@17618
   388
          (
webertj@17618
   389
            if (is_clause t) then inst_thm sign [t] cnf_eq_id
webertj@17618
   390
            else 
webertj@17618
   391
             let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
webertj@17618
   392
                 val thm2 = mk_cnf_thm sign (mk_disj(q, p))
webertj@17618
   393
             in
webertj@17618
   394
                cnf_eq_trans OF [thm1, thm2]
webertj@17618
   395
             end
webertj@17618
   396
          )
webertj@17618
   397
       else 
webertj@17618
   398
            let val (u, thm1) = head_nnf sign p;
webertj@17618
   399
                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
webertj@17618
   400
                val thm3 = mk_cnf_thm sign (mk_disj(u, q))
webertj@17618
   401
            in
webertj@17618
   402
                cnf_eq_trans OF [(thm1 RS thm2), thm3]
webertj@17618
   403
            end
webertj@17618
   404
webertj@17618
   405
 | mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
webertj@17618
   406
    (* error ("I don't know how to handle the formula " ^ 
webertj@17618
   407
                          (Sign.string_of_term sign t))
webertj@17618
   408
    *)
webertj@17618
   409
webertj@17618
   410
fun term_of_thm c = term_of (cprop_of c)
webertj@17618
   411
webertj@17618
   412
webertj@17618
   413
(* Transform a given list of theorems (thms) into CNF *)
webertj@17618
   414
webertj@17618
   415
fun mk_cnf_thms sg nil = nil
webertj@17618
   416
  | mk_cnf_thms sg (x::l) = 
webertj@17618
   417
    let val t = term_of_thm x
webertj@17618
   418
    in
webertj@17618
   419
      if (is_clause t) then x :: mk_cnf_thms sg l
webertj@17618
   420
      else 
webertj@17618
   421
       let val thm1 = mk_cnf_thm sg t
webertj@17618
   422
           val thm2 = cnf_eq_imp OF [thm1, x]
webertj@17618
   423
       in 
webertj@17618
   424
           thm2 :: mk_cnf_thms sg l
webertj@17618
   425
       end
webertj@17618
   426
    end
webertj@17618
   427
webertj@17618
   428
webertj@17618
   429
(* Count the number of hypotheses in a formula *)
webertj@17618
   430
fun num_of_hyps (Const("Trueprop", _) $ x) = num_of_hyps x
webertj@17618
   431
  | num_of_hyps (Const("==>",_) $ x $ y) = 1 + (num_of_hyps y)
webertj@17618
   432
  | num_of_hyps t = 0
webertj@17618
   433
webertj@17618
   434
(* Tactic for converting to CNF (in primitive form): 
webertj@17618
   435
   it takes the first subgoal of the proof state, transform all its
webertj@17618
   436
   hypotheses into CNF (in primivite form) and remove the original 
webertj@17618
   437
   hypotheses.
webertj@17618
   438
*)
webertj@17618
   439
fun cnf_thin_tac state =
webertj@17618
   440
let val sg = Thm.sign_of_thm state
webertj@17618
   441
in
webertj@17618
   442
case (prems_of state) of 
webertj@17618
   443
  [] => Seq.empty
webertj@17618
   444
| (subgoal::_) => 
webertj@17618
   445
  let 
webertj@17618
   446
    val n = num_of_hyps (strip_all_body subgoal);
webertj@17618
   447
    val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
webertj@17618
   448
  in
webertj@17618
   449
    (tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
webertj@17618
   450
  end
webertj@17618
   451
end
webertj@17618
   452
webertj@17618
   453
(* Tactic for converting to CNF (in primitive form), keeping 
webertj@17618
   454
   the original hypotheses. *)
webertj@17618
   455
webertj@17618
   456
fun cnf_tac state =
webertj@17618
   457
let val sg = Thm.sign_of_thm state
webertj@17618
   458
in
webertj@17618
   459
case (prems_of state) of 
webertj@17618
   460
  [] => Seq.empty
webertj@17618
   461
| (subgoal::_) => 
webertj@17618
   462
   METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1 
webertj@17618
   463
                    THEN (REPEAT (etac conjE 1)) ) 1 state
webertj@17618
   464
end
webertj@17618
   465
webertj@17618
   466
webertj@17618
   467
(***************************************************************************)
webertj@17618
   468
(*            CNF transformation by introducing new literals               *)
webertj@17618
   469
webertj@17618
   470
(*** IMPORTANT: 
webertj@17618
   471
  This transformation uses variables of the form "lit_i", where i is a natural
webertj@17618
   472
  number. For the transformation to work, these variables must not already
webertj@17618
   473
  occur freely in the formula being transformed.
webertj@17618
   474
***)
webertj@17618
   475
webertj@17618
   476
fun ext_conj x p q r =
webertj@17618
   477
   mk_conj(
webertj@17618
   478
    mk_disj(Not $ x, p),
webertj@17618
   479
    mk_conj(
webertj@17618
   480
      mk_disj(Not $ x, q),
webertj@17618
   481
      mk_conj(
webertj@17618
   482
        mk_disj(x, mk_disj(Not $ p, Not $ q)),
webertj@17618
   483
        mk_disj(x, r)
webertj@17618
   484
      )
webertj@17618
   485
    )
webertj@17618
   486
   )
webertj@17618
   487
webertj@17618
   488
webertj@17618
   489
(* Transform to CNF in primitive forms, possibly introduce extra variables *)
webertj@17618
   490
fun mk_cnfx_thm sign (Const("Trueprop",_) $ x) = mk_cnfx_thm sign x 
webertj@17618
   491
  | mk_cnfx_thm sign (t as (Const(_,_)))  = inst_thm sign [t] cnf_eq_id
webertj@17618
   492
  | mk_cnfx_thm sign (t as (Free(_,_)))  = inst_thm sign [t] cnf_eq_id
webertj@17618
   493
  | mk_cnfx_thm sign (Const("op -->", _) $ x $ y)  =
webertj@17618
   494
       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
webertj@17618
   495
           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ x, y)) 
webertj@17618
   496
       in
webertj@17618
   497
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   498
       end
webertj@17618
   499
webertj@17618
   500
  | mk_cnfx_thm sign (Const("op &", _) $ x $ y)  = 
webertj@17618
   501
       let val cnf1 = mk_cnfx_thm sign x
webertj@17618
   502
           val cnf2 = mk_cnfx_thm sign y
webertj@17618
   503
       in
webertj@17618
   504
           cnf_comb2eq OF [cnf1, cnf2]
webertj@17618
   505
       end
webertj@17618
   506
webertj@17618
   507
  | mk_cnfx_thm sign (Const("Not",_) $ Const("True",_)) = 
webertj@17618
   508
        cnf_not_true_false
webertj@17618
   509
webertj@17618
   510
  | mk_cnfx_thm sign (Const("Not",_) $ Const("False",_))  = 
webertj@17618
   511
        cnf_not_false_true
webertj@17618
   512
webertj@17618
   513
  | mk_cnfx_thm sign (t as (Const("Not", _) $ x))  =
webertj@17618
   514
      ( 
webertj@17618
   515
       if (is_atm x) then inst_thm sign [t] cnf_eq_id
webertj@17618
   516
       else
webertj@17618
   517
         let val (t1, hn_thm) = head_nnf sign t
webertj@17618
   518
             val cnf_thm = mk_cnfx_thm sign t1 
webertj@17618
   519
         in
webertj@17618
   520
             cnf_eq_trans OF [hn_thm, cnf_thm]
webertj@17618
   521
         end
webertj@17618
   522
       ) 
webertj@17618
   523
webertj@17618
   524
  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r)  =
webertj@17618
   525
      if (is_lit r) then
webertj@17618
   526
        let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
webertj@17618
   527
            val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
webertj@17618
   528
        in
webertj@17618
   529
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   530
        end
webertj@17618
   531
      else cnfx_newlit sign p q r 
webertj@17618
   532
webertj@17618
   533
  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r)  =
webertj@17618
   534
       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
webertj@17618
   535
           val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r))) 
webertj@17618
   536
       in
webertj@17618
   537
          cnf_eq_trans OF [thm1, thm2]
webertj@17618
   538
       end
webertj@17618
   539
webertj@17618
   540
  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
webertj@17618
   541
       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
webertj@17618
   542
           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ p, mk_disj(q, r))) 
webertj@17618
   543
       in
webertj@17618
   544
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   545
       end
webertj@17618
   546
webertj@17618
   547
  | mk_cnfx_thm sign (Const("op |",_) $ Const("False",_) $ p)  =
webertj@17618
   548
       let val thm1 = inst_thm sign [p] cnf_disj_false;
webertj@17618
   549
           val thm2 = mk_cnfx_thm sign p 
webertj@17618
   550
       in
webertj@17618
   551
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   552
       end
webertj@17618
   553
webertj@17618
   554
  | mk_cnfx_thm sign (Const("op |",_) $ Const("True",_) $ p)  =
webertj@17618
   555
       inst_thm sign [p] cnf_disj_true
webertj@17618
   556
webertj@17618
   557
  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p)  =
webertj@17618
   558
       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
webertj@17618
   559
           val thm2 = mk_cnfx_thm sign p 
webertj@17618
   560
       in
webertj@17618
   561
           cnf_eq_trans OF [thm1, thm2]
webertj@17618
   562
       end
webertj@17618
   563
webertj@17618
   564
  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p)  =
webertj@17618
   565
       inst_thm sign [p] cnf_disj_not_false
webertj@17618
   566
webertj@17618
   567
  | mk_cnfx_thm sign (t as (Const("op |",_) $ p $ q))  = 
webertj@17618
   568
       if (is_lit p) then
webertj@17618
   569
          (
webertj@17618
   570
            if (is_clause t) then inst_thm sign [t] cnf_eq_id
webertj@17618
   571
            else 
webertj@17618
   572
             let val thm1 = inst_thm sign [p, q] cnf_disj_sym
webertj@17618
   573
                 val thm2 = mk_cnfx_thm sign (mk_disj(q, p)) 
webertj@17618
   574
             in
webertj@17618
   575
                cnf_eq_trans OF [thm1, thm2]
webertj@17618
   576
             end
webertj@17618
   577
          )
webertj@17618
   578
       else 
webertj@17618
   579
            let val (u, thm1) = head_nnf sign p
webertj@17618
   580
                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
webertj@17618
   581
                val thm3 = mk_cnfx_thm sign (mk_disj(u, q)) 
webertj@17618
   582
            in
webertj@17618
   583
                cnf_eq_trans OF [(thm1 RS thm2), thm3]
webertj@17618
   584
            end
webertj@17618
   585
webertj@17618
   586
 | mk_cnfx_thm sign t  = error ("I don't know how to handle the formula " ^ 
webertj@17618
   587
                          (Sign.string_of_term sign t))
webertj@17618
   588
webertj@17618
   589
and cnfx_newlit sign p q r  = 
webertj@17618
   590
   let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
webertj@17618
   591
       val _ = (lit_id := !lit_id + 1)
webertj@17618
   592
       val ct_lit = cterm_of sign lit
webertj@17618
   593
       val x_conj = ext_conj lit p q r
webertj@17618
   594
       val thm1 = inst_thm sign [p,q,r] cnf_newlit
webertj@17618
   595
       val thm2 = mk_cnfx_thm sign x_conj 
webertj@17618
   596
       val thm3 = forall_intr ct_lit thm2
webertj@17618
   597
       val thm4 = strip_shyps (thm3 COMP allI)
webertj@17618
   598
       val thm5 = strip_shyps (thm4 RS cnf_all_ex)
webertj@17618
   599
   in
webertj@17618
   600
       cnf_eq_trans OF [thm1, thm5]
webertj@17618
   601
   end
webertj@17618
   602
webertj@17618
   603
webertj@17618
   604
(* Theorems for converting formula into CNF (in primitive form), with 
webertj@17618
   605
   new extra variables *)
webertj@17618
   606
webertj@17618
   607
webertj@17618
   608
fun mk_cnfx_thms sg nil = nil
webertj@17618
   609
  | mk_cnfx_thms sg (x::l) = 
webertj@17618
   610
    let val t = term_of_thm x
webertj@17618
   611
    in
webertj@17618
   612
      if (is_clause t) then x :: mk_cnfx_thms sg l
webertj@17618
   613
      else 
webertj@17618
   614
       let val thm1 = mk_cnfx_thm sg t
webertj@17618
   615
           val thm2 = cnf_eq_imp OF [thm1,x]
webertj@17618
   616
       in 
webertj@17618
   617
           thm2 :: mk_cnfx_thms sg l
webertj@17618
   618
       end
webertj@17618
   619
    end
webertj@17618
   620
webertj@17618
   621
webertj@17618
   622
(* Tactic for converting hypotheses into CNF, possibly
webertj@17618
   623
   introducing new variables *)
webertj@17618
   624
webertj@17618
   625
fun cnfx_thin_tac state =
webertj@17618
   626
let val sg = Thm.sign_of_thm state
webertj@17618
   627
in
webertj@17618
   628
case (prems_of state) of 
webertj@17618
   629
  [] => Seq.empty
webertj@17618
   630
| (subgoal::_) => 
webertj@17618
   631
   let val n = num_of_hyps (strip_all_body subgoal);
webertj@17618
   632
       val tac1 =  METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
webertj@17618
   633
   in
webertj@17618
   634
      EVERY [tac1, weakenings_tac n, 
webertj@17618
   635
             REPEAT (etac conjE 1 ORELSE etac exE 1)] state
webertj@17618
   636
   end
webertj@17618
   637
end
webertj@17618
   638
webertj@17618
   639
(* Tactic for converting the conclusion of a goal into CNF *)
webertj@17618
   640
webertj@17618
   641
fun get_concl (Const("Trueprop", _) $ x) = get_concl x
webertj@17618
   642
  | get_concl (Const("==>",_) $ x $ y) = get_concl y
webertj@17618
   643
  | get_concl t = t
webertj@17618
   644
webertj@17618
   645
fun cnf_concl_tac' state =
webertj@17618
   646
case (prems_of state) of 
webertj@17618
   647
  [] => Seq.empty
webertj@17618
   648
| (subgoal::_) =>
webertj@17618
   649
  let val sg = Thm.sign_of_thm state
webertj@17618
   650
      val c = get_concl subgoal
webertj@17618
   651
      val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
webertj@17618
   652
      val thm2 = thm1 RS subst
webertj@17618
   653
  in
webertj@17618
   654
    rtac thm2 1 state
webertj@17618
   655
  end
webertj@17618
   656
webertj@17618
   657
val cnf_concl_tac  = METAHYPS (fn l => cnf_concl_tac') 1 
webertj@17618
   658
webertj@17618
   659
webertj@17618
   660
end (*of structure*)