# HG changeset patch
# User blanchet
# Date 1402527649 -7200
# Node ID ec5ff6bb2a92440cd932e5ac75ddda31d77b7fa3
# Parent  489083abce44a51043ad64378d67c696a756ca87
eliminate dependency of SMT2 module on 'list'

diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT2.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -5,15 +5,10 @@
 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *}
 
 theory SMT2
-imports List
+imports Divides
 keywords "smt2_status" :: diag
 begin
 
-ML_file "Tools/SMT2/smt2_util.ML"
-ML_file "Tools/SMT2/smt2_failure.ML"
-ML_file "Tools/SMT2/smt2_config.ML"
-
-
 subsection {* Triggers for quantifier instantiation *}
 
 text {*
@@ -31,13 +26,20 @@
 quantifier block.
 *}
 
+typedecl 'a symb_list
+
+consts
+  Symb_Nil :: "'a symb_list"
+  Symb_Cons :: "'a \<Rightarrow> 'a symb_list \<Rightarrow> 'a symb_list"
+
 typedecl pattern
 
 consts
   pat :: "'a \<Rightarrow> pattern"
   nopat :: "'a \<Rightarrow> pattern"
 
-definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P"
+definition trigger :: "pattern symb_list symb_list \<Rightarrow> bool \<Rightarrow> bool" where
+  "trigger _ P = P"
 
 
 subsection {* Higher-order encoding *}
@@ -68,8 +70,8 @@
 lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
 lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
 
-lemma nat_zero_as_int: "0 = nat 0" by (rule transfer_nat_int_numerals(1))
-lemma nat_one_as_int: "1 = nat 1" by (rule transfer_nat_int_numerals(2))
+lemma nat_zero_as_int: "0 = nat 0" by simp
+lemma nat_one_as_int: "1 = nat 1" by simp
 lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
 lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
 lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a <= int b)" by simp
@@ -116,6 +118,9 @@
 
 subsection {* Setup *}
 
+ML_file "Tools/SMT2/smt2_util.ML"
+ML_file "Tools/SMT2/smt2_failure.ML"
+ML_file "Tools/SMT2/smt2_config.ML"
 ML_file "Tools/SMT2/smt2_builtin.ML"
 ML_file "Tools/SMT2/smt2_datatypes.ML"
 ML_file "Tools/SMT2/smt2_normalize.ML"
@@ -355,7 +360,7 @@
   "0 * x = 0"
   "1 * x = x"
   "x + y = y + x"
-  by auto
+  by (auto simp add: mult_2)
 
 lemma [z3_new_rule]:  (* for def-axiom *)
   "P = Q \<or> P \<or> Q"
@@ -386,8 +391,7 @@
   "(if P then Q else \<not> R) \<or> P \<or> R"
   by auto
 
-hide_type (open) pattern
-hide_const fun_app z3div z3mod
-hide_const (open) trigger pat nopat
+hide_type (open) symb_list pattern
+hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod
 
 end
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/smt2_builtin.ML
--- a/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -50,7 +50,7 @@
 
 datatype ('a, 'b) kind = Ext of 'a | Int of 'b
 
-type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict 
+type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict
 
 fun typ_ord ((T, _), (U, _)) =
   let
@@ -120,7 +120,7 @@
 fun dest_builtin_typ ctxt T =
   (case lookup_builtin_typ ctxt T of
     SOME (_, Int (f, _)) => f T
-  | _ => NONE) 
+  | _ => NONE)
 
 fun is_builtin_typ_ext ctxt T =
   (case lookup_builtin_typ ctxt T of
@@ -205,7 +205,7 @@
     | NONE => dest_builtin_fun ctxt c ts)
   end
 
-fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
+fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =
   (case lookup_builtin_fun ctxt c of
     SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
   | SOME (_, Ext f) => SOME (f ctxt T ts)
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/smt2_config.ML
--- a/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -220,7 +220,7 @@
     val ns = if null names then ["(none)"] else sort_strings names
     val n = the_default "(none)" (solver_name_of ctxt)
     val opts = solver_options_of ctxt
-    
+
     val t = string_of_real (Config.get ctxt timeout)
 
     val certs_filename =
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/smt2_normalize.ML
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -29,7 +29,7 @@
 (* general theorem normalizations *)
 
 (** instantiate elimination rules **)
- 
+
 local
   val (cpfalse, cfalse) = `SMT2_Util.mk_cprop (Thm.cterm_of @{theory} @{const False})
 
@@ -113,8 +113,8 @@
 
   fun proper_trigger t =
     t
-    |> these o try HOLogic.dest_list
-    |> map (map_filter dest_trigger o these o try HOLogic.dest_list)
+    |> these o try SMT2_Util.dest_symb_list
+    |> map (map_filter dest_trigger o these o try SMT2_Util.dest_symb_list)
     |> (fn [] => false | bss => forall eq_list bss)
 
   fun proper_quant inside f t =
@@ -185,16 +185,17 @@
             Pattern.matches thy (t', u) andalso not (t aconv u))
         in not (Term.exists_subterm some_match u) end
 
-  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Util.destT1
+  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name pat} SMT2_Util.destT1
   fun mk_pat ct = Thm.apply (SMT2_Util.instT' ct pat) ct
 
-  fun mk_clist T = pairself (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T)
+  fun mk_clist T =
+    pairself (Thm.cterm_of @{theory}) (SMT2_Util.symb_cons_const T, SMT2_Util.symb_nil_const T)
   fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
-  val mk_pat_list = mk_list (mk_clist @{typ SMT2.pattern})
-  val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})  
+  val mk_pat_list = mk_list (mk_clist @{typ pattern})
+  val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
   fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
 
-  val trigger_eq = mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)}
+  val trigger_eq = mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)}
 
   fun insert_trigger_conv [] ct = Conv.all_conv ct
     | insert_trigger_conv ctss ct =
@@ -216,7 +217,7 @@
 
     in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
 
-  fun has_trigger (@{const SMT2.trigger} $ _ $ _) = true
+  fun has_trigger (@{const trigger} $ _ $ _) = true
     | has_trigger _ = false
 
   fun try_trigger_conv cv ct =
@@ -234,7 +235,7 @@
 
 val setup_trigger =
   fold SMT2_Builtin.add_builtin_fun_ext''
-    [@{const_name SMT2.pat}, @{const_name SMT2.nopat}, @{const_name SMT2.trigger}]
+    [@{const_name pat}, @{const_name nopat}, @{const_name trigger}]
 
 end
 
@@ -317,7 +318,7 @@
 
 fun unfold_abs_min_max_conv ctxt =
   SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
-  
+
 val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table
 
 end
@@ -481,18 +482,17 @@
 
   val schematic_consts_of =
     let
-      fun collect (@{const SMT2.trigger} $ p $ t) =
-            collect_trigger p #> collect t
+      fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
         | collect (t $ u) = collect t #> collect u
         | collect (Abs (_, _, t)) = collect t
-        | collect (t as Const (n, _)) = 
+        | collect (t as Const (n, _)) =
             if not (ignored n) then Monomorph.add_schematic_consts_of t else I
         | collect _ = I
       and collect_trigger t =
-        let val dest = these o try HOLogic.dest_list 
+        let val dest = these o try SMT2_Util.dest_symb_list
         in fold (fold collect_pat o dest) (dest t) end
-      and collect_pat (Const (@{const_name SMT2.pat}, _) $ t) = collect t
-        | collect_pat (Const (@{const_name SMT2.nopat}, _) $ t) = collect t
+      and collect_pat (Const (@{const_name pat}, _) $ t) = collect t
+        | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t
         | collect_pat _ = I
     in (fn t => collect t Symtab.empty) end
 in
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/smt2_translate.ML
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -104,7 +104,7 @@
 fun add_fun t sort (cx as (names, typs, terms)) =
   (case Termtab.lookup terms t of
     SOME (name, _) => (name, cx)
-  | NONE => 
+  | NONE =>
       let
         val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix
         val (name, names') = Name.variant sugg names
@@ -214,7 +214,7 @@
           | (u, ts) => Term.list_comb (u, map expand ts))
 
     and abs_expand (n, T, t) = Abs (n, T, expand t)
-  
+
   in map expand end
 
 end
@@ -246,7 +246,7 @@
       val (Ts, T) = Term.strip_type (Term.type_of t)
     in find_min 0 (take i (rev Ts)) T end
 
-  fun app u (t, T) = (Const (@{const_name SMT2.fun_app}, T --> T) $ t $ u, Term.range_type T)
+  fun app u (t, T) = (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T)
 
   fun apply i t T ts =
     let
@@ -264,7 +264,7 @@
       if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
       else apply (the (Termtab.lookup arities' t)) t T ts
 
-    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
+    fun in_list T f t = SMT2_Util.mk_symb_list T (map f (SMT2_Util.dest_symb_list t))
 
     fun traverse Ts t =
       (case Term.strip_comb t of
@@ -286,17 +286,17 @@
       | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
       | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
       | (u, ts) => traverses Ts u ts)
-    and in_trigger Ts ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
+    and in_trigger Ts ((c as @{const trigger}) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
       | in_trigger Ts t = traverse Ts t
     and in_pats Ts ps =
-      in_list @{typ "SMT2.pattern list"} (in_list @{typ SMT2.pattern} (in_pat Ts)) ps
-    and in_pat Ts ((p as Const (@{const_name SMT2.pat}, _)) $ t) = p $ traverse Ts t
-      | in_pat Ts ((p as Const (@{const_name SMT2.nopat}, _)) $ t) = p $ traverse Ts t
+      in_list @{typ "pattern symb_list"} (in_list @{typ pattern} (in_pat Ts)) ps
+    and in_pat Ts ((p as Const (@{const_name pat}, _)) $ t) = p $ traverse Ts t
+      | in_pat Ts ((p as Const (@{const_name nopat}, _)) $ t) = p $ traverse Ts t
       | in_pat _ t = raise TERM ("bad pattern", [t])
     and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
   in map (traverse []) ts end
 
-val fun_app_eq = mk_meta_eq @{thm SMT2.fun_app_def}
+val fun_app_eq = mk_meta_eq @{thm fun_app_def}
 
 end
 
@@ -323,7 +323,7 @@
 
 fun folify ctxt =
   let
-    fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t))
+    fun in_list T f t = SMT2_Util.mk_symb_list T (map_filter f (SMT2_Util.dest_symb_list t))
 
     fun in_term pat t =
       (case Term.strip_comb t of
@@ -338,16 +338,16 @@
       | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
       | _ => t)
 
-    and in_pat ((p as Const (@{const_name SMT2.pat}, _)) $ t) =
+    and in_pat ((p as Const (@{const_name pat}, _)) $ t) =
           p $ in_term true t
-      | in_pat ((p as Const (@{const_name SMT2.nopat}, _)) $ t) =
+      | in_pat ((p as Const (@{const_name nopat}, _)) $ t) =
           p $ in_term true t
       | in_pat t = raise TERM ("bad pattern", [t])
 
     and in_pats ps =
-      in_list @{typ "SMT2.pattern list"} (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps
+      in_list @{typ "pattern symb_list"} (SOME o in_list @{typ pattern} (try in_pat)) ps
 
-    and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_form t
+    and in_trigger ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
       | in_trigger t = in_form t
 
     and in_form t =
@@ -384,8 +384,8 @@
       if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
   | group_quant _ Ts t = (Ts, t)
 
-fun dest_pat (Const (@{const_name SMT2.pat}, _) $ t) = (t, true)
-  | dest_pat (Const (@{const_name SMT2.nopat}, _) $ t) = (t, false)
+fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
+  | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
   | dest_pat t = raise TERM ("bad pattern", [t])
 
 fun dest_pats [] = I
@@ -395,8 +395,8 @@
       | (ps, [false]) => cons (SNoPat ps)
       | _ => raise TERM ("bad multi-pattern", ts))
 
-fun dest_trigger (@{const SMT2.trigger} $ tl $ t) =
-      (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
+fun dest_trigger (@{const trigger} $ tl $ t) =
+      (rev (fold (dest_pats o SMT2_Util.dest_symb_list) (SMT2_Util.dest_symb_list tl) []), t)
   | dest_trigger t = ([], t)
 
 fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
@@ -439,7 +439,7 @@
       | (u as Free (_, T), ts) => transs u T ts
       | (Bound i, []) => pair (SVar i)
       | _ => raise TERM ("bad SMT term", [t]))
- 
+
     and transs t T ts =
       let val (Us, U) = SMT2_Util.dest_funT (length ts) T
       in
@@ -463,7 +463,7 @@
 
 fun add_config (cs, cfg) = Configs.map (SMT2_Util.dict_update (cs, cfg))
 
-fun get_config ctxt = 
+fun get_config ctxt =
   let val cs = SMT2_Config.solver_class_of ctxt
   in
     (case SMT2_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of
@@ -491,11 +491,11 @@
     fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) =
           q $ Abs (n, T, mk_trigger t)
       | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) =
-          Term.domain_type T --> @{typ SMT2.pattern}
-          |> (fn T => Const (@{const_name SMT2.pat}, T) $ lhs)
-          |> HOLogic.mk_list @{typ SMT2.pattern} o single
-          |> HOLogic.mk_list @{typ "SMT2.pattern list"} o single
-          |> (fn t => @{const SMT2.trigger} $ t $ eq)
+          Term.domain_type T --> @{typ pattern}
+          |> (fn T => Const (@{const_name pat}, T) $ lhs)
+          |> SMT2_Util.mk_symb_list @{typ pattern} o single
+          |> SMT2_Util.mk_symb_list @{typ "pattern symb_list"} o single
+          |> (fn t => @{const trigger} $ t $ eq)
       | mk_trigger t = t
 
     val (ctxt2, ts3) =
@@ -505,7 +505,7 @@
       |-> Lambda_Lifting.lift_lambdas NONE is_binder
       |-> (fn (ts', defs) => fn ctxt' =>
           map mk_trigger defs @ ts'
-          |> intro_explicit_application ctxt' funcs 
+          |> intro_explicit_application ctxt' funcs
           |> pair ctxt')
 
     val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/smt2_util.ML
--- a/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -30,6 +30,12 @@
   val under_quant: (term -> 'a) -> term -> 'a
   val is_number: term -> bool
 
+  (*symbolic lists*)
+  val symb_nil_const: typ -> term
+  val symb_cons_const: typ -> term
+  val mk_symb_list: typ -> term list -> term
+  val dest_symb_list: term -> term list
+
   (*patterns and instantiations*)
   val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
   val destT1: ctyp -> ctyp
@@ -142,6 +148,22 @@
   in is_num [] end
 
 
+(* symbolic lists *)
+
+fun symb_listT T = Type (@{type_name symb_list}, [T])
+
+fun symb_nil_const T = Const (@{const_name Symb_Nil}, symb_listT T)
+
+fun symb_cons_const T =
+  let val listT = symb_listT T in Const (@{const_name Symb_Cons}, T --> listT --> listT) end
+
+fun mk_symb_list T ts =
+  fold_rev (fn t => fn u => symb_cons_const T $ t $ u) ts (symb_nil_const T)
+
+fun dest_symb_list (Const (@{const_name Symb_Nil}, _)) = []
+  | dest_symb_list (Const (@{const_name Symb_Cons}, _) $ t $ u) = t :: dest_symb_list u
+
+
 (* patterns and instantiations *)
 
 fun mk_const_pat thy name destT =
@@ -160,7 +182,7 @@
 
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
 
-fun typ_of ct = #T (Thm.rep_cterm ct) 
+fun typ_of ct = #T (Thm.rep_cterm ct)
 
 fun dest_cabs ct ctxt =
   (case Thm.term_of ct of
@@ -169,7 +191,7 @@
       in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
   | _ => raise CTERM ("no abstraction", [ct]))
 
-val dest_all_cabs = repeat_yield (try o dest_cabs) 
+val dest_all_cabs = repeat_yield (try o dest_cabs)
 
 fun dest_cbinder ct ctxt =
   (case Thm.term_of ct of
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/smtlib2_proof.ML
--- a/src/HOL/Tools/SMT2/smtlib2_proof.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_proof.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -164,8 +164,8 @@
       SOME (mk_lassoc' @{const_name minus_class.minus} t ts)
   | core_term_parser (SMTLIB2.Sym "*", t :: ts) =
       SOME (mk_lassoc' @{const_name times_class.times} t ts)
-  | core_term_parser (SMTLIB2.Sym "div", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3div} t1 t2)
-  | core_term_parser (SMTLIB2.Sym "mod", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3mod} t1 t2)
+  | core_term_parser (SMTLIB2.Sym "div", [t1, t2]) = SOME (mk_binary @{const_name z3div} t1 t2)
+  | core_term_parser (SMTLIB2.Sym "mod", [t1, t2]) = SOME (mk_binary @{const_name z3mod} t1 t2)
   | core_term_parser (SMTLIB2.Sym "<", [t1, t2]) = SOME (mk_less t1 t2)
   | core_term_parser (SMTLIB2.Sym ">", [t1, t2]) = SOME (mk_less t2 t1)
   | core_term_parser (SMTLIB2.Sym "<=", [t1, t2]) = SOME (mk_less_eq t1 t2)
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/z3_new_replay.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -71,8 +71,8 @@
   in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end
 
 local
-  val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def}
-  val remove_fun_app = mk_meta_eq @{thm SMT2.fun_app_def}
+  val remove_trigger = mk_meta_eq @{thm trigger_def}
+  val remove_fun_app = mk_meta_eq @{thm fun_app_def}
 
   fun rewrite_conv _ [] = Conv.all_conv
     | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
@@ -97,7 +97,7 @@
       assms
       |> map (apsnd (rewrite ctxt eqs'))
       |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
-      |> Z3_New_Replay_Util.thm_net_of snd 
+      |> Z3_New_Replay_Util.thm_net_of snd
 
     fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
 
@@ -159,7 +159,7 @@
 
 fun discharge_assms_tac rules =
   REPEAT (HEADGOAL (resolve_tac (intro_def_rules @ rules) ORELSE' SOLVED' discharge_sk_tac))
-  
+
 fun discharge_assms ctxt rules thm =
   (if Thm.nprems_of thm = 0 then
      thm
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/z3_new_replay_literals.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -92,7 +92,7 @@
   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}
@@ -251,7 +251,7 @@
     fun join1 (s, t) =
       (case lookup t of
         SOME lit => (s, lit)
-      | NONE => 
+      | NONE =>
           (case lookup_rule t of
             (rewrite, SOME lit) => (s, rewrite lit)
           | (_, NONE) => (s, comp (pairself join1 (dest t)))))
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/z3_new_replay_methods.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -472,7 +472,7 @@
 
 val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
 
-fun quant_inst ctxt _ t = prove ctxt t (fn _ => 
+fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
   REPEAT_ALL_NEW (rtac quant_inst_rule)
   THEN' rtac @{thm excluded_middle})
 
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/z3_new_replay_rules.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -29,7 +29,7 @@
     val net = Data.get (Context.Proof ctxt)
     val xthms = Net.match_term net (Thm.term_of ct)
 
-    fun select ct = map_filter (maybe_instantiate ct) xthms 
+    fun select ct = map_filter (maybe_instantiate ct) xthms
     fun select' ct =
       let val thm = Thm.trivial ct
       in map_filter (try (fn rule => rule COMP thm)) xthms end
diff -r 489083abce44 -r ec5ff6bb2a92 src/HOL/Tools/SMT2/z3_new_replay_util.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
@@ -43,7 +43,7 @@
     let
       val lookup = if match then Net.match_term else Net.unify_term
       val xthms = lookup net (Thm.term_of ct)
-      fun select ct = map_filter (f (maybe_instantiate ct)) xthms 
+      fun select ct = map_filter (f (maybe_instantiate ct)) xthms
       fun select' ct =
         let val thm = Thm.trivial ct
         in map_filter (f (try (fn rule => rule COMP thm))) xthms end