--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Wed Mar 04 23:31:13 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Wed Mar 04 23:42:47 2015 +0100
@@ -39,7 +39,6 @@
val instT': cterm -> ctyp * cterm -> cterm
(*certified terms*)
- val certify: Proof.context -> term -> cterm
val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
@@ -160,8 +159,6 @@
(* certified terms *)
-fun certify ctxt = Proof_Context.cterm_of ctxt
-
fun dest_cabs ct ctxt =
(case Thm.term_of ct of
Abs _ =>
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Wed Mar 04 23:31:13 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Wed Mar 04 23:42:47 2015 +0100
@@ -51,15 +51,15 @@
fun mk_inv_of ctxt ct =
let
val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
- val inv = Old_SMT_Utils.certify ctxt (mk_inv_into dT rT)
- val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
+ val inv = Proof_Context.cterm_of ctxt (mk_inv_into dT rT)
+ val univ = Proof_Context.cterm_of ctxt (mk_univ dT)
in Thm.mk_binop inv univ ct end
fun mk_inj_prop ctxt ct =
let
val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
- val inj = Old_SMT_Utils.certify ctxt (mk_inj_on dT rT)
- val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
+ val inj = Proof_Context.cterm_of ctxt (mk_inj_on dT rT)
+ val univ = Proof_Context.cterm_of ctxt (mk_univ dT)
in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Wed Mar 04 23:31:13 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Wed Mar 04 23:42:47 2015 +0100
@@ -109,7 +109,7 @@
val max = fold (Integer.max o fst) vars 0
val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
fun mk (i, v) =
- (v, Old_SMT_Utils.certify ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
+ (v, Proof_Context.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
in map mk vars end
fun close ctxt (ct, vars) =
@@ -120,7 +120,7 @@
fun mk_bound ctxt (i, T) =
- let val ct = Old_SMT_Utils.certify ctxt (Var ((Name.uu, 0), T))
+ let val ct = Proof_Context.cterm_of ctxt (Var ((Name.uu, 0), T))
in (ct, [(i, ct)]) end
local
@@ -129,7 +129,7 @@
val cv =
(case AList.lookup (op =) vars 0 of
SOME cv => cv
- | _ => Old_SMT_Utils.certify ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T)))
+ | _ => Proof_Context.cterm_of ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T)))
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
val vars' = map_filter dec vars
in (Thm.apply (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
@@ -191,7 +191,7 @@
|> Symtab.fold (Variable.declare_term o snd) terms
fun cert @{const True} = not_false
- | cert t = Old_SMT_Utils.certify ctxt' t
+ | cert t = Proof_Context.cterm_of ctxt' t
in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end
@@ -207,7 +207,7 @@
| NONE => cx |> fresh_name (decl_prefix ^ n)
|> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
let
- val upd = Symtab.update (n, Old_SMT_Utils.certify ctxt (Free (m, T)))
+ val upd = Symtab.update (n, Proof_Context.cterm_of ctxt (Free (m, T)))
in (typs, upd terms, exprs, steps, vars, ctxt) end))
fun mk_typ (typs, _, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _)) =
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Wed Mar 04 23:31:13 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Wed Mar 04 23:42:47 2015 +0100
@@ -617,7 +617,7 @@
fun get_vars f mk pred ctxt t =
Term.fold_aterms f t []
|> map_filter (fn v =>
- if pred v then SOME (Old_SMT_Utils.certify ctxt (mk v)) else NONE)
+ if pred v then SOME (Proof_Context.cterm_of ctxt (mk v)) else NONE)
fun close vars f ct ctxt =
let
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Mar 04 23:31:13 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Mar 04 23:42:47 2015 +0100
@@ -156,7 +156,7 @@
| NONE =>
let
val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
- val cv = Old_SMT_Utils.certify ctxt'
+ val cv = Proof_Context.cterm_of ctxt'
(Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
val cu = Drule.list_comb (cv, cvs')
val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
--- a/src/Pure/drule.ML Wed Mar 04 23:31:13 2015 +0100
+++ b/src/Pure/drule.ML Wed Mar 04 23:42:47 2015 +0100
@@ -773,10 +773,10 @@
local
fun add_types (ct, cu) (thy, tye, maxidx) =
let
- val {t, T, maxidx = maxt, ...} = Thm.rep_cterm ct;
- val {t = u, T = U, maxidx = maxu, ...} = Thm.rep_cterm cu;
- val maxi = Int.max (maxidx, Int.max (maxt, maxu));
- val thy' = Theory.merge (thy, Theory.merge (Thm.theory_of_cterm ct, Thm.theory_of_cterm cu));
+ val t = Thm.term_of ct and T = Thm.typ_of_cterm ct;
+ val u = Thm.term_of cu and U = Thm.typ_of_cterm cu;
+ val maxi = Int.max (maxidx, Int.max (apply2 Thm.maxidx_of_cterm (ct, cu)));
+ val thy' = Theory.merge (thy, Theory.merge (apply2 Thm.theory_of_cterm (ct, cu)));
val (tye', maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^
Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^
--- a/src/Pure/thm.ML Wed Mar 04 23:31:13 2015 +0100
+++ b/src/Pure/thm.ML Wed Mar 04 23:42:47 2015 +0100
@@ -3,12 +3,12 @@
Author: Makarius
The very core of Isabelle's Meta Logic: certified types and terms,
-derivations, theorems, framework rules (including lifting and
+derivations, theorems, inference rules (including lifting and
resolution), oracles.
*)
signature BASIC_THM =
- sig
+sig
type ctyp
type cterm
exception CTERM of string * cterm list
@@ -20,17 +20,12 @@
signature THM =
sig
include BASIC_THM
-
(*certified types*)
- val rep_ctyp: ctyp -> {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T}
val theory_of_ctyp: ctyp -> theory
val typ_of: ctyp -> typ
val ctyp_of: theory -> typ -> ctyp
val dest_ctyp: ctyp -> ctyp list
-
(*certified terms*)
- val rep_cterm: cterm -> {thy: theory, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}
- val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
val theory_of_cterm: cterm -> theory
val term_of: cterm -> term
val typ_of_cterm: cterm -> typ
@@ -50,7 +45,6 @@
val incr_indexes_cterm: int -> cterm -> cterm
val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
-
(*theorems*)
val rep_thm: thm ->
{thy: theory,
@@ -102,7 +96,7 @@
val map_tags: (Properties.T -> Properties.T) -> thm -> thm
val norm_proof: thm -> thm
val adjust_maxidx_thm: int -> thm -> thm
- (*meta rules*)
+ (*inference rules*)
val assume: cterm -> thm
val implies_intr: cterm -> thm -> thm
val implies_elim: thm -> thm -> thm
@@ -140,6 +134,7 @@
val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
+ (*oracles*)
val extern_oracles: Proof.context -> (Markup.T * xstring) list
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
@@ -154,7 +149,6 @@
abstype ctyp = Ctyp of {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T}
with
-fun rep_ctyp (Ctyp args) = args;
fun theory_of_ctyp (Ctyp {thy, ...}) = thy;
fun typ_of (Ctyp {T, ...}) = T;
@@ -179,12 +173,6 @@
exception CTERM of string * cterm list;
-fun rep_cterm (Cterm args) = args;
-
-fun crep_cterm (Cterm {thy, t, T, maxidx, sorts}) =
- {thy = thy, t = t, maxidx = maxidx, sorts = sorts,
- T = Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}};
-
fun theory_of_cterm (Cterm {thy, ...}) = thy;
fun term_of (Cterm {t, ...}) = t;