use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 17 08:14:56 2010 +0100
@@ -162,10 +162,12 @@
addsimps [@{thm Nat_Numeral.int_nat_number_of}]
addsimps @{thms neg_simps}
+ val int_eq = Thm.cterm_of @{theory} @{const "==" (int)}
+
fun cancel_int_nat_simproc _ ss ct =
let
val num = Thm.dest_arg (Thm.dest_arg ct)
- val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
+ val goal = Thm.mk_binop int_eq ct num
val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
fun tac _ = Simplifier.simp_tac simpset 1
in on_positive num (Goal.prove_internal [] goal) tac end
@@ -180,8 +182,8 @@
fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
- val uses_nat_int =
- Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
+ val uses_nat_int = Term.exists_subterm (member (op aconv)
+ [@{const of_nat (int)}, @{const nat}])
in
fun nat_as_int ctxt =
map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
@@ -285,7 +287,7 @@
fun norm_def ctxt thm =
(case Thm.prop_of thm of
- @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
+ @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def ctxt (thm RS @{thm fun_cong})
| Const (@{const_name "=="}, _) $ _ $ Abs _ =>
norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
@@ -293,7 +295,7 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- @{term "op ==>"} $ _ $ _ =>
+ @{const "==>"} $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_imp}
| Const (@{const_name "=="}, _) $ _ $ _ =>
--- a/src/HOL/Tools/SMT/smt_real.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Nov 17 08:14:56 2010 +0100
@@ -63,7 +63,7 @@
(* Z3 builtins *)
local
- fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts)
+ fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
| z3_builtin_fun _ _ = NONE
in
@@ -86,13 +86,13 @@
if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
else NONE
- val mk_uminus = Thm.capply @{cterm "uminus :: real => _"}
- val mk_add = Thm.mk_binop @{cterm "op + :: real => _"}
- val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"}
- val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"}
- val mk_div = Thm.mk_binop @{cterm "op / :: real => _"}
- val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"}
- val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"}
+ val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
+ val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
+ val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
+ val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
+ val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
+ val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
+ val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
| z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 08:14:56 2010 +0100
@@ -264,6 +264,8 @@
in
raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
end)
+
+ val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
in
fun add_solver cfg =
@@ -271,7 +273,7 @@
val {name, env_var, is_remote, options, interface, outcome, cex_parser,
reconstruct} = cfg
- fun core_oracle () = @{cprop False}
+ fun core_oracle () = cfalse
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
interface=interface,
@@ -312,6 +314,8 @@
"contains the universal sort {}"))
else solver_of ctxt rm ctxt irules
+val cnot = Thm.cterm_of @{theory} @{const Not}
+
fun smt_filter run_remote time_limit st xrules i =
let
val {facts, goal, ...} = Proof.goal st
@@ -322,10 +326,8 @@
|> Config.put C.drop_bad_facts true
|> Config.put C.filter_only_facts true
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
- val cprop =
- concl
- |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
- |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
+ fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
+ val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
val rm = SOME run_remote
in
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 17 08:14:56 2010 +0100
@@ -134,7 +134,7 @@
| (ps, [false]) => cons (SNoPat ps)
| _ => raise TERM ("dest_pats", ts))
-fun dest_trigger (@{term trigger} $ tl $ t) =
+fun dest_trigger (@{const trigger} $ tl $ t) =
(rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
| dest_trigger t = ([], t)
@@ -161,8 +161,8 @@
val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
Const (@{const_name Let}, _) => true
- | @{term "op = :: bool => _"} $ _ $ @{term True} => true
- | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
+ | @{const HOL.eq (bool)} $ _ $ @{const True} => true
+ | Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true
| _ => false)
val rewrite_rules = [
@@ -199,11 +199,11 @@
fun conn (n, T) = (n, mapTs as_propT as_propT T)
fun pred (n, T) = (n, mapTs I as_propT T)
- val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
- fun as_term t = Const term_eq $ t $ @{term True}
+ val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
+ fun as_term t = Const term_eq $ t $ @{const True}
val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
- fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
+ fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
@@ -225,7 +225,7 @@
and in_pats ps =
in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
- and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
+ and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
| in_trig t = in_form t
and in_form t =
--- a/src/HOL/Tools/SMT/smt_word.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_word.ML Wed Nov 17 08:14:56 2010 +0100
@@ -60,7 +60,7 @@
fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
| dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
- fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
+ fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
| dest_nat ts = raise TERM ("dest_nat", ts)
fun dest_nat_word_funT (T, ts) =
(dest_word_funT (Term.range_type T), dest_nat ts)
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 17 08:14:56 2010 +0100
@@ -70,8 +70,8 @@
val {is_builtin_pred, ...}= the strict
val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
- fun is_int_div_mod @{term "op div :: int => _"} = true
- | is_int_div_mod @{term "op mod :: int => _"} = true
+ fun is_int_div_mod @{const div (int)} = true
+ | is_int_div_mod @{const mod (int)} = true
| is_int_div_mod _ = false
fun add_div_mod irules =
@@ -170,11 +170,13 @@
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
-val mk_true = @{cterm "~False"}
-val mk_false = @{cterm False}
-val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm HOL.implies}
-val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
+val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+val mk_false = Thm.cterm_of @{theory} @{const False}
+val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies})
+val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)})
+val conj = Thm.cterm_of @{theory} @{const HOL.conj}
+val disj = Thm.cterm_of @{theory} @{const HOL.disj}
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -205,22 +207,22 @@
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
in Thm.capply (Thm.mk_binop (instTs cTs update) array index) value end
-val mk_uminus = Thm.capply @{cterm "uminus :: int => _"}
-val mk_add = Thm.mk_binop @{cterm "op + :: int => _"}
-val mk_sub = Thm.mk_binop @{cterm "op - :: int => _"}
-val mk_mul = Thm.mk_binop @{cterm "op * :: int => _"}
-val mk_div = Thm.mk_binop @{cterm "z3div :: int => _"}
-val mk_mod = Thm.mk_binop @{cterm "z3mod :: int => _"}
-val mk_lt = Thm.mk_binop @{cterm "op < :: int => _"}
-val mk_le = Thm.mk_binop @{cterm "op <= :: int => _"}
+val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
+val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
+val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
+val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
+val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
+val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod})
+val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)})
+val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (int)})
fun mk_builtin_fun ctxt sym cts =
(case (sym, cts) of
(Sym ("true", _), []) => SOME mk_true
| (Sym ("false", _), []) => SOME mk_false
| (Sym ("not", _), [ct]) => SOME (mk_not ct)
- | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
- | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
+ | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
+ | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
--- a/src/HOL/Tools/SMT/z3_model.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML Wed Nov 17 08:14:56 2010 +0100
@@ -115,7 +115,7 @@
fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
val (default_int, ints) =
- (case find_first (match [@{term int}]) vs of
+ (case find_first (match [@{const of_nat (int)}]) vs of
NONE => (NONE, [])
| SOME (_, cases) =>
let val (cs, (_, e)) = split_last cases
@@ -138,7 +138,7 @@
| SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
in
map subst_nats vs
- |> filter_out (match [@{term int}, @{term nat}])
+ |> filter_out (match [@{const of_nat (int)}, @{const nat}])
end
fun filter_valid_valuations terms = map_filter (fn
@@ -179,8 +179,8 @@
fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
-fun trans_expr _ True = pair @{term True}
- | trans_expr _ False = pair @{term False}
+fun trans_expr _ True = pair @{const True}
+ | trans_expr _ False = pair @{const False}
| trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
| trans_expr T (Number (i, SOME j)) =
pair (Const (@{const_name divide}, [T, T] ---> T) $
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Nov 17 08:14:56 2010 +0100
@@ -22,6 +22,7 @@
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
@@ -59,19 +60,19 @@
(** properties and term operations **)
-val is_neg = (fn @{term Not} $ _ => true | _ => false)
-fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
+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 @{term HOL.conj} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false)
fun dest_disj_term' f = (fn
- @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
+ @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u)
| _ => NONE)
-val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
val dest_disj_term =
- dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
+ dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t)
fun exists_lit is_conj P =
let
@@ -82,6 +83,8 @@
| NONE => false)
in exists end
+val negate = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+
(** proof tools **)
@@ -135,7 +138,7 @@
end
| NONE => add (t, rev rules))
- fun explode0 (@{term Not} $ (@{term Not} $ t)) =
+ fun explode0 (@{const Not} $ (@{const Not} $ t)) =
Termtab.make [(t, [dneg_rule])]
| explode0 t = explode1 [] t Termtab.empty
@@ -202,23 +205,23 @@
| comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
| comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
- fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
+ fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u))
| dest_conj t = raise TERM ("dest_conj", [t])
- val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
- fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
+ 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}
- fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
+ fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
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 iff_const = @{term "op = :: bool => _"}
- fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
- f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
+ 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
@@ -231,12 +234,12 @@
fun lookup_rule t =
(case t of
- @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
- | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
- (T.compose negIffI, lookup (iff_const $ u $ t))
- | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
+ @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t)
+ | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
+ (T.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 (@{term Not} $ (eq $ u $ t))) end
+ in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
| _ =>
(case as_dneg lookup t of
NONE => (T.compose negIffE, as_negIff lookup t)
@@ -264,11 +267,10 @@
val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
- val neg = Thm.capply @{cterm Not}
in
-fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
-fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
-fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
+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
@@ -279,10 +281,10 @@
val rules = explode_term conj (T.prop_of thm)
fun contra_lits (t, rs) =
(case t of
- @{term Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
+ @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
| _ => NONE)
in
- (case Termtab.lookup rules @{term False} of
+ (case Termtab.lookup rules @{const False} of
SOME rs => extract_lit thm rs
| NONE =>
the (Termtab.get_first contra_lits rules)
@@ -322,8 +324,9 @@
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, @{term False}) => contradict true cl
- | (SOME DISJ, @{term "~False"}) => contrapos2 (contradict false o fst) cp
+ (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
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Wed Nov 17 08:14:56 2010 +0100
@@ -113,10 +113,11 @@
fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
in map mk vars end
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
+
fun close ctxt (ct, vars) =
let
val inst = mk_inst ctxt vars
- val mk_prop = Thm.capply @{cterm Trueprop}
val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
@@ -182,6 +183,8 @@
(* parser context *)
+val not_false = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+
fun make_context ctxt typs terms =
let
val ctxt' =
@@ -189,7 +192,7 @@
|> Symtab.fold (Variable.declare_typ o snd) typs
|> Symtab.fold (Variable.declare_term o snd) terms
- fun cert @{term True} = @{cterm "~False"}
+ fun cert @{const True} = not_false
| cert t = certify ctxt' t
in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
@@ -357,8 +360,10 @@
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+val ctrue = Thm.cterm_of @{theory} @{const True}
+
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
- (the o mk_fun (K (SOME @{cterm True})))) st
+ (the o mk_fun (K (SOME ctrue)))) st
fun quant_kind st = st |> (
this "forall" >> K (mk_forall o theory_of) ||
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Nov 17 08:14:56 2010 +0100
@@ -231,7 +231,7 @@
in
fun lemma thm ct =
let
- val cu = Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ val cu = L.negate (Thm.dest_arg ct)
val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
end
@@ -243,7 +243,7 @@
val explode_disj = L.explode false true false
val join_disj = L.join false
fun unit thm thms th =
- let val t = @{term Not} $ T.prop_of thm and ts = map T.prop_of thms
+ let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -251,7 +251,7 @@
val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
in
fun unit_resolution thm thms ct =
- Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ L.negate (Thm.dest_arg ct)
|> T.under_assumption (unit thm thms)
|> Thm o T.discharge thm o T.compose contrapos
end
@@ -295,14 +295,14 @@
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
in
(case Thm.term_of ct1 of
- @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
+ @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
- | @{term HOL.conj} $ _ $ _ =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
- | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
- | @{term HOL.disj} $ _ $ _ =>
- prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
+ | @{const HOL.conj} $ _ $ _ =>
+ prove disjI3 (L.negate ct2, false) (ct1, true)
+ | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
+ prove disjI3 (L.negate ct2, false) (ct1, false)
+ | @{const HOL.disj} $ _ $ _ =>
+ prove disjI2 (L.negate ct1, false) (ct2, true)
| Const (@{const_name SMT.distinct}, _) $ _ =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
@@ -310,7 +310,7 @@
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
- | @{term Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
+ | @{const Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
fun prv cu =
@@ -392,7 +392,7 @@
if l aconv r
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
- | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
+ | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
| _ =>
let
@@ -474,8 +474,8 @@
fun mono f (cp as (cl, _)) =
(case Term.head_of (Thm.term_of cl) of
- @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
- | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
+ @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+ | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
| Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
| _ => prove (prove_eq_safe f)) cp
in
@@ -589,8 +589,8 @@
|> Conv.fconv_rule (Thm.beta_conversion true)
fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
- | kind (@{term Not} $ (Const (@{const_name All}, _) $ _)) =
- (sk_all_rule, Thm.dest_arg, Thm.capply @{cterm Not})
+ | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
+ (sk_all_rule, Thm.dest_arg, L.negate)
| kind t = raise TERM ("skolemize", [t])
fun dest_abs_type (Abs (_, T, _)) = T
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Nov 17 08:14:55 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Nov 17 08:14:56 2010 +0100
@@ -53,12 +53,12 @@
(* accessing terms *)
-val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
+val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
fun term_of ct = dest_prop (Thm.term_of ct)
fun prop_of thm = dest_prop (Thm.prop_of thm)
-val mk_prop = Thm.capply @{cterm Trueprop}
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
val eq = I.mk_inst_pair I.destT1 @{cpat "op =="}
fun mk_meta_eq_cterm ct cu = Thm.mk_binop (I.instT' ct eq) ct cu
@@ -195,14 +195,14 @@
and abstr cvs ct =
(case Thm.term_of ct of
- @{term Trueprop} $ _ => abstr1 cvs ct
- | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
- | @{term True} => pair ct
- | @{term False} => pair ct
- | @{term Not} $ _ => abstr1 cvs ct
- | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
- | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
- | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
+ @{const Trueprop} $ _ => abstr1 cvs ct
+ | @{const "==>"} $ _ $ _ => abstr2 cvs ct
+ | @{const True} => pair ct
+ | @{const False} => pair ct
+ | @{const Not} $ _ => abstr1 cvs ct
+ | @{const HOL.conj} $ _ $ _ => abstr2 cvs ct
+ | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
+ | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name SMT.distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
@@ -221,8 +221,10 @@
else fresh_abstraction cvs ct cx))
in abstr [] end
+val cimp = Thm.cterm_of @{theory} @{const "==>"}
+
fun with_prems thms f ct =
- fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
+ fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
|> f
|> fold (fn prem => fn th => Thm.implies_elim th prem) thms