--- 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
--- 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)
--- 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 =
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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)))))
--- 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})
--- 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
--- 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