src/HOL/Tools/prop_logic.ML
author blanchet
Tue, 06 Oct 2015 11:34:07 +0200
changeset 61332 22378817612f
parent 58322 f13f6e27d68e
child 69605 3dda49e08b9d
permissions -rw-r--r--
tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     1
(*  Title:      HOL/Tools/prop_logic.ML
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     2
    Author:     Tjark Weber
31220
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
     3
    Copyright   2004-2009
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     4
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     5
Formulas of propositional logic.
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     6
*)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     7
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     8
signature PROP_LOGIC =
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     9
sig
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    10
  datatype prop_formula =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    11
      True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    12
    | False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    13
    | BoolVar of int  (* NOTE: only use indices >= 1 *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    14
    | Not of prop_formula
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    15
    | Or of prop_formula * prop_formula
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    16
    | And of prop_formula * prop_formula
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    17
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    18
  val SNot: prop_formula -> prop_formula
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    19
  val SOr: prop_formula * prop_formula -> prop_formula
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    20
  val SAnd: prop_formula * prop_formula -> prop_formula
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    21
  val simplify: prop_formula -> prop_formula  (* eliminates True/False and double-negation *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    22
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    23
  val indices: prop_formula -> int list  (* set of all variable indices *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    24
  val maxidx: prop_formula -> int       (* maximal variable index *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    25
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    26
  val exists: prop_formula list -> prop_formula  (* finite disjunction *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    27
  val all: prop_formula list -> prop_formula  (* finite conjunction *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    28
  val dot_product: prop_formula list * prop_formula list -> prop_formula
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    29
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    30
  val is_nnf: prop_formula -> bool  (* returns true iff the formula is in negation normal form *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    31
  val is_cnf: prop_formula -> bool  (* returns true iff the formula is in conjunctive normal form *)
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
    32
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    33
  val nnf: prop_formula -> prop_formula  (* negation normal form *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    34
  val cnf: prop_formula -> prop_formula  (* conjunctive normal form *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    35
  val defcnf: prop_formula -> prop_formula  (* definitional cnf *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    36
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    37
  val eval: (int -> bool) -> prop_formula -> bool  (* semantics *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
    38
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    39
  (* propositional representation of HOL terms *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    40
  val prop_formula_of_term: term -> int Termtab.table -> prop_formula * int Termtab.table
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    41
  (* HOL term representation of propositional formulae *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    42
  val term_of_prop_formula: prop_formula -> term
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    43
end;
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    44
41471
54a58904a598 modernized structure Prop_Logic;
wenzelm
parents: 41447
diff changeset
    45
structure Prop_Logic : PROP_LOGIC =
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    46
struct
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    47
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    48
(* ------------------------------------------------------------------------- *)
14753
f40b45db8cf0 Comments fixed
webertj
parents: 14681
diff changeset
    49
(* prop_formula: formulas of propositional logic, built from Boolean         *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    50
(*               variables (referred to by index) and True/False using       *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    51
(*               not/or/and                                                  *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    52
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    53
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    54
datatype prop_formula =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    55
    True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    56
  | False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    57
  | BoolVar of int  (* NOTE: only use indices >= 1 *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    58
  | Not of prop_formula
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    59
  | Or of prop_formula * prop_formula
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    60
  | And of prop_formula * prop_formula;
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    61
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    62
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    63
(* The following constructor functions make sure that True and False do not  *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    64
(* occur within any of the other connectives (i.e. Not, Or, And), and        *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    65
(* perform double-negation elimination.                                      *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    66
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    67
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    68
fun SNot True = False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    69
  | SNot False = True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    70
  | SNot (Not fm) = fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    71
  | SNot fm = Not fm;
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    72
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    73
fun SOr (True, _) = True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    74
  | SOr (_, True) = True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    75
  | SOr (False, fm) = fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    76
  | SOr (fm, False) = fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    77
  | SOr (fm1, fm2) = Or (fm1, fm2);
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    78
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    79
fun SAnd (True, fm) = fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    80
  | SAnd (fm, True) = fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    81
  | SAnd (False, _) = False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    82
  | SAnd (_, False) = False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    83
  | SAnd (fm1, fm2) = And (fm1, fm2);
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    84
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    85
(* ------------------------------------------------------------------------- *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    86
(* simplify: eliminates True/False below other connectives, and double-      *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    87
(*      negation                                                             *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    88
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    89
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    90
fun simplify (Not fm) = SNot (simplify fm)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    91
  | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    92
  | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
    93
  | simplify fm = fm;
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    94
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    95
(* ------------------------------------------------------------------------- *)
14753
f40b45db8cf0 Comments fixed
webertj
parents: 14681
diff changeset
    96
(* indices: collects all indices of Boolean variables that occur in a        *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    97
(*      propositional formula 'fm'; no duplicates                            *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    98
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    99
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   100
fun indices True = []
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   101
  | indices False = []
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   102
  | indices (BoolVar i) = [i]
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   103
  | indices (Not fm) = indices fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   104
  | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   105
  | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2);
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   106
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   107
(* ------------------------------------------------------------------------- *)
58322
f13f6e27d68e fixed spellings
blanchet
parents: 55436
diff changeset
   108
(* maxidx: computes the maximal variable index occurring in a formula of     *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   109
(*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   110
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   111
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   112
fun maxidx True = 0
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   113
  | maxidx False = 0
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   114
  | maxidx (BoolVar i) = i
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   115
  | maxidx (Not fm) = maxidx fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   116
  | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   117
  | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   118
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   119
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   120
(* exists: computes the disjunction over a list 'xs' of propositional        *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   121
(*      formulas                                                             *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   122
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   123
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   124
fun exists xs = Library.foldl SOr (False, xs);
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   125
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   126
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   127
(* all: computes the conjunction over a list 'xs' of propositional formulas  *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   128
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   129
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   130
fun all xs = Library.foldl SAnd (True, xs);
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   131
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   132
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   133
(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   134
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   135
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   136
fun dot_product (xs, ys) = exists (map SAnd (xs ~~ ys));
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   137
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   138
(* ------------------------------------------------------------------------- *)
31220
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   139
(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e.,  *)
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   140
(*         only variables may be negated, but not subformulas).              *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   141
(* ------------------------------------------------------------------------- *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   142
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   143
local
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   144
  fun is_literal (BoolVar _) = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   145
    | is_literal (Not (BoolVar _)) = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   146
    | is_literal _ = false
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   147
  fun is_conj_disj (Or (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   148
    | is_conj_disj (And (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   149
    | is_conj_disj fm = is_literal fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   150
in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   151
  fun is_nnf True = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   152
    | is_nnf False = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   153
    | is_nnf fm = is_conj_disj fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   154
end;
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   155
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   156
(* ------------------------------------------------------------------------- *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   157
(* is_cnf: returns 'true' iff the formula is in conjunctive normal form      *)
31220
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   158
(*         (i.e., a conjunction of disjunctions of literals). 'is_cnf'       *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   159
(*         implies 'is_nnf'.                                                 *)
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   160
(* ------------------------------------------------------------------------- *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   161
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   162
local
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   163
  fun is_literal (BoolVar _) = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   164
    | is_literal (Not (BoolVar _)) = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   165
    | is_literal _ = false
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   166
  fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   167
    | is_disj fm = is_literal fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   168
  fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   169
    | is_conj fm = is_disj fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   170
in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   171
  fun is_cnf True = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   172
    | is_cnf False = true
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   173
    | is_cnf fm = is_conj fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   174
end;
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   175
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   176
(* ------------------------------------------------------------------------- *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   177
(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
31220
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   178
(*      logic (i.e., only variables may be negated, but not subformulas).    *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   179
(*      Simplification (cf. 'simplify') is performed as well. Not            *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   180
(*      surprisingly, 'is_nnf o nnf' always returns 'true'. 'nnf fm' returns *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   181
(*      'fm' if (and only if) 'is_nnf fm' returns 'true'.                    *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   182
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   183
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   184
fun nnf fm =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   185
  let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   186
    fun
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   187
      (* constants *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   188
        nnf_aux True = True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   189
      | nnf_aux False = False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   190
      (* variables *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   191
      | nnf_aux (BoolVar i) = (BoolVar i)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   192
      (* 'or' and 'and' as outermost connectives are left untouched *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   193
      | nnf_aux (Or  (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   194
      | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   195
      (* 'not' + constant *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   196
      | nnf_aux (Not True) = False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   197
      | nnf_aux (Not False) = True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   198
      (* 'not' + variable *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   199
      | nnf_aux (Not (BoolVar i)) = Not (BoolVar i)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   200
      (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   201
      | nnf_aux (Not (Or  (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   202
      | nnf_aux (Not (And (fm1, fm2))) = SOr  (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   203
      (* double-negation elimination *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   204
      | nnf_aux (Not (Not fm)) = nnf_aux fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   205
  in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   206
    if is_nnf fm then fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   207
    else nnf_aux fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   208
  end;
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   209
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   210
(* ------------------------------------------------------------------------- *)
31220
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   211
(* cnf: computes the conjunctive normal form (i.e., a conjunction of         *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   212
(*      disjunctions of literals) of a formula 'fm' of propositional logic.  *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   213
(*      Simplification (cf. 'simplify') is performed as well. The result     *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   214
(*      is equivalent to 'fm', but may be exponentially longer. Not          *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   215
(*      surprisingly, 'is_cnf o cnf' always returns 'true'. 'cnf fm' returns *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   216
(*      'fm' if (and only if) 'is_cnf fm' returns 'true'.                    *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   217
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   218
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   219
fun cnf fm =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   220
  let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   221
    (* function to push an 'Or' below 'And's, using distributive laws *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   222
    fun cnf_or (And (fm11, fm12), fm2) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   223
          And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   224
      | cnf_or (fm1, And (fm21, fm22)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   225
          And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   226
    (* neither subformula contains 'And' *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   227
      | cnf_or (fm1, fm2) = Or (fm1, fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   228
    fun cnf_from_nnf True = True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   229
      | cnf_from_nnf False = False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   230
      | cnf_from_nnf (BoolVar i) = BoolVar i
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   231
    (* 'fm' must be a variable since the formula is in NNF *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   232
      | cnf_from_nnf (Not fm) = Not fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   233
    (* 'Or' may need to be pushed below 'And' *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   234
      | cnf_from_nnf (Or (fm1, fm2)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   235
        cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   236
    (* 'And' as outermost connective is left untouched *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   237
      | cnf_from_nnf (And (fm1, fm2)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   238
        And (cnf_from_nnf fm1, cnf_from_nnf fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   239
  in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   240
    if is_cnf fm then fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   241
    else (cnf_from_nnf o nnf) fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   242
  end;
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   243
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   244
(* ------------------------------------------------------------------------- *)
31220
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   245
(* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   246
(*      of propositional logic. Simplification (cf. 'simplify') is performed *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   247
(*      as well. 'defcnf' may introduce auxiliary Boolean variables to avoid *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   248
(*      an exponential blowup of the formula.  The result is equisatisfiable *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   249
(*      (i.e., satisfiable if and only if 'fm' is satisfiable), but not      *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   250
(*      necessarily equivalent to 'fm'. Not surprisingly, 'is_cnf o defcnf'  *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   251
(*      always returns 'true'. 'defcnf fm' returns 'fm' if (and only if)     *)
f1c0ed85a33b implementation of definitional CNF improved
webertj
parents: 22441
diff changeset
   252
(*      'is_cnf fm' returns 'true'.                                          *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   253
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   254
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   255
fun defcnf fm =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   256
  if is_cnf fm then fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   257
  else
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   258
    let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   259
      val fm' = nnf fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   260
      (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   261
      val new = Unsynchronized.ref (maxidx fm' + 1)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   262
      fun new_idx () = let val idx = !new in new := idx+1; idx end
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   263
      (* replaces 'And' by an auxiliary variable (and its definition) *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   264
      fun defcnf_or (And x) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   265
            let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   266
              val i = new_idx ()
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   267
            in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   268
              (* Note that definitions are in NNF, but not CNF. *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   269
              (BoolVar i, [Or (Not (BoolVar i), And x)])
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   270
            end
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   271
        | defcnf_or (Or (fm1, fm2)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   272
            let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   273
              val (fm1', defs1) = defcnf_or fm1
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   274
              val (fm2', defs2) = defcnf_or fm2
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   275
            in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   276
              (Or (fm1', fm2'), defs1 @ defs2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   277
            end
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   278
        | defcnf_or fm = (fm, [])
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   279
      fun defcnf_from_nnf True = True
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   280
        | defcnf_from_nnf False = False
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   281
        | defcnf_from_nnf (BoolVar i) = BoolVar i
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   282
      (* 'fm' must be a variable since the formula is in NNF *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   283
        | defcnf_from_nnf (Not fm) = Not fm
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   284
      (* 'Or' may need to be pushed below 'And' *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   285
      (* 'Or' of literal and 'And': use distributivity *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   286
        | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   287
            And (defcnf_from_nnf (Or (BoolVar i, fm1)),
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   288
                 defcnf_from_nnf (Or (BoolVar i, fm2)))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   289
        | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   290
            And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)),
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   291
                 defcnf_from_nnf (Or (Not (BoolVar i), fm2)))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   292
        | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   293
            And (defcnf_from_nnf (Or (fm1, BoolVar i)),
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   294
                 defcnf_from_nnf (Or (fm2, BoolVar i)))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   295
        | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   296
            And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))),
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   297
                 defcnf_from_nnf (Or (fm2, Not (BoolVar i))))
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   298
      (* all other cases: turn the formula into a disjunction of literals, *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   299
      (*                  adding definitions as necessary                  *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   300
        | defcnf_from_nnf (Or x) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   301
            let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   302
              val (fm, defs) = defcnf_or (Or x)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   303
              val cnf_defs = map defcnf_from_nnf defs
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   304
            in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   305
              all (fm :: cnf_defs)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   306
            end
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   307
      (* 'And' as outermost connective is left untouched *)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   308
        | defcnf_from_nnf (And (fm1, fm2)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   309
            And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   310
    in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   311
      defcnf_from_nnf fm'
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   312
    end;
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   313
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   314
(* ------------------------------------------------------------------------- *)
14753
f40b45db8cf0 Comments fixed
webertj
parents: 14681
diff changeset
   315
(* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   316
(*      truth value of a propositional formula 'fm' is computed              *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   317
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   318
61332
blanchet
parents: 58322
diff changeset
   319
fun eval _ True = true
blanchet
parents: 58322
diff changeset
   320
  | eval _ False = false
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   321
  | eval a (BoolVar i) = (a i)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   322
  | eval a (Not fm) = not (eval a fm)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   323
  | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   324
  | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2);
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   325
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   326
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   327
(* prop_formula_of_term: returns the propositional structure of a HOL term,  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   328
(*      with subterms replaced by Boolean variables.  Also returns a table   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   329
(*      of terms and corresponding variables that extends the table that was *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   330
(*      given as an argument.  Usually, you'll just want to use              *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   331
(*      'Termtab.empty' as value for 'table'.                                *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   332
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   333
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   334
(* Note: The implementation is somewhat optimized; the next index to be used *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   335
(*       is computed only when it is actually needed.  However, when         *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   336
(*       'prop_formula_of_term' is invoked many times, it might be more      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   337
(*       efficient to pass and return this value as an additional parameter, *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   338
(*       so that it does not have to be recomputed (by folding over the      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   339
(*       table) for each invocation.                                         *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   340
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   341
fun prop_formula_of_term t table =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   342
  let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   343
    val next_idx_is_valid = Unsynchronized.ref false
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   344
    val next_idx = Unsynchronized.ref 0
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   345
    fun get_next_idx () =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   346
      if !next_idx_is_valid then
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   347
        Unsynchronized.inc next_idx
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   348
      else (
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   349
        next_idx := Termtab.fold (Integer.max o snd) table 0;
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   350
        next_idx_is_valid := true;
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   351
        Unsynchronized.inc next_idx
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   352
      )
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   353
    fun aux (Const (@{const_name True}, _)) table = (True, table)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   354
      | aux (Const (@{const_name False}, _)) table = (False, table)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   355
      | aux (Const (@{const_name Not}, _) $ x) table = apfst Not (aux x table)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   356
      | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   357
          let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   358
            val (fm1, table1) = aux x table
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   359
            val (fm2, table2) = aux y table1
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   360
          in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   361
            (Or (fm1, fm2), table2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   362
          end
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   363
      | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   364
          let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   365
            val (fm1, table1) = aux x table
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   366
            val (fm2, table2) = aux y table1
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   367
          in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   368
            (And (fm1, fm2), table2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   369
          end
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   370
      | aux x table =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   371
          (case Termtab.lookup table x of
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   372
            SOME i => (BoolVar i, table)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   373
          | NONE =>
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   374
              let
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   375
                val i = get_next_idx ()
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   376
              in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   377
                (BoolVar i, Termtab.update (x, i) table)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   378
              end)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   379
  in
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   380
    aux t table
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   381
  end;
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   382
20442
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   383
(* ------------------------------------------------------------------------- *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   384
(* term_of_prop_formula: returns a HOL term that corresponds to a            *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   385
(*      propositional formula, with Boolean variables replaced by Free's     *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   386
(* ------------------------------------------------------------------------- *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   387
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   388
(* Note: A more generic implementation should take another argument of type  *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   389
(*       Term.term Inttab.table (or so) that specifies HOL terms for some    *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   390
(*       Boolean variables in the formula, similar to 'prop_formula_of_term' *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   391
(*       (but the other way round).                                          *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   392
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 41491
diff changeset
   393
fun term_of_prop_formula True = @{term True}
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 41491
diff changeset
   394
  | term_of_prop_formula False = @{term False}
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41471
diff changeset
   395
  | term_of_prop_formula (BoolVar i) = Free ("v" ^ string_of_int i, HOLogic.boolT)
41447
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   396
  | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   397
  | term_of_prop_formula (Or (fm1, fm2)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   398
      HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   399
  | term_of_prop_formula (And (fm1, fm2)) =
537b290bbe38 tuned whitespace, indentation, comments;
wenzelm
parents: 38795
diff changeset
   400
      HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
20442
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   401
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   402
end;