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