# HG changeset patch # User wenzelm # Date 1425508967 -3600 # Node ID 81b33949622cfd5f2de1abf0b8feadec5047f918 # Parent c6f3dbe466b66c21a391b73ab61268517ebfde51# Parent d223f586c7c3dc5cbfac159b4742be5e6f68097c merged diff -r c6f3dbe466b6 -r 81b33949622c src/HOL/Library/Old_SMT/old_smt_utils.ML --- 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 _ => diff -r c6f3dbe466b6 -r 81b33949622c src/HOL/Library/Old_SMT/old_z3_proof_methods.ML --- 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 diff -r c6f3dbe466b6 -r 81b33949622c src/HOL/Library/Old_SMT/old_z3_proof_parser.ML --- 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, _)) = diff -r c6f3dbe466b6 -r 81b33949622c src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- 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 diff -r c6f3dbe466b6 -r 81b33949622c src/HOL/Library/Old_SMT/old_z3_proof_tools.ML --- 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)) diff -r c6f3dbe466b6 -r 81b33949622c src/Pure/drule.ML --- 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) ^ diff -r c6f3dbe466b6 -r 81b33949622c src/Pure/thm.ML --- 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;