src/HOL/Tools/SMT/z3_proof_literals.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36898 8e55aa1306c5
child 38795 848be46708dc
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/z3_proof_literals.ML
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Proof tools related to conjunctions and disjunctions.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature Z3_PROOF_LITERALS =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     9
  (* literal table *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  type littab = thm Termtab.table
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
  val make_littab: thm list -> littab
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
  val insert_lit: thm -> littab -> littab
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
  val delete_lit: thm -> littab -> littab
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
  val lookup_lit: littab -> term -> thm option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
  val get_first_lit: (term -> bool) -> littab -> thm option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
  (* rules *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
  val true_thm: thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  val rewrite_true: thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
  (* properties *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
  val is_conj: term -> bool
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
  val is_disj: term -> bool
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
  val exists_lit: bool -> (term -> bool) -> term -> bool
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
  (* proof tools *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
  val explode: bool -> bool -> bool -> term list -> thm -> thm list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
  val join: bool -> littab -> term -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
  val prove_conj_disj_eq: cterm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
structure T = Z3_Proof_Tools
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
(** literal table **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
type littab = thm Termtab.table
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
fun insert_lit thm = Termtab.update (`T.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
fun delete_lit thm = Termtab.delete (T.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
fun lookup_lit lits = Termtab.lookup lits
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
fun get_first_lit f =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
  Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
(** rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
val true_thm = @{lemma "~False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
val rewrite_true = @{lemma "True == ~ False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
(** properties and term operations **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
val is_neg = (fn @{term Not} $ _ => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
val is_dneg = is_neg' is_neg
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
fun dest_disj_term' f = (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
    @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
  | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
val dest_disj_term =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
fun exists_lit is_conj P =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
    val dest = if is_conj then dest_conj_term else dest_disj_term
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
    fun exists t = P t orelse
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
      (case dest t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
        SOME (t1, t2) => exists t1 orelse exists t2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
      | NONE => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
  in exists end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
(** proof tools **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
(* explosion of conjunctions and disjunctions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
  fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
  val dest_conj1 = T.precompose2 destc @{thm conjunct1}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
  val dest_conj2 = T.precompose2 destc @{thm conjunct2}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
  fun dest_conj_rules t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
    dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
    
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
  fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
  val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
  val dest_disj1 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
  val dest_disj2 = T.precompose2 (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
  val dest_disj3 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
  val dest_disj4 = T.precompose2 (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
  fun dest_disj_rules t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
    (case dest_disj_term' is_neg t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
      SOME (true, true) => SOME (dest_disj2, dest_disj4)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
    | SOME (true, false) => SOME (dest_disj2, dest_disj3)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
    | SOME (false, true) => SOME (dest_disj1, dest_disj4)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
    | SOME (false, false) => SOME (dest_disj1, dest_disj3)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
    | NONE => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
  fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
  val dneg_rule = T.precompose destn @{thm notnotD}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
(* explode a term into literals and collect all rules to be able to deduce
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
   particular literals afterwards *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
fun explode_term is_conj =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
    val dest = if is_conj then dest_conj_term else dest_disj_term
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
    val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
    fun add (t, rs) = Termtab.map_default (t, rs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
      (fn rs' => if length rs' < length rs then rs' else rs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
    fun explode1 rules t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
      (case dest t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
        SOME (t1, t2) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
          let val (rule1, rule2) = the (dest_rules t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
          in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
            explode1 (rule1 :: rules) t1 #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
            explode1 (rule2 :: rules) t2 #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
            add (t, rev rules)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
          end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
      | NONE => add (t, rev rules))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
    fun explode0 (@{term Not} $ (@{term Not} $ t)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
          Termtab.make [(t, [dneg_rule])]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
      | explode0 t = explode1 [] t Termtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
  in explode0 end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
(* extract a literal by applying previously collected rules *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
fun extract_lit thm rules = fold T.compose rules thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
(* explode a theorem into its literals *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
fun explode is_conj full keep_intermediate stop_lits =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
    val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
    val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
    fun explode1 thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
      if Termtab.defined tab (T.prop_of thm) then cons thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
      else
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
        (case dest_rules (T.prop_of thm) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
          SOME (rule1, rule2) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
            explode2 rule1 thm #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
            explode2 rule2 thm #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
            keep_intermediate ? cons thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
        | NONE => cons thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
    and explode2 dest_rule thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
      if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
      then explode1 (T.compose dest_rule thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
      else cons (T.compose dest_rule thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
    fun explode0 thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
      if not is_conj andalso is_dneg (T.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
      then [T.compose dneg_rule thm]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
      else explode1 thm []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
  in explode0 end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
(* joining of literals to conjunctions or disjunctions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
  fun on_cprem i f thm = f (Thm.cprem_of thm i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
  fun on_cprop f thm = f (Thm.cprop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
  fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
  fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
    Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
    |> T.discharge thm1 |> T.discharge thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
  fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
  val conj_rule = precomp2 d1 d1 @{thm conjI}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
  fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
  val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
  val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
  val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
  val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
  fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
    | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
    | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
    | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
  fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
    | dest_conj t = raise TERM ("dest_conj", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
  val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
  fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
    | dest_disj t = raise TERM ("dest_disj", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
  val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
  val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
  fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
  fun dni f = apsnd f o Thm.dest_binop o f o d1
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
  val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
  val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
  val iff_const = @{term "op = :: bool => _"}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
  fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
        f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
    | as_negIff _ _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
fun join is_conj littab t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
    val comp = if is_conj then comp_conj else comp_disj
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
    val dest = if is_conj then dest_conj else dest_disj
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
    val lookup = lookup_lit littab
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
    fun lookup_rule t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
      (case t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
        @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
      | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
          (T.compose negIffI, lookup (iff_const $ u $ t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
      | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
          let fun rewr lit = lit COMP @{thm not_sym}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
          in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
      | _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
          (case as_dneg lookup t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
            NONE => (T.compose negIffE, as_negIff lookup t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
          | x => (T.compose dnegE, x)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
    fun join1 (s, t) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
      (case lookup t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
        SOME lit => (s, lit)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
      | NONE => 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
          (case lookup_rule t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
            (rewrite, SOME lit) => (s, rewrite lit)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
          | (_, NONE) => (s, comp (pairself join1 (dest t)))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
  in snd (join1 (if is_conj then (false, t) else (true, t))) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
(* proving equality of conjunctions or disjunctions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
  val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
  val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
  val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
  val neg = Thm.capply @{cterm Not}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
  val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
  fun contra_left conj thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
      val rules = explode_term conj (T.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
      fun contra_lits (t, rs) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
        (case t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
          @{term Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
        | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
      (case Termtab.lookup rules @{term False} of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
        SOME rs => extract_lit thm rs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
      | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
          the (Termtab.get_first contra_lits rules)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
          |> pairself (extract_lit thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
          |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
  val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
  fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
fun contradict conj ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
  iff_intro (T.under_assumption (contra_left conj) ct) (contra_right ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
  fun prove_eq l r (cl, cr) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
      fun explode' is_conj = explode is_conj true (l <> r) []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
      fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
      fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
      val thm1 = T.under_assumption (prove r cr o make_tab l) cl
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
      val thm2 = T.under_assumption (prove l cl o make_tab r) cr
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
    in iff_intro thm1 thm2 end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
  datatype conj_disj = CONJ | DISJ | NCON | NDIS
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
  fun kind_of t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
    if is_conj t then SOME CONJ
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
    else if is_disj t then SOME DISJ
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
    else if is_neg' is_conj t then SOME NCON
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
    else if is_neg' is_disj t then SOME NDIS
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
    else NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   321
fun prove_conj_disj_eq ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   322
  let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   323
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   324
    (case (kind_of (Thm.term_of cl), Thm.term_of cr) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   325
      (SOME CONJ, @{term False}) => contradict true cl
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   326
    | (SOME DISJ, @{term "~False"}) => contrapos2 (contradict false o fst) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   327
    | (kl, _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   328
        (case (kl, kind_of (Thm.term_of cr)) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
          (SOME CONJ, SOME CONJ) => prove_eq true true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   330
        | (SOME CONJ, SOME NDIS) => prove_eq true false cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
        | (SOME CONJ, _) => prove_eq true true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
        | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   333
        | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
        | (SOME DISJ, _) => contrapos1 (prove_eq false false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
        | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
        | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   337
        | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
        | (SOME NDIS, SOME NDIS) => prove_eq false false cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   339
        | (SOME NDIS, SOME CONJ) => prove_eq false true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
        | (SOME NDIS, NONE) => prove_eq false true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   341
        | _ => raise CTERM ("prove_conj_disj_eq", [ct])))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   342
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   344
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
end