# HG changeset patch
# User boehmes
# Date 1421447011 -3600
# Node ID de4218223e009c4c18d0b0e52220c753576a7d98
# Parent  c7f6f01ede154ed513f7170beadabc6a48d15666
more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT

diff -r c7f6f01ede15 -r de4218223e00 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/HOL/SMT.thy	Fri Jan 16 23:23:31 2015 +0100
@@ -163,9 +163,9 @@
 ML_file "Tools/SMT/verit_proof.ML"
 ML_file "Tools/SMT/verit_isar.ML"
 ML_file "Tools/SMT/verit_proof_parse.ML"
+ML_file "Tools/SMT/conj_disj_perm.ML"
 ML_file "Tools/SMT/z3_interface.ML"
 ML_file "Tools/SMT/z3_replay_util.ML"
-ML_file "Tools/SMT/z3_replay_literals.ML"
 ML_file "Tools/SMT/z3_replay_rules.ML"
 ML_file "Tools/SMT/z3_replay_methods.ML"
 ML_file "Tools/SMT/z3_replay.ML"
diff -r c7f6f01ede15 -r de4218223e00 src/HOL/Tools/SMT/conj_disj_perm.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/conj_disj_perm.ML	Fri Jan 16 23:23:31 2015 +0100
@@ -0,0 +1,127 @@
+(*  Title:      HOL/Tools/SMT/conj_disj_perm.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Tactic to prove equivalence of permutations of conjunctions and disjunctions.
+*)
+
+signature CONJ_DISJ_PERM =
+sig
+  val conj_disj_perm_tac: int -> tactic
+end
+
+structure Conj_Disj_Perm: CONJ_DISJ_PERM =
+struct
+
+fun with_assumption ct f =
+  let val ct' = Thm.apply @{cterm HOL.Trueprop} ct
+  in Thm.implies_intr ct' (f (Thm.assume ct')) end
+
+fun eq_from_impls thm1 thm2 = thm2 INCR_COMP (thm1 INCR_COMP @{thm iffI})
+
+fun add_lit thm = Termtab.update (HOLogic.dest_Trueprop (Thm.prop_of thm), thm)
+
+val ndisj1_rule = @{lemma "~(P | Q) ==> ~P" by auto}
+val ndisj2_rule = @{lemma "~(P | Q) ==> ~Q" by auto}
+
+fun explode_thm thm =
+  (case HOLogic.dest_Trueprop (Thm.prop_of thm) of
+    @{const HOL.conj} $ _ $ _ => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
+  | @{const HOL.Not} $ (@{const HOL.disj} $ _ $ _) => explode_conj_thm ndisj1_rule ndisj2_rule thm
+  | @{const HOL.Not} $ (@{const HOL.Not} $ _) => explode_thm (thm RS @{thm notnotD})
+  | _ => add_lit thm)
+
+and explode_conj_thm rule1 rule2 thm lits =
+  explode_thm (thm RS rule1) (explode_thm (thm RS rule2) (add_lit thm lits))
+
+val not_false_rule = @{lemma "~False" by auto}
+fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty))
+
+fun find_dual_lit lits (@{const HOL.Not} $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm)
+  | find_dual_lit _ _ = NONE
+
+fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits
+
+val not_not_rule = @{lemma "P ==> ~~P" by auto}
+val ndisj_rule = @{lemma "~P ==> ~Q ==> ~(P | Q)" by auto}
+
+fun join lits t =
+  (case Termtab.lookup lits t of
+    SOME thm => thm
+  | NONE => join_term lits t)
+
+and join_term lits (@{const HOL.conj} $ t $ u) = @{thm conjI} OF (map (join lits) [t, u])
+  | join_term lits (@{const HOL.Not} $ (@{const HOL.disj} $ t $ u)) =
+      ndisj_rule OF (map (join lits o HOLogic.mk_not) [t, u])
+  | join_term lits (@{const HOL.Not} $ (@{const HOL.Not} $ t)) = join lits t RS not_not_rule
+  | join_term _ t = raise TERM ("join_term", [t])
+
+fun prove_conj_disj_imp ct cu = with_assumption ct (fn thm => join (explode thm) (Thm.term_of cu))
+
+fun prove_conj_disj_eq (clhs, crhs) =
+  let
+    val thm1 = prove_conj_disj_imp clhs crhs
+    val thm2 = prove_conj_disj_imp crhs clhs
+  in eq_from_impls thm1 thm2 end
+
+val not_not_false_rule = @{lemma "~~False ==> P" by auto}
+val not_true_rule = @{lemma "~True ==> P" by auto}
+
+fun prove_any_imp ct =
+  (case Thm.term_of ct of
+    @{const HOL.False} => @{thm FalseE}
+  | @{const HOL.Not} $ (@{const HOL.Not} $ @{const HOL.False}) => not_not_false_rule
+  | @{const HOL.Not} $ @{const HOL.True} => not_true_rule
+  | _ => raise CTERM ("prove_any_imp", [ct]))
+
+fun prove_contradiction_imp ct =
+  with_assumption ct (fn thm =>
+    let val lits = explode thm
+    in
+      (case Termtab.lookup lits @{const HOL.False} of
+        SOME thm' => thm' RS @{thm FalseE}
+      | NONE =>
+          (case Termtab.lookup lits (@{const HOL.Not} $ @{const HOL.True}) of
+            SOME thm' => thm' RS not_true_rule
+          | NONE =>
+              (case find_dual_lits lits of
+                SOME (not_lit_thm, lit_thm) => @{thm notE} OF [not_lit_thm, lit_thm]
+              | NONE => raise CTERM ("prove_contradiction", [ct]))))
+    end)
+
+fun prove_contradiction_eq to_right (clhs, crhs) =
+  let
+    val thm1 = if to_right then prove_contradiction_imp clhs else prove_any_imp clhs
+    val thm2 = if to_right then prove_any_imp crhs else prove_contradiction_imp crhs
+  in eq_from_impls thm1 thm2 end
+
+val contrapos_rule = @{lemma "(~P) = (~Q) ==> P = Q" by auto}
+fun contrapos prove cp = contrapos_rule OF [prove (apply2 (Thm.apply @{cterm HOL.Not}) cp)]
+
+datatype kind = True | False | Conj | Disj | Other
+
+fun choose t _ _ _ @{const HOL.True} = t
+  | choose _ f _ _ @{const HOL.False} = f
+  | choose _ _ c _ (@{const HOL.conj} $ _ $ _) = c
+  | choose _ _ _ d (@{const HOL.disj} $ _ $ _) = d
+  | choose _ _ _ _ _ = Other
+
+fun kind_of (@{const HOL.Not} $ t) = choose False True Disj Conj t
+  | kind_of t = choose True False Conj Disj t
+
+fun prove_conj_disj_perm ct cp =
+  (case apply2 (kind_of o Thm.term_of) cp of
+    (Conj, Conj) => prove_conj_disj_eq cp
+  | (Disj, Disj) => contrapos prove_conj_disj_eq cp
+  | (Conj, False) => prove_contradiction_eq true cp
+  | (False, Conj) => prove_contradiction_eq false cp
+  | (Disj, True) => contrapos (prove_contradiction_eq true) cp
+  | (True, Disj) => contrapos (prove_contradiction_eq false) cp
+  | _ => raise CTERM ("prove_conj_disj_perm", [ct]))
+
+val conj_disj_perm_tac = CSUBGOAL (fn (ct, i) => 
+  (case Thm.term_of ct of
+    @{const HOL.Trueprop} $ (@{const HOL.eq(bool)} $ _ $ _) =>
+      rtac (prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))) i
+  | _ => no_tac))
+
+end
diff -r c7f6f01ede15 -r de4218223e00 src/HOL/Tools/SMT/z3_replay.ML
--- a/src/HOL/Tools/SMT/z3_replay.ML	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML	Fri Jan 16 23:23:31 2015 +0100
@@ -83,7 +83,8 @@
   fun rewrite_conv _ [] = Conv.all_conv
     | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
 
-  val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, Z3_Replay_Literals.rewrite_true]
+  val rewrite_true_rule = @{lemma "True == ~ False" by simp}
+  val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, rewrite_true_rule]
 
   fun rewrite _ [] = I
     | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
@@ -95,7 +96,7 @@
 
 fun add_asserted outer_ctxt rewrite_rules assms steps ctxt =
   let
-    val eqs = map (rewrite ctxt [Z3_Replay_Literals.rewrite_true]) rewrite_rules
+    val eqs = map (rewrite ctxt [rewrite_true_rule]) rewrite_rules
     val eqs' = union Thm.eq_thm eqs prep_rules
 
     val assms_net =
@@ -154,8 +155,8 @@
 
 end
 
-fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, @{thm reflexive},
-  Z3_Replay_Literals.true_thm]
+val true_thm = @{lemma "~False" by simp}
+fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, @{thm reflexive}, true_thm]
 
 val intro_def_rules = @{lemma
   "(~ P | P) & (P | ~ P)"
diff -r c7f6f01ede15 -r de4218223e00 src/HOL/Tools/SMT/z3_replay_literals.ML
--- a/src/HOL/Tools/SMT/z3_replay_literals.ML	Thu Jan 15 13:39:41 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-(*  Title:      HOL/Tools/SMT/z3_replay_literals.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Proof tools related to conjunctions and disjunctions.
-*)
-
-signature Z3_REPLAY_LITERALS =
-sig
-  (*literal table*)
-  type littab = thm Termtab.table
-  val make_littab: thm list -> littab
-  val insert_lit: thm -> littab -> littab
-  val delete_lit: thm -> littab -> littab
-  val lookup_lit: littab -> term -> thm option
-  val get_first_lit: (term -> bool) -> littab -> thm option
-
-  (*rules*)
-  val true_thm: thm
-  val rewrite_true: thm
-
-  (*properties*)
-  val is_conj: term -> bool
-  val is_disj: term -> bool
-  val exists_lit: bool -> (term -> bool) -> term -> bool
-  val negate: cterm -> cterm
-
-  (*proof tools*)
-  val explode: bool -> bool -> bool -> term list -> thm -> thm list
-  val join: bool -> littab -> term -> thm
-  val prove_conj_disj_eq: cterm -> thm
-end;
-
-structure Z3_Replay_Literals: Z3_REPLAY_LITERALS =
-struct
-
-(* literal table *)
-
-type littab = thm Termtab.table
-
-fun make_littab thms = fold (Termtab.update o `SMT_Util.prop_of) thms Termtab.empty
-
-fun insert_lit thm = Termtab.update (`SMT_Util.prop_of thm)
-fun delete_lit thm = Termtab.delete (SMT_Util.prop_of thm)
-fun lookup_lit lits = Termtab.lookup lits
-fun get_first_lit f =
-  Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
-
-
-(* rules *)
-
-val true_thm = @{lemma "~False" by simp}
-val rewrite_true = @{lemma "True == ~ False" by simp}
-
-
-(* properties and term operations *)
-
-val is_neg = (fn @{const Not} $ _ => true | _ => false)
-fun is_neg' f = (fn @{const Not} $ t => f t | _ => false)
-val is_dneg = is_neg' is_neg
-val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false)
-
-fun dest_disj_term' f = (fn
-    @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u)
-  | _ => NONE)
-
-val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
-val dest_disj_term =
-  dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t)
-
-fun exists_lit is_conj P =
-  let
-    val dest = if is_conj then dest_conj_term else dest_disj_term
-    fun exists t = P t orelse
-      (case dest t of
-        SOME (t1, t2) => exists t1 orelse exists t2
-      | NONE => false)
-  in exists end
-
-val negate = Thm.apply (Thm.cterm_of @{theory} @{const Not})
-
-
-(* proof tools *)
-
-(** explosion of conjunctions and disjunctions **)
-
-local
-  val precomp = Z3_Replay_Util.precompose2
-
-  fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
-  val dest_conj1 = precomp destc @{thm conjunct1}
-  val dest_conj2 = precomp destc @{thm conjunct2}
-  fun dest_conj_rules t =
-    dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
-
-  fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct)))
-  val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
-  val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
-  val dest_disj2 = precomp (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
-  val dest_disj3 = precomp (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
-  val dest_disj4 = precomp (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
-
-  fun dest_disj_rules t =
-    (case dest_disj_term' is_neg t of
-      SOME (true, true) => SOME (dest_disj2, dest_disj4)
-    | SOME (true, false) => SOME (dest_disj2, dest_disj3)
-    | SOME (false, true) => SOME (dest_disj1, dest_disj4)
-    | SOME (false, false) => SOME (dest_disj1, dest_disj3)
-    | NONE => NONE)
-
-  fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
-  val dneg_rule = Z3_Replay_Util.precompose destn @{thm notnotD}
-in
-
-(*
-  explode a term into literals and collect all rules to be able to deduce
-  particular literals afterwards
-*)
-fun explode_term is_conj =
-  let
-    val dest = if is_conj then dest_conj_term else dest_disj_term
-    val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
-
-    fun add (t, rs) = Termtab.map_default (t, rs)
-      (fn rs' => if length rs' < length rs then rs' else rs)
-
-    fun explode1 rules t =
-      (case dest t of
-        SOME (t1, t2) =>
-          let val (rule1, rule2) = the (dest_rules t)
-          in
-            explode1 (rule1 :: rules) t1 #>
-            explode1 (rule2 :: rules) t2 #>
-            add (t, rev rules)
-          end
-      | NONE => add (t, rev rules))
-
-    fun explode0 (@{const Not} $ (@{const Not} $ t)) =
-          Termtab.make [(t, [dneg_rule])]
-      | explode0 t = explode1 [] t Termtab.empty
-
-  in explode0 end
-
-(*
-  extract a literal by applying previously collected rules
-*)
-fun extract_lit thm rules = fold Z3_Replay_Util.compose rules thm
-
-
-(*
-  explode a theorem into its literals
-*)
-fun explode is_conj full keep_intermediate stop_lits =
-  let
-    val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
-    val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
-
-    fun explode1 thm =
-      if Termtab.defined tab (SMT_Util.prop_of thm) then cons thm
-      else
-        (case dest_rules (SMT_Util.prop_of thm) of
-          SOME (rule1, rule2) =>
-            explode2 rule1 thm #>
-            explode2 rule2 thm #>
-            keep_intermediate ? cons thm
-        | NONE => cons thm)
-
-    and explode2 dest_rule thm =
-      if full orelse
-        exists_lit is_conj (Termtab.defined tab) (SMT_Util.prop_of thm)
-      then explode1 (Z3_Replay_Util.compose dest_rule thm)
-      else cons (Z3_Replay_Util.compose dest_rule thm)
-
-    fun explode0 thm =
-      if not is_conj andalso is_dneg (SMT_Util.prop_of thm)
-      then [Z3_Replay_Util.compose dneg_rule thm]
-      else explode1 thm []
-
-  in explode0 end
-
-end
-
-
-(** joining of literals to conjunctions or disjunctions **)
-
-local
-  fun on_cprem i f thm = f (Thm.cprem_of thm i)
-  fun on_cprop f thm = f (Thm.cprop_of thm)
-  fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
-  fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
-    Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
-    |> Z3_Replay_Util.discharge thm1 |> Z3_Replay_Util.discharge thm2
-
-  fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
-
-  val conj_rule = precomp2 d1 d1 @{thm conjI}
-  fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2
-
-  val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast}
-  val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast}
-  val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast}
-  val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast}
-
-  fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2
-    | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2
-    | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
-    | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
-
-  fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u))
-    | dest_conj t = raise TERM ("dest_conj", [t])
-
-  val neg = (fn @{const Not} $ t => (true, t) | t => (false, @{const Not} $ t))
-  fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
-    | dest_disj t = raise TERM ("dest_disj", [t])
-
-  val precomp = Z3_Replay_Util.precompose
-  val dnegE = precomp (single o d2 o d1) @{thm notnotD}
-  val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast}
-  fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
-
-  val precomp2 = Z3_Replay_Util.precompose2
-  fun dni f = apsnd f o Thm.dest_binop o f o d1
-  val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
-  val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
-  val iff_const = @{const HOL.eq (bool)}
-  fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) =
-        f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t)))
-    | as_negIff _ _ = NONE
-in
-
-fun join is_conj littab t =
-  let
-    val comp = if is_conj then comp_conj else comp_disj
-    val dest = if is_conj then dest_conj else dest_disj
-
-    val lookup = lookup_lit littab
-
-    fun lookup_rule t =
-      (case t of
-        @{const Not} $ (@{const Not} $ t) => (Z3_Replay_Util.compose dnegI, lookup t)
-      | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
-          (Z3_Replay_Util.compose negIffI, lookup (iff_const $ u $ t))
-      | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
-          let fun rewr lit = lit COMP @{thm not_sym}
-          in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
-      | _ =>
-          (case as_dneg lookup t of
-            NONE => (Z3_Replay_Util.compose negIffE, as_negIff lookup t)
-          | x => (Z3_Replay_Util.compose dnegE, x)))
-
-    fun join1 (s, t) =
-      (case lookup t of
-        SOME lit => (s, lit)
-      | NONE =>
-          (case lookup_rule t of
-            (rewrite, SOME lit) => (s, rewrite lit)
-          | (_, NONE) => (s, comp (apply2 join1 (dest t)))))
-
-  in snd (join1 (if is_conj then (false, t) else (true, t))) end
-
-end
-
-
-(** proving equality of conjunctions or disjunctions **)
-
-fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})
-
-local
-  val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
-  val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastforce}
-  val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
-in
-fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1
-fun contrapos2 prove (ct, cu) = prove (negate ct, Thm.dest_arg cu) COMP cp2
-fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, negate cu) COMP cp3
-end
-
-local
-  val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
-  fun contra_left conj thm =
-    let
-      val rules = explode_term conj (SMT_Util.prop_of thm)
-      fun contra_lits (t, rs) =
-        (case t of
-          @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
-        | _ => NONE)
-    in
-      (case Termtab.lookup rules @{const False} of
-        SOME rs => extract_lit thm rs
-      | NONE =>
-          the (Termtab.get_first contra_lits rules)
-          |> apply2 (extract_lit thm)
-          |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
-    end
-
-  val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
-  fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
-in
-
-fun contradict conj ct =
-  iff_intro (Z3_Replay_Util.under_assumption (contra_left conj) ct) (contra_right ct)
-
-end
-
-local
-  fun prove_eq l r (cl, cr) =
-    let
-      fun explode' is_conj = explode is_conj true (l <> r) []
-      fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
-      fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
-
-      val thm1 = Z3_Replay_Util.under_assumption (prove r cr o make_tab l) cl
-      val thm2 = Z3_Replay_Util.under_assumption (prove l cl o make_tab r) cr
-    in iff_intro thm1 thm2 end
-
-  datatype conj_disj = CONJ | DISJ | NCON | NDIS
-  fun kind_of t =
-    if is_conj t then SOME CONJ
-    else if is_disj t then SOME DISJ
-    else if is_neg' is_conj t then SOME NCON
-    else if is_neg' is_disj t then SOME NDIS
-    else NONE
-in
-
-fun prove_conj_disj_eq ct =
-  let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
-  in
-    (case (kind_of (Thm.term_of cl), Thm.term_of cr) of
-      (SOME CONJ, @{const False}) => contradict true cl
-    | (SOME DISJ, @{const Not} $ @{const False}) =>
-        contrapos2 (contradict false o fst) cp
-    | (kl, _) =>
-        (case (kl, kind_of (Thm.term_of cr)) of
-          (SOME CONJ, SOME CONJ) => prove_eq true true cp
-        | (SOME CONJ, SOME NDIS) => prove_eq true false cp
-        | (SOME CONJ, _) => prove_eq true true cp
-        | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
-        | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
-        | (SOME DISJ, _) => contrapos1 (prove_eq false false) cp
-        | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
-        | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
-        | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
-        | (SOME NDIS, SOME NDIS) => prove_eq false false cp
-        | (SOME NDIS, SOME CONJ) => prove_eq false true cp
-        | (SOME NDIS, NONE) => prove_eq false true cp
-        | _ => raise CTERM ("prove_conj_disj_eq", [ct])))
-  end
-
-end
-
-end;
diff -r c7f6f01ede15 -r de4218223e00 src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri Jan 16 23:23:31 2015 +0100
@@ -447,8 +447,11 @@
     CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt)))
     THEN' rtac @{thm refl})
 
+fun prove_conj_disj_perm ctxt t = prove ctxt t (fn _ => Conj_Disj_Perm.conj_disj_perm_tac)
+
 fun rewrite ctxt _ = try_provers ctxt Z3_Proof.Rewrite [
   ("rules", apply_rule ctxt),
+  ("conj_disj_perm", prove_conj_disj_perm ctxt),
   ("prop_rewrite", prove_prop_rewrite ctxt),
   ("arith_rewrite", focus_eq prove_arith_rewrite ctxt),
   ("if_rewrite", lift_ite_rewrite ctxt)] []