src/HOL/Library/Old_SMT/old_z3_proof_literals.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 60642 48dd1cefb4ae
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_z3_proof_literals.ML
36898
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
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_Z3_PROOF_LITERALS =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
41123
boehmes
parents: 40579
diff changeset
     9
  (*literal table*)
36898
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
41123
boehmes
parents: 40579
diff changeset
    17
  (*rules*)
36898
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
41123
boehmes
parents: 40579
diff changeset
    21
  (*properties*)
36898
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
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    25
  val negate: cterm -> cterm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
41123
boehmes
parents: 40579
diff changeset
    27
  (*proof tools*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
  val explode: bool -> bool -> bool -> term list -> thm -> thm list
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
  val join: bool -> littab -> term -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
  val prove_conj_disj_eq: cterm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    33
structure Old_Z3_Proof_Literals: OLD_Z3_PROOF_LITERALS =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
41123
boehmes
parents: 40579
diff changeset
    38
(* literal table *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
type littab = thm Termtab.table
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
    42
fun make_littab thms =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    43
  fold (Termtab.update o `Old_SMT_Utils.prop_of) thms Termtab.empty
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    45
fun insert_lit thm = Termtab.update (`Old_SMT_Utils.prop_of thm)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    46
fun delete_lit thm = Termtab.delete (Old_SMT_Utils.prop_of thm)
36898
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
41123
boehmes
parents: 40579
diff changeset
    53
(* rules *)
36898
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
41123
boehmes
parents: 40579
diff changeset
    60
(* properties and term operations *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    62
val is_neg = (fn @{const Not} $ _ => true | _ => false)
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    63
fun is_neg' f = (fn @{const Not} $ t => f t | _ => false)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
val is_dneg = is_neg' is_neg
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    65
val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false)
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    66
val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false)
36898
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
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    69
    @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u)
36898
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
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    72
val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
val dest_disj_term =
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    74
  dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t)
36898
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
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
    85
val negate = Thm.apply (Thm.cterm_of @{context} @{const Not})
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
    86
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
41123
boehmes
parents: 40579
diff changeset
    89
(* proof tools *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
41123
boehmes
parents: 40579
diff changeset
    91
(** explosion of conjunctions and disjunctions **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
local
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    94
  val precomp = Old_Z3_Proof_Tools.precompose2
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
    95
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
  fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
    97
  val dest_conj1 = precomp destc @{thm conjunct1}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
    98
  val dest_conj2 = precomp destc @{thm conjunct2}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
  fun dest_conj_rules t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
    dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
    
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
  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
   103
  val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   104
  val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   105
  val dest_disj2 = precomp (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   106
  val dest_disj3 = precomp (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   107
  val dest_disj4 = precomp (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
  fun dest_disj_rules t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
    (case dest_disj_term' is_neg t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
      SOME (true, true) => SOME (dest_disj2, dest_disj4)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
    | SOME (true, false) => SOME (dest_disj2, dest_disj3)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
    | SOME (false, true) => SOME (dest_disj1, dest_disj4)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
    | SOME (false, false) => SOME (dest_disj1, dest_disj3)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
    | NONE => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
  fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   118
  val dneg_rule = Old_Z3_Proof_Tools.precompose destn @{thm notnotD}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
41123
boehmes
parents: 40579
diff changeset
   121
(*
boehmes
parents: 40579
diff changeset
   122
  explode a term into literals and collect all rules to be able to deduce
boehmes
parents: 40579
diff changeset
   123
  particular literals afterwards
boehmes
parents: 40579
diff changeset
   124
*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
fun explode_term is_conj =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
    val dest = if is_conj then dest_conj_term else dest_disj_term
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
    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
   129
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
    fun add (t, rs) = Termtab.map_default (t, rs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
      (fn rs' => if length rs' < length rs then rs' else rs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
    fun explode1 rules t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
      (case dest t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
        SOME (t1, t2) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
          let val (rule1, rule2) = the (dest_rules t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
          in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
            explode1 (rule1 :: rules) t1 #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
            explode1 (rule2 :: rules) t2 #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
            add (t, rev rules)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
          end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
      | NONE => add (t, rev rules))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   144
    fun explode0 (@{const Not} $ (@{const Not} $ t)) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
          Termtab.make [(t, [dneg_rule])]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
      | explode0 t = explode1 [] t Termtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
  in explode0 end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
41123
boehmes
parents: 40579
diff changeset
   150
(*
boehmes
parents: 40579
diff changeset
   151
  extract a literal by applying previously collected rules
boehmes
parents: 40579
diff changeset
   152
*)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   153
fun extract_lit thm rules = fold Old_Z3_Proof_Tools.compose rules thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
41123
boehmes
parents: 40579
diff changeset
   156
(*
boehmes
parents: 40579
diff changeset
   157
  explode a theorem into its literals
boehmes
parents: 40579
diff changeset
   158
*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
fun explode is_conj full keep_intermediate stop_lits =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
    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
   162
    val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
    fun explode1 thm =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   165
      if Termtab.defined tab (Old_SMT_Utils.prop_of thm) then cons thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
      else
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   167
        (case dest_rules (Old_SMT_Utils.prop_of thm) of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
          SOME (rule1, rule2) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
            explode2 rule1 thm #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
            explode2 rule2 thm #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
            keep_intermediate ? cons thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
        | NONE => cons 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
    and explode2 dest_rule thm =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   175
      if full orelse
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   176
        exists_lit is_conj (Termtab.defined tab) (Old_SMT_Utils.prop_of thm)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   177
      then explode1 (Old_Z3_Proof_Tools.compose dest_rule thm)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   178
      else cons (Old_Z3_Proof_Tools.compose dest_rule thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
    fun explode0 thm =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   181
      if not is_conj andalso is_dneg (Old_SMT_Utils.prop_of thm)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   182
      then [Old_Z3_Proof_Tools.compose dneg_rule thm]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
      else explode1 thm []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
  in explode0 end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
41123
boehmes
parents: 40579
diff changeset
   191
(** joining of literals to conjunctions or disjunctions **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
  fun on_cprem i f thm = f (Thm.cprem_of thm i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
  fun on_cprop f thm = f (Thm.cprop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
  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
   197
  fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   198
    Thm.instantiate ([],
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   199
      [(dest_Var (Thm.term_of cv1), on_cprop f thm1),
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   200
       (dest_Var (Thm.term_of cv2), on_cprop g thm2)]) rule
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   201
    |> Old_Z3_Proof_Tools.discharge thm1 |> Old_Z3_Proof_Tools.discharge thm2
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
  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
   204
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
  val conj_rule = precomp2 d1 d1 @{thm conjI}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
  fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2
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 disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
  val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
  val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
  val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
  fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
    | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
    | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
    | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   218
  fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
    | dest_conj t = raise TERM ("dest_conj", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   221
  val neg = (fn @{const Not} $ t => (true, t) | t => (false, @{const Not} $ t))
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   222
  fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
    | dest_disj t = raise TERM ("dest_disj", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   225
  val precomp = Old_Z3_Proof_Tools.precompose
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   226
  val dnegE = precomp (single o d2 o d1) @{thm notnotD}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   227
  val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast}
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   228
  fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   230
  val precomp2 = Old_Z3_Proof_Tools.precompose2
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
  fun dni f = apsnd f o Thm.dest_binop o f o d1
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   232
  val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   233
  val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   234
  val iff_const = @{const HOL.eq (bool)}
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   235
  fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) =
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   236
        f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
    | as_negIff _ _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
fun join is_conj littab t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
    val comp = if is_conj then comp_conj else comp_disj
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
    val dest = if is_conj then dest_conj else dest_disj
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
    val lookup = lookup_lit littab
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
    fun lookup_rule t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
      (case t of
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   249
        @{const Not} $ (@{const Not} $ t) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   250
          (Old_Z3_Proof_Tools.compose dnegI, lookup t)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   251
      | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   252
          (Old_Z3_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t))
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   253
      | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
          let fun rewr lit = lit COMP @{thm not_sym}
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   255
          in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
      | _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
          (case as_dneg lookup t of
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   258
            NONE => (Old_Z3_Proof_Tools.compose negIffE, as_negIff lookup t)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   259
          | x => (Old_Z3_Proof_Tools.compose dnegE, x)))
36898
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 join1 (s, t) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
      (case lookup t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
        SOME lit => (s, lit)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
      | NONE => 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
          (case lookup_rule t of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
            (rewrite, SOME lit) => (s, rewrite lit)
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58058
diff changeset
   267
          | (_, NONE) => (s, comp (apply2 join1 (dest t)))))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
  in snd (join1 (if is_conj then (false, t) else (true, t))) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
41123
boehmes
parents: 40579
diff changeset
   275
(** proving equality of conjunctions or disjunctions **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
  val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 41328
diff changeset
   281
  val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastforce}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
  val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
in
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   284
fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   285
fun contrapos2 prove (ct, cu) = prove (negate ct, Thm.dest_arg cu) COMP cp2
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   286
fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, negate cu) COMP cp3
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
  val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
  fun contra_left conj thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
    let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   294
      val rules = explode_term conj (Old_SMT_Utils.prop_of thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
      fun contra_lits (t, rs) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
        (case t of
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   297
          @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
        | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
    in
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   300
      (case Termtab.lookup rules @{const False} of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
        SOME rs => extract_lit thm rs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
      | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
          the (Termtab.get_first contra_lits rules)
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58058
diff changeset
   304
          |> apply2 (extract_lit thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
          |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   308
  val falseE_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
  fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
fun contradict conj ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   312
  iff_intro (Old_Z3_Proof_Tools.under_assumption (contra_left conj) ct)
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   313
    (contra_right ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
  fun prove_eq l r (cl, cr) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
      fun explode' is_conj = explode is_conj true (l <> r) []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   321
      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
   322
      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
   323
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   324
      val thm1 = Old_Z3_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   325
      val thm2 = Old_Z3_Proof_Tools.under_assumption (prove l cl o make_tab r) cr
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   326
    in iff_intro thm1 thm2 end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   327
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   328
  datatype conj_disj = CONJ | DISJ | NCON | NDIS
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
  fun kind_of t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   330
    if is_conj t then SOME CONJ
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
    else if is_disj t then SOME DISJ
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
    else if is_neg' is_conj t then SOME NCON
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   333
    else if is_neg' is_disj t then SOME NDIS
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
    else NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   337
fun prove_conj_disj_eq ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
  let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   339
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
    (case (kind_of (Thm.term_of cl), Thm.term_of cr) of
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   341
      (SOME CONJ, @{const False}) => contradict true cl
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   342
    | (SOME DISJ, @{const Not} $ @{const False}) =>
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 38864
diff changeset
   343
        contrapos2 (contradict false o fst) cp
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   344
    | (kl, _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
        (case (kl, kind_of (Thm.term_of cr)) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
          (SOME CONJ, SOME CONJ) => prove_eq true true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
        | (SOME CONJ, SOME NDIS) => prove_eq true false cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   348
        | (SOME CONJ, _) => prove_eq true true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
        | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
        | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
        | (SOME DISJ, _) => contrapos1 (prove_eq false false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
        | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
        | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   354
        | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   355
        | (SOME NDIS, SOME NDIS) => prove_eq false false cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   356
        | (SOME NDIS, SOME CONJ) => prove_eq false true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   357
        | (SOME NDIS, NONE) => prove_eq false true cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   358
        | _ => raise CTERM ("prove_conj_disj_eq", [ct])))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   359
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   360
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   362
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   363
end