eliminate dependency of SMT2 module on 'list'
authorblanchet
Thu Jun 12 01:00:49 2014 +0200 (2014-06-12)
changeset 57230ec5ff6bb2a92
parent 57229 489083abce44
child 57231 dca8d06ecbba
eliminate dependency of SMT2 module on 'list'
src/HOL/SMT2.thy
src/HOL/Tools/SMT2/smt2_builtin.ML
src/HOL/Tools/SMT2/smt2_config.ML
src/HOL/Tools/SMT2/smt2_normalize.ML
src/HOL/Tools/SMT2/smt2_translate.ML
src/HOL/Tools/SMT2/smt2_util.ML
src/HOL/Tools/SMT2/smtlib2_proof.ML
src/HOL/Tools/SMT2/z3_new_replay.ML
src/HOL/Tools/SMT2/z3_new_replay_literals.ML
src/HOL/Tools/SMT2/z3_new_replay_methods.ML
src/HOL/Tools/SMT2/z3_new_replay_rules.ML
src/HOL/Tools/SMT2/z3_new_replay_util.ML
     1.1 --- a/src/HOL/SMT2.thy	Thu Jun 12 01:00:49 2014 +0200
     1.2 +++ b/src/HOL/SMT2.thy	Thu Jun 12 01:00:49 2014 +0200
     1.3 @@ -5,15 +5,10 @@
     1.4  header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *}
     1.5  
     1.6  theory SMT2
     1.7 -imports List
     1.8 +imports Divides
     1.9  keywords "smt2_status" :: diag
    1.10  begin
    1.11  
    1.12 -ML_file "Tools/SMT2/smt2_util.ML"
    1.13 -ML_file "Tools/SMT2/smt2_failure.ML"
    1.14 -ML_file "Tools/SMT2/smt2_config.ML"
    1.15 -
    1.16 -
    1.17  subsection {* Triggers for quantifier instantiation *}
    1.18  
    1.19  text {*
    1.20 @@ -31,13 +26,20 @@
    1.21  quantifier block.
    1.22  *}
    1.23  
    1.24 +typedecl 'a symb_list
    1.25 +
    1.26 +consts
    1.27 +  Symb_Nil :: "'a symb_list"
    1.28 +  Symb_Cons :: "'a \<Rightarrow> 'a symb_list \<Rightarrow> 'a symb_list"
    1.29 +
    1.30  typedecl pattern
    1.31  
    1.32  consts
    1.33    pat :: "'a \<Rightarrow> pattern"
    1.34    nopat :: "'a \<Rightarrow> pattern"
    1.35  
    1.36 -definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P"
    1.37 +definition trigger :: "pattern symb_list symb_list \<Rightarrow> bool \<Rightarrow> bool" where
    1.38 +  "trigger _ P = P"
    1.39  
    1.40  
    1.41  subsection {* Higher-order encoding *}
    1.42 @@ -68,8 +70,8 @@
    1.43  lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
    1.44  lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
    1.45  
    1.46 -lemma nat_zero_as_int: "0 = nat 0" by (rule transfer_nat_int_numerals(1))
    1.47 -lemma nat_one_as_int: "1 = nat 1" by (rule transfer_nat_int_numerals(2))
    1.48 +lemma nat_zero_as_int: "0 = nat 0" by simp
    1.49 +lemma nat_one_as_int: "1 = nat 1" by simp
    1.50  lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
    1.51  lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
    1.52  lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a <= int b)" by simp
    1.53 @@ -116,6 +118,9 @@
    1.54  
    1.55  subsection {* Setup *}
    1.56  
    1.57 +ML_file "Tools/SMT2/smt2_util.ML"
    1.58 +ML_file "Tools/SMT2/smt2_failure.ML"
    1.59 +ML_file "Tools/SMT2/smt2_config.ML"
    1.60  ML_file "Tools/SMT2/smt2_builtin.ML"
    1.61  ML_file "Tools/SMT2/smt2_datatypes.ML"
    1.62  ML_file "Tools/SMT2/smt2_normalize.ML"
    1.63 @@ -355,7 +360,7 @@
    1.64    "0 * x = 0"
    1.65    "1 * x = x"
    1.66    "x + y = y + x"
    1.67 -  by auto
    1.68 +  by (auto simp add: mult_2)
    1.69  
    1.70  lemma [z3_new_rule]:  (* for def-axiom *)
    1.71    "P = Q \<or> P \<or> Q"
    1.72 @@ -386,8 +391,7 @@
    1.73    "(if P then Q else \<not> R) \<or> P \<or> R"
    1.74    by auto
    1.75  
    1.76 -hide_type (open) pattern
    1.77 -hide_const fun_app z3div z3mod
    1.78 -hide_const (open) trigger pat nopat
    1.79 +hide_type (open) symb_list pattern
    1.80 +hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod
    1.81  
    1.82  end
     2.1 --- a/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
     2.3 @@ -50,7 +50,7 @@
     2.4  
     2.5  datatype ('a, 'b) kind = Ext of 'a | Int of 'b
     2.6  
     2.7 -type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict 
     2.8 +type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict
     2.9  
    2.10  fun typ_ord ((T, _), (U, _)) =
    2.11    let
    2.12 @@ -120,7 +120,7 @@
    2.13  fun dest_builtin_typ ctxt T =
    2.14    (case lookup_builtin_typ ctxt T of
    2.15      SOME (_, Int (f, _)) => f T
    2.16 -  | _ => NONE) 
    2.17 +  | _ => NONE)
    2.18  
    2.19  fun is_builtin_typ_ext ctxt T =
    2.20    (case lookup_builtin_typ ctxt T of
    2.21 @@ -205,7 +205,7 @@
    2.22      | NONE => dest_builtin_fun ctxt c ts)
    2.23    end
    2.24  
    2.25 -fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
    2.26 +fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =
    2.27    (case lookup_builtin_fun ctxt c of
    2.28      SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
    2.29    | SOME (_, Ext f) => SOME (f ctxt T ts)
     3.1 --- a/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
     3.3 @@ -220,7 +220,7 @@
     3.4      val ns = if null names then ["(none)"] else sort_strings names
     3.5      val n = the_default "(none)" (solver_name_of ctxt)
     3.6      val opts = solver_options_of ctxt
     3.7 -    
     3.8 +
     3.9      val t = string_of_real (Config.get ctxt timeout)
    3.10  
    3.11      val certs_filename =
     4.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4  (* general theorem normalizations *)
     4.5  
     4.6  (** instantiate elimination rules **)
     4.7 - 
     4.8 +
     4.9  local
    4.10    val (cpfalse, cfalse) = `SMT2_Util.mk_cprop (Thm.cterm_of @{theory} @{const False})
    4.11  
    4.12 @@ -113,8 +113,8 @@
    4.13  
    4.14    fun proper_trigger t =
    4.15      t
    4.16 -    |> these o try HOLogic.dest_list
    4.17 -    |> map (map_filter dest_trigger o these o try HOLogic.dest_list)
    4.18 +    |> these o try SMT2_Util.dest_symb_list
    4.19 +    |> map (map_filter dest_trigger o these o try SMT2_Util.dest_symb_list)
    4.20      |> (fn [] => false | bss => forall eq_list bss)
    4.21  
    4.22    fun proper_quant inside f t =
    4.23 @@ -185,16 +185,17 @@
    4.24              Pattern.matches thy (t', u) andalso not (t aconv u))
    4.25          in not (Term.exists_subterm some_match u) end
    4.26  
    4.27 -  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Util.destT1
    4.28 +  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name pat} SMT2_Util.destT1
    4.29    fun mk_pat ct = Thm.apply (SMT2_Util.instT' ct pat) ct
    4.30  
    4.31 -  fun mk_clist T = pairself (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T)
    4.32 +  fun mk_clist T =
    4.33 +    pairself (Thm.cterm_of @{theory}) (SMT2_Util.symb_cons_const T, SMT2_Util.symb_nil_const T)
    4.34    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
    4.35 -  val mk_pat_list = mk_list (mk_clist @{typ SMT2.pattern})
    4.36 -  val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})  
    4.37 +  val mk_pat_list = mk_list (mk_clist @{typ pattern})
    4.38 +  val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
    4.39    fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
    4.40  
    4.41 -  val trigger_eq = mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)}
    4.42 +  val trigger_eq = mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)}
    4.43  
    4.44    fun insert_trigger_conv [] ct = Conv.all_conv ct
    4.45      | insert_trigger_conv ctss ct =
    4.46 @@ -216,7 +217,7 @@
    4.47  
    4.48      in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
    4.49  
    4.50 -  fun has_trigger (@{const SMT2.trigger} $ _ $ _) = true
    4.51 +  fun has_trigger (@{const trigger} $ _ $ _) = true
    4.52      | has_trigger _ = false
    4.53  
    4.54    fun try_trigger_conv cv ct =
    4.55 @@ -234,7 +235,7 @@
    4.56  
    4.57  val setup_trigger =
    4.58    fold SMT2_Builtin.add_builtin_fun_ext''
    4.59 -    [@{const_name SMT2.pat}, @{const_name SMT2.nopat}, @{const_name SMT2.trigger}]
    4.60 +    [@{const_name pat}, @{const_name nopat}, @{const_name trigger}]
    4.61  
    4.62  end
    4.63  
    4.64 @@ -317,7 +318,7 @@
    4.65  
    4.66  fun unfold_abs_min_max_conv ctxt =
    4.67    SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
    4.68 -  
    4.69 +
    4.70  val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table
    4.71  
    4.72  end
    4.73 @@ -481,18 +482,17 @@
    4.74  
    4.75    val schematic_consts_of =
    4.76      let
    4.77 -      fun collect (@{const SMT2.trigger} $ p $ t) =
    4.78 -            collect_trigger p #> collect t
    4.79 +      fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
    4.80          | collect (t $ u) = collect t #> collect u
    4.81          | collect (Abs (_, _, t)) = collect t
    4.82 -        | collect (t as Const (n, _)) = 
    4.83 +        | collect (t as Const (n, _)) =
    4.84              if not (ignored n) then Monomorph.add_schematic_consts_of t else I
    4.85          | collect _ = I
    4.86        and collect_trigger t =
    4.87 -        let val dest = these o try HOLogic.dest_list 
    4.88 +        let val dest = these o try SMT2_Util.dest_symb_list
    4.89          in fold (fold collect_pat o dest) (dest t) end
    4.90 -      and collect_pat (Const (@{const_name SMT2.pat}, _) $ t) = collect t
    4.91 -        | collect_pat (Const (@{const_name SMT2.nopat}, _) $ t) = collect t
    4.92 +      and collect_pat (Const (@{const_name pat}, _) $ t) = collect t
    4.93 +        | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t
    4.94          | collect_pat _ = I
    4.95      in (fn t => collect t Symtab.empty) end
    4.96  in
     5.1 --- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
     5.3 @@ -104,7 +104,7 @@
     5.4  fun add_fun t sort (cx as (names, typs, terms)) =
     5.5    (case Termtab.lookup terms t of
     5.6      SOME (name, _) => (name, cx)
     5.7 -  | NONE => 
     5.8 +  | NONE =>
     5.9        let
    5.10          val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix
    5.11          val (name, names') = Name.variant sugg names
    5.12 @@ -214,7 +214,7 @@
    5.13            | (u, ts) => Term.list_comb (u, map expand ts))
    5.14  
    5.15      and abs_expand (n, T, t) = Abs (n, T, expand t)
    5.16 -  
    5.17 +
    5.18    in map expand end
    5.19  
    5.20  end
    5.21 @@ -246,7 +246,7 @@
    5.22        val (Ts, T) = Term.strip_type (Term.type_of t)
    5.23      in find_min 0 (take i (rev Ts)) T end
    5.24  
    5.25 -  fun app u (t, T) = (Const (@{const_name SMT2.fun_app}, T --> T) $ t $ u, Term.range_type T)
    5.26 +  fun app u (t, T) = (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T)
    5.27  
    5.28    fun apply i t T ts =
    5.29      let
    5.30 @@ -264,7 +264,7 @@
    5.31        if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
    5.32        else apply (the (Termtab.lookup arities' t)) t T ts
    5.33  
    5.34 -    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
    5.35 +    fun in_list T f t = SMT2_Util.mk_symb_list T (map f (SMT2_Util.dest_symb_list t))
    5.36  
    5.37      fun traverse Ts t =
    5.38        (case Term.strip_comb t of
    5.39 @@ -286,17 +286,17 @@
    5.40        | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
    5.41        | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
    5.42        | (u, ts) => traverses Ts u ts)
    5.43 -    and in_trigger Ts ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
    5.44 +    and in_trigger Ts ((c as @{const trigger}) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
    5.45        | in_trigger Ts t = traverse Ts t
    5.46      and in_pats Ts ps =
    5.47 -      in_list @{typ "SMT2.pattern list"} (in_list @{typ SMT2.pattern} (in_pat Ts)) ps
    5.48 -    and in_pat Ts ((p as Const (@{const_name SMT2.pat}, _)) $ t) = p $ traverse Ts t
    5.49 -      | in_pat Ts ((p as Const (@{const_name SMT2.nopat}, _)) $ t) = p $ traverse Ts t
    5.50 +      in_list @{typ "pattern symb_list"} (in_list @{typ pattern} (in_pat Ts)) ps
    5.51 +    and in_pat Ts ((p as Const (@{const_name pat}, _)) $ t) = p $ traverse Ts t
    5.52 +      | in_pat Ts ((p as Const (@{const_name nopat}, _)) $ t) = p $ traverse Ts t
    5.53        | in_pat _ t = raise TERM ("bad pattern", [t])
    5.54      and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
    5.55    in map (traverse []) ts end
    5.56  
    5.57 -val fun_app_eq = mk_meta_eq @{thm SMT2.fun_app_def}
    5.58 +val fun_app_eq = mk_meta_eq @{thm fun_app_def}
    5.59  
    5.60  end
    5.61  
    5.62 @@ -323,7 +323,7 @@
    5.63  
    5.64  fun folify ctxt =
    5.65    let
    5.66 -    fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t))
    5.67 +    fun in_list T f t = SMT2_Util.mk_symb_list T (map_filter f (SMT2_Util.dest_symb_list t))
    5.68  
    5.69      fun in_term pat t =
    5.70        (case Term.strip_comb t of
    5.71 @@ -338,16 +338,16 @@
    5.72        | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
    5.73        | _ => t)
    5.74  
    5.75 -    and in_pat ((p as Const (@{const_name SMT2.pat}, _)) $ t) =
    5.76 +    and in_pat ((p as Const (@{const_name pat}, _)) $ t) =
    5.77            p $ in_term true t
    5.78 -      | in_pat ((p as Const (@{const_name SMT2.nopat}, _)) $ t) =
    5.79 +      | in_pat ((p as Const (@{const_name nopat}, _)) $ t) =
    5.80            p $ in_term true t
    5.81        | in_pat t = raise TERM ("bad pattern", [t])
    5.82  
    5.83      and in_pats ps =
    5.84 -      in_list @{typ "SMT2.pattern list"} (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps
    5.85 +      in_list @{typ "pattern symb_list"} (SOME o in_list @{typ pattern} (try in_pat)) ps
    5.86  
    5.87 -    and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_form t
    5.88 +    and in_trigger ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
    5.89        | in_trigger t = in_form t
    5.90  
    5.91      and in_form t =
    5.92 @@ -384,8 +384,8 @@
    5.93        if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
    5.94    | group_quant _ Ts t = (Ts, t)
    5.95  
    5.96 -fun dest_pat (Const (@{const_name SMT2.pat}, _) $ t) = (t, true)
    5.97 -  | dest_pat (Const (@{const_name SMT2.nopat}, _) $ t) = (t, false)
    5.98 +fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
    5.99 +  | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
   5.100    | dest_pat t = raise TERM ("bad pattern", [t])
   5.101  
   5.102  fun dest_pats [] = I
   5.103 @@ -395,8 +395,8 @@
   5.104        | (ps, [false]) => cons (SNoPat ps)
   5.105        | _ => raise TERM ("bad multi-pattern", ts))
   5.106  
   5.107 -fun dest_trigger (@{const SMT2.trigger} $ tl $ t) =
   5.108 -      (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
   5.109 +fun dest_trigger (@{const trigger} $ tl $ t) =
   5.110 +      (rev (fold (dest_pats o SMT2_Util.dest_symb_list) (SMT2_Util.dest_symb_list tl) []), t)
   5.111    | dest_trigger t = ([], t)
   5.112  
   5.113  fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
   5.114 @@ -439,7 +439,7 @@
   5.115        | (u as Free (_, T), ts) => transs u T ts
   5.116        | (Bound i, []) => pair (SVar i)
   5.117        | _ => raise TERM ("bad SMT term", [t]))
   5.118 - 
   5.119 +
   5.120      and transs t T ts =
   5.121        let val (Us, U) = SMT2_Util.dest_funT (length ts) T
   5.122        in
   5.123 @@ -463,7 +463,7 @@
   5.124  
   5.125  fun add_config (cs, cfg) = Configs.map (SMT2_Util.dict_update (cs, cfg))
   5.126  
   5.127 -fun get_config ctxt = 
   5.128 +fun get_config ctxt =
   5.129    let val cs = SMT2_Config.solver_class_of ctxt
   5.130    in
   5.131      (case SMT2_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of
   5.132 @@ -491,11 +491,11 @@
   5.133      fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) =
   5.134            q $ Abs (n, T, mk_trigger t)
   5.135        | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) =
   5.136 -          Term.domain_type T --> @{typ SMT2.pattern}
   5.137 -          |> (fn T => Const (@{const_name SMT2.pat}, T) $ lhs)
   5.138 -          |> HOLogic.mk_list @{typ SMT2.pattern} o single
   5.139 -          |> HOLogic.mk_list @{typ "SMT2.pattern list"} o single
   5.140 -          |> (fn t => @{const SMT2.trigger} $ t $ eq)
   5.141 +          Term.domain_type T --> @{typ pattern}
   5.142 +          |> (fn T => Const (@{const_name pat}, T) $ lhs)
   5.143 +          |> SMT2_Util.mk_symb_list @{typ pattern} o single
   5.144 +          |> SMT2_Util.mk_symb_list @{typ "pattern symb_list"} o single
   5.145 +          |> (fn t => @{const trigger} $ t $ eq)
   5.146        | mk_trigger t = t
   5.147  
   5.148      val (ctxt2, ts3) =
   5.149 @@ -505,7 +505,7 @@
   5.150        |-> Lambda_Lifting.lift_lambdas NONE is_binder
   5.151        |-> (fn (ts', defs) => fn ctxt' =>
   5.152            map mk_trigger defs @ ts'
   5.153 -          |> intro_explicit_application ctxt' funcs 
   5.154 +          |> intro_explicit_application ctxt' funcs
   5.155            |> pair ctxt')
   5.156  
   5.157      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
     6.1 --- a/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
     6.2 +++ b/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
     6.3 @@ -30,6 +30,12 @@
     6.4    val under_quant: (term -> 'a) -> term -> 'a
     6.5    val is_number: term -> bool
     6.6  
     6.7 +  (*symbolic lists*)
     6.8 +  val symb_nil_const: typ -> term
     6.9 +  val symb_cons_const: typ -> term
    6.10 +  val mk_symb_list: typ -> term list -> term
    6.11 +  val dest_symb_list: term -> term list
    6.12 +
    6.13    (*patterns and instantiations*)
    6.14    val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
    6.15    val destT1: ctyp -> ctyp
    6.16 @@ -142,6 +148,22 @@
    6.17    in is_num [] end
    6.18  
    6.19  
    6.20 +(* symbolic lists *)
    6.21 +
    6.22 +fun symb_listT T = Type (@{type_name symb_list}, [T])
    6.23 +
    6.24 +fun symb_nil_const T = Const (@{const_name Symb_Nil}, symb_listT T)
    6.25 +
    6.26 +fun symb_cons_const T =
    6.27 +  let val listT = symb_listT T in Const (@{const_name Symb_Cons}, T --> listT --> listT) end
    6.28 +
    6.29 +fun mk_symb_list T ts =
    6.30 +  fold_rev (fn t => fn u => symb_cons_const T $ t $ u) ts (symb_nil_const T)
    6.31 +
    6.32 +fun dest_symb_list (Const (@{const_name Symb_Nil}, _)) = []
    6.33 +  | dest_symb_list (Const (@{const_name Symb_Cons}, _) $ t $ u) = t :: dest_symb_list u
    6.34 +
    6.35 +
    6.36  (* patterns and instantiations *)
    6.37  
    6.38  fun mk_const_pat thy name destT =
    6.39 @@ -160,7 +182,7 @@
    6.40  
    6.41  fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
    6.42  
    6.43 -fun typ_of ct = #T (Thm.rep_cterm ct) 
    6.44 +fun typ_of ct = #T (Thm.rep_cterm ct)
    6.45  
    6.46  fun dest_cabs ct ctxt =
    6.47    (case Thm.term_of ct of
    6.48 @@ -169,7 +191,7 @@
    6.49        in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
    6.50    | _ => raise CTERM ("no abstraction", [ct]))
    6.51  
    6.52 -val dest_all_cabs = repeat_yield (try o dest_cabs) 
    6.53 +val dest_all_cabs = repeat_yield (try o dest_cabs)
    6.54  
    6.55  fun dest_cbinder ct ctxt =
    6.56    (case Thm.term_of ct of
     7.1 --- a/src/HOL/Tools/SMT2/smtlib2_proof.ML	Thu Jun 12 01:00:49 2014 +0200
     7.2 +++ b/src/HOL/Tools/SMT2/smtlib2_proof.ML	Thu Jun 12 01:00:49 2014 +0200
     7.3 @@ -164,8 +164,8 @@
     7.4        SOME (mk_lassoc' @{const_name minus_class.minus} t ts)
     7.5    | core_term_parser (SMTLIB2.Sym "*", t :: ts) =
     7.6        SOME (mk_lassoc' @{const_name times_class.times} t ts)
     7.7 -  | core_term_parser (SMTLIB2.Sym "div", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3div} t1 t2)
     7.8 -  | core_term_parser (SMTLIB2.Sym "mod", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3mod} t1 t2)
     7.9 +  | core_term_parser (SMTLIB2.Sym "div", [t1, t2]) = SOME (mk_binary @{const_name z3div} t1 t2)
    7.10 +  | core_term_parser (SMTLIB2.Sym "mod", [t1, t2]) = SOME (mk_binary @{const_name z3mod} t1 t2)
    7.11    | core_term_parser (SMTLIB2.Sym "<", [t1, t2]) = SOME (mk_less t1 t2)
    7.12    | core_term_parser (SMTLIB2.Sym ">", [t1, t2]) = SOME (mk_less t2 t1)
    7.13    | core_term_parser (SMTLIB2.Sym "<=", [t1, t2]) = SOME (mk_less_eq t1 t2)
     8.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
     8.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
     8.3 @@ -71,8 +71,8 @@
     8.4    in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end
     8.5  
     8.6  local
     8.7 -  val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def}
     8.8 -  val remove_fun_app = mk_meta_eq @{thm SMT2.fun_app_def}
     8.9 +  val remove_trigger = mk_meta_eq @{thm trigger_def}
    8.10 +  val remove_fun_app = mk_meta_eq @{thm fun_app_def}
    8.11  
    8.12    fun rewrite_conv _ [] = Conv.all_conv
    8.13      | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
    8.14 @@ -97,7 +97,7 @@
    8.15        assms
    8.16        |> map (apsnd (rewrite ctxt eqs'))
    8.17        |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
    8.18 -      |> Z3_New_Replay_Util.thm_net_of snd 
    8.19 +      |> Z3_New_Replay_Util.thm_net_of snd
    8.20  
    8.21      fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
    8.22  
    8.23 @@ -159,7 +159,7 @@
    8.24  
    8.25  fun discharge_assms_tac rules =
    8.26    REPEAT (HEADGOAL (resolve_tac (intro_def_rules @ rules) ORELSE' SOLVED' discharge_sk_tac))
    8.27 -  
    8.28 +
    8.29  fun discharge_assms ctxt rules thm =
    8.30    (if Thm.nprems_of thm = 0 then
    8.31       thm
     9.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
     9.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
     9.3 @@ -92,7 +92,7 @@
     9.4    val dest_conj2 = precomp destc @{thm conjunct2}
     9.5    fun dest_conj_rules t =
     9.6      dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
     9.7 -    
     9.8 +
     9.9    fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct)))
    9.10    val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
    9.11    val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
    9.12 @@ -251,7 +251,7 @@
    9.13      fun join1 (s, t) =
    9.14        (case lookup t of
    9.15          SOME lit => (s, lit)
    9.16 -      | NONE => 
    9.17 +      | NONE =>
    9.18            (case lookup_rule t of
    9.19              (rewrite, SOME lit) => (s, rewrite lit)
    9.20            | (_, NONE) => (s, comp (pairself join1 (dest t)))))
    10.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
    10.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
    10.3 @@ -472,7 +472,7 @@
    10.4  
    10.5  val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
    10.6  
    10.7 -fun quant_inst ctxt _ t = prove ctxt t (fn _ => 
    10.8 +fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
    10.9    REPEAT_ALL_NEW (rtac quant_inst_rule)
   10.10    THEN' rtac @{thm excluded_middle})
   10.11  
    11.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
    11.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
    11.3 @@ -29,7 +29,7 @@
    11.4      val net = Data.get (Context.Proof ctxt)
    11.5      val xthms = Net.match_term net (Thm.term_of ct)
    11.6  
    11.7 -    fun select ct = map_filter (maybe_instantiate ct) xthms 
    11.8 +    fun select ct = map_filter (maybe_instantiate ct) xthms
    11.9      fun select' ct =
   11.10        let val thm = Thm.trivial ct
   11.11        in map_filter (try (fn rule => rule COMP thm)) xthms end
    12.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
    12.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
    12.3 @@ -43,7 +43,7 @@
    12.4      let
    12.5        val lookup = if match then Net.match_term else Net.unify_term
    12.6        val xthms = lookup net (Thm.term_of ct)
    12.7 -      fun select ct = map_filter (f (maybe_instantiate ct)) xthms 
    12.8 +      fun select ct = map_filter (f (maybe_instantiate ct)) xthms
    12.9        fun select' ct =
   12.10          let val thm = Thm.trivial ct
   12.11          in map_filter (f (try (fn rule => rule COMP thm))) xthms end