src/HOL/Tools/SMT/z3_proof_literals.ML

 end
 
 structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
 struct
 
-structure U = SMT_Utils
-structure T = Z3_Proof_Tools
-
 
 
 (* literal table *)
 
 type littab = thm Termtab.table
 
-fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty
-
-fun insert_lit thm = Termtab.update (`U.prop_of thm)
-fun delete_lit thm = Termtab.delete (U.prop_of thm)
+fun make_littab thms =
+  fold (Termtab.update o `SMT_Utils.prop_of) thms Termtab.empty
+
+fun insert_lit thm = Termtab.update (`SMT_Utils.prop_of thm)
+fun delete_lit thm = Termtab.delete (SMT_Utils.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)
 
 

 (* proof tools *)
 
 (** explosion of conjunctions and disjunctions **)
 
 local
+  val precomp = Z3_Proof_Tools.precompose2
+
   fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
-  val dest_conj1 = T.precompose2 destc @{thm conjunct1}
-  val dest_conj2 = T.precompose2 destc @{thm conjunct2}
+  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 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
-  val dest_disj2 = T.precompose2 (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
-  val dest_disj3 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
-  val dest_disj4 = T.precompose2 (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
+  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 = T.precompose destn @{thm notnotD}
+  val dneg_rule = Z3_Proof_Tools.precompose destn @{thm notnotD}
 in
 
 (*
   explode a term into literals and collect all rules to be able to deduce
   particular literals afterwards

   in explode0 end
 
 (*
   extract a literal by applying previously collected rules
 *)
-fun extract_lit thm rules = fold T.compose rules thm
+fun extract_lit thm rules = fold Z3_Proof_Tools.compose rules thm
 
 
 (*
   explode a theorem into its literals
 *)

   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 (U.prop_of thm) then cons thm
+      if Termtab.defined tab (SMT_Utils.prop_of thm) then cons thm
       else
-        (case dest_rules (U.prop_of thm) of
+        (case dest_rules (SMT_Utils.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) (U.prop_of thm)
-      then explode1 (T.compose dest_rule thm)
-      else cons (T.compose dest_rule thm)
+      if full orelse
+        exists_lit is_conj (Termtab.defined tab) (SMT_Utils.prop_of thm)
+      then explode1 (Z3_Proof_Tools.compose dest_rule thm)
+      else cons (Z3_Proof_Tools.compose dest_rule thm)
 
     fun explode0 thm =
-      if not is_conj andalso is_dneg (U.prop_of thm)
-      then [T.compose dneg_rule thm]
+      if not is_conj andalso is_dneg (SMT_Utils.prop_of thm)
+      then [Z3_Proof_Tools.compose dneg_rule thm]
       else explode1 thm []
 
   in explode0 end
 
 end

   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
-    |> T.discharge thm1 |> T.discharge thm2
+    |> Z3_Proof_Tools.discharge thm1 |> Z3_Proof_Tools.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 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 dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
-  val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
+  val precomp = Z3_Proof_Tools.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_Proof_Tools.precompose2
   fun dni f = apsnd f o Thm.dest_binop o f o d1
-  val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
-  val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
+  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

 
     val lookup = lookup_lit littab
 
     fun lookup_rule t =
       (case t of
-        @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t)
+        @{const Not} $ (@{const Not} $ t) =>
+          (Z3_Proof_Tools.compose dnegI, lookup t)
       | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
-            (T.compose negIffI, lookup (iff_const $ u $ t))
+          (Z3_Proof_Tools.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 => (T.compose negIffE, as_negIff lookup t)
-          | x => (T.compose dnegE, x)))
+            NONE => (Z3_Proof_Tools.compose negIffE, as_negIff lookup t)
+          | x => (Z3_Proof_Tools.compose dnegE, x)))
 
     fun join1 (s, t) =
       (case lookup t of
         SOME lit => (s, lit)
       | NONE => 

 
 local
   val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
   fun contra_left conj thm =
     let
-      val rules = explode_term conj (U.prop_of thm)
+      val rules = explode_term conj (SMT_Utils.prop_of thm)
       fun contra_lits (t, rs) =
         (case t of
           @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
         | _ => NONE)
     in

 
   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 (T.under_assumption (contra_left conj) ct) (contra_right ct)
+  iff_intro (Z3_Proof_Tools.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 = T.under_assumption (prove r cr o make_tab l) cl
-      val thm2 = T.under_assumption (prove l cl o make_tab r) cr
+      val thm1 = Z3_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
+      val thm2 = Z3_Proof_Tools.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