--- a/src/HOL/Library/positivstellensatz.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Sun Apr 14 12:00:17 2019 +0100
@@ -522,7 +522,7 @@
\<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
- val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
+ val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p)
val th0 = fconv_rule (Thm.beta_conversion true)
(Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
--- a/src/HOL/ROOT Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/ROOT Sun Apr 14 12:00:17 2019 +0100
@@ -74,7 +74,7 @@
theories
Approximations
-session "HOL-Homology" (main timing) in Homology = "HOL-Analysis" +
+session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
document_variants = "document:manual=-proof,-ML,-unimportant"]
sessions
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun Apr 14 12:00:17 2019 +0100
@@ -94,37 +94,36 @@
| is_quasi_lambda_free (Abs _) = false
| is_quasi_lambda_free _ = true
-(* FIXME: Requires more use of cterm constructors. *)
fun abstract ctxt ct =
let
- val Abs(x,_,body) = Thm.term_of ct
- val Type (\<^type_name>\<open>fun\<close>, [xT,bodyT]) = Thm.typ_of_cterm ct
- val cxT = Thm.ctyp_of ctxt xT
- val cbodyT = Thm.ctyp_of ctxt bodyT
- fun makeK () =
- Thm.instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
+ val Abs (_, _, body) = Thm.term_of ct
+ val (x, cbody) = Thm.dest_abs NONE ct
+ val (A, cbodyT) = Thm.dest_funT (Thm.ctyp_of_cterm ct)
+ fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K}
in
case body of
Const _ => makeK()
| Free _ => makeK()
| Var _ => makeK() (*though Var isn't expected*)
- | Bound 0 => Thm.instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
+ | Bound 0 => Thm.instantiate' [SOME A] [] @{thm abs_I} (*identity: I*)
| rator$rand =>
if Term.is_dependent rator then (*C or S*)
if Term.is_dependent rand then (*S*)
- let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
- val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
- val abs_S' =
- infer_instantiate ctxt [(("f", 0), crator), (("g", 0), crand)] @{thm abs_S}
+ let val crator = Thm.lambda x (Thm.dest_fun cbody)
+ val crand = Thm.lambda x (Thm.dest_arg cbody)
+ val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator))
+ val abs_S' = @{thm abs_S}
+ |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S')
in
Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs)
end
else (*C*)
- let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
- val abs_C' =
- infer_instantiate ctxt [(("f", 0), crator), (("b", 0), Thm.cterm_of ctxt rand)]
- @{thm abs_C}
+ let val crator = Thm.lambda x (Thm.dest_fun cbody)
+ val crand = Thm.dest_arg cbody
+ val (C, B) = Thm.dest_funT (Thm.dest_ctyp1 (Thm.ctyp_of_cterm crator))
+ val abs_C' = @{thm abs_C}
+ |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C')
in
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs)
@@ -132,10 +131,11 @@
else if Term.is_dependent rand then (*B or eta*)
if rand = Bound 0 then Thm.eta_conversion ct
else (*B*)
- let val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
- val crator = Thm.cterm_of ctxt rator
- val abs_B' =
- infer_instantiate ctxt [(("a", 0), crator), (("g", 0), crand)] @{thm abs_B}
+ let val crator = Thm.dest_fun cbody
+ val crand = Thm.lambda x (Thm.dest_arg cbody)
+ val (C, B) = Thm.dest_funT (Thm.ctyp_of_cterm crator)
+ val abs_B' = @{thm abs_B}
+ |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B')
in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end
else makeK ()
--- a/src/HOL/Tools/Qelim/qelim.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Sun Apr 14 12:00:17 2019 +0100
@@ -41,9 +41,10 @@
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
else Thm.transitive (Thm.transitive th th') (conv env r) end
| Const(\<^const_name>\<open>Ex\<close>,_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const(\<^const_name>\<open>All\<close>, allT)$_ =>
+ | Const(\<^const_name>\<open>All\<close>, _)$_ =>
let
- val T = Thm.ctyp_of ctxt (#1 (Term.dest_funT (#1 (Term.dest_funT allT))))
+ val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
+ val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT)
val p = Thm.dest_arg p
val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
in Thm.transitive th (conv env (Thm.rhs_of th))
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Apr 14 12:00:17 2019 +0100
@@ -70,13 +70,12 @@
local
-fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k;
val eq = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_arg;
val lhs = eq |> Thm.dest_arg1;
val pt_random_aux = lhs |> Thm.dest_fun;
val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
val a_v =
- pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1
+ pt_random_aux |> Thm.ctyp_of_cterm |> Thm.dest_ctyp1
|> Thm.typ_of |> dest_TVar;
val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one},
--- a/src/HOL/Tools/SMT/smt_normalize.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Sun Apr 14 12:00:17 2019 +0100
@@ -186,7 +186,7 @@
Pattern.matches thy (t', u) andalso not (t aconv u))
in not (Term.exists_subterm some_match u) end
- val pat = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>pat\<close> SMT_Util.destT1
+ val pat = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>pat\<close> Thm.dest_ctyp0
fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
fun mk_clist T =
--- a/src/HOL/Tools/SMT/smt_util.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/SMT/smt_util.ML Sun Apr 14 12:00:17 2019 +0100
@@ -40,8 +40,6 @@
(*patterns and instantiations*)
val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
- val destT1: ctyp -> ctyp
- val destT2: ctyp -> ctyp
val instTs: ctyp list -> ctyp list * cterm -> cterm
val instT: ctyp -> ctyp * cterm -> cterm
val instT': cterm -> ctyp * cterm -> cterm
@@ -175,9 +173,6 @@
let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name))
in (destT (Thm.ctyp_of_cterm cpat), cpat) end
-val destT1 = hd o Thm.dest_ctyp
-val destT2 = hd o tl o Thm.dest_ctyp
-
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
fun instT' ct = instT (Thm.ctyp_of_cterm ct)
@@ -208,7 +203,7 @@
\<^const>\<open>Trueprop\<close> $ _ => Thm.dest_arg ct
| _ => raise CTERM ("not a property", [ct]))
-val equals = mk_const_pat \<^theory> \<^const_name>\<open>Pure.eq\<close> destT1
+val equals = mk_const_pat \<^theory> \<^const_name>\<open>Pure.eq\<close> Thm.dest_ctyp0
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
val dest_prop = (fn \<^const>\<open>Trueprop\<close> $ t => t | t => t)
--- a/src/HOL/Tools/SMT/z3_interface.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Sun Apr 14 12:00:17 2019 +0100
@@ -127,18 +127,18 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
-val eq = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>HOL.eq\<close> SMT_Util.destT1
+val eq = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>HOL.eq\<close> Thm.dest_ctyp0
fun mk_eq ct cu = Thm.mk_binop (SMT_Util.instT' ct eq) ct cu
val if_term =
- SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>If\<close> (SMT_Util.destT1 o SMT_Util.destT2)
+ SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>If\<close> (Thm.dest_ctyp0 o Thm.dest_ctyp1)
fun mk_if cc ct = Thm.mk_binop (Thm.apply (SMT_Util.instT' ct if_term) cc) ct
-val access = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>fun_app\<close> SMT_Util.destT1
+val access = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>fun_app\<close> Thm.dest_ctyp0
fun mk_access array = Thm.apply (SMT_Util.instT' array access) array
val update =
- SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>fun_upd\<close> (Thm.dest_ctyp o SMT_Util.destT1)
+ SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>fun_upd\<close> (Thm.dest_ctyp o Thm.dest_ctyp0)
fun mk_update array index value =
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
--- a/src/HOL/Tools/Transfer/transfer.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML Sun Apr 14 12:00:17 2019 +0100
@@ -213,13 +213,9 @@
val Rel_rule = Thm.symmetric @{thm Rel_def}
-fun dest_funcT cT =
- (case Thm.dest_ctyp cT of [T, U] => (T, U)
- | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
-
fun Rel_conv ct =
- let val (cT, cT') = dest_funcT (Thm.ctyp_of_cterm ct)
- val (cU, _) = dest_funcT cT'
+ let val (cT, cT') = Thm.dest_funT (Thm.ctyp_of_cterm ct)
+ val (cU, _) = Thm.dest_funT cT'
in Thm.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
(* Conversion to preprocess a transfer rule *)
@@ -465,8 +461,8 @@
val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
val r2 = Thm.dest_fun2 (Thm.dest_arg (Thm.cprop_of thm1))
- val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r1))
- val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (Thm.ctyp_of_cterm r2))
+ val (a1, (b1, _)) = apsnd Thm.dest_funT (Thm.dest_funT (Thm.ctyp_of_cterm r1))
+ val (a2, (b2, _)) = apsnd Thm.dest_funT (Thm.dest_funT (Thm.ctyp_of_cterm r2))
val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
val rule = Thm.instantiate' tinsts insts @{thm Rel_abs}
--- a/src/HOL/Tools/groebner.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/HOL/Tools/groebner.ML Sun Apr 14 12:00:17 2019 +0100
@@ -481,7 +481,7 @@
\<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
- val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
+ val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p)
val th0 = Conv.fconv_rule (Thm.beta_conversion true)
(Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
val pv = (Thm.rhs_of o Thm.beta_conversion true)
--- a/src/Pure/drule.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/Pure/drule.ML Sun Apr 14 12:00:17 2019 +0100
@@ -21,6 +21,7 @@
val implies_intr_list: cterm list -> thm -> thm
val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
thm -> thm
+ val instantiate'_normalize: ctyp option list -> cterm option list -> thm -> thm
val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
val infer_instantiate': Proof.context -> cterm option list -> thm -> thm
@@ -56,7 +57,6 @@
val generalize: string list * string list -> thm -> thm
val list_comb: cterm * cterm list -> cterm
val strip_comb: cterm -> cterm * cterm list
- val strip_type: ctyp -> ctyp list * ctyp
val beta_conv: cterm -> cterm -> cterm
val flexflex_unique: Proof.context option -> thm -> thm
val export_without_context: thm -> thm
@@ -155,15 +155,6 @@
in stripc (ct1, ct2 :: cts) end handle CTERM _ => p
in stripc (ct, []) end;
-(* cterm version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *)
-fun strip_type cT = (case Thm.typ_of cT of
- Type ("fun", _) =>
- let
- val [cT1, cT2] = Thm.dest_ctyp cT;
- val (cTs, cT') = strip_type cT2
- in (cT1 :: cTs, cT') end
- | _ => ([], cT));
-
(*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
of the meta-equality returned by the beta_conversion rule.*)
fun beta_conv x y =
@@ -741,6 +732,9 @@
fun instantiate_normalize instpair th =
Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
+fun instantiate'_normalize Ts ts th =
+ Thm.adjust_maxidx_thm ~1 (Thm.instantiate' Ts ts th COMP_INCR asm_rl);
+
(*instantiation with type-inference for variables*)
fun infer_instantiate_types _ [] th = th
| infer_instantiate_types ctxt args raw_th =
--- a/src/Pure/more_thm.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/Pure/more_thm.ML Sun Apr 14 12:00:17 2019 +0100
@@ -28,6 +28,8 @@
val add_tvars: thm -> ctyp list -> ctyp list
val add_frees: thm -> cterm list -> cterm list
val add_vars: thm -> cterm list -> cterm list
+ val dest_funT: ctyp -> ctyp * ctyp
+ val strip_type: ctyp -> ctyp list * ctyp
val all_name: Proof.context -> string * cterm -> cterm -> cterm
val all: Proof.context -> cterm -> cterm -> cterm
val mk_binop: cterm -> cterm -> cterm -> cterm
@@ -142,7 +144,25 @@
val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
-(* cterm constructors and destructors *)
+(* ctyp operations *)
+
+fun dest_funT cT =
+ (case Thm.typ_of cT of
+ Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end
+ | T => raise TYPE ("dest_funT", [T], []));
+
+(* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *)
+fun strip_type cT =
+ (case Thm.typ_of cT of
+ Type ("fun", _) =>
+ let
+ val (cT1, cT2) = dest_funT cT;
+ val (cTs, cT') = strip_type cT2
+ in (cT1 :: cTs, cT') end
+ | _ => ([], cT));
+
+
+(* cterm operations *)
fun all_name ctxt (x, t) A =
let
--- a/src/Pure/thm.ML Sun Apr 14 11:59:54 2019 +0100
+++ b/src/Pure/thm.ML Sun Apr 14 12:00:17 2019 +0100
@@ -25,6 +25,10 @@
val global_ctyp_of: theory -> typ -> ctyp
val ctyp_of: Proof.context -> typ -> ctyp
val dest_ctyp: ctyp -> ctyp list
+ val dest_ctypN: int -> ctyp -> ctyp
+ val dest_ctyp0: ctyp -> ctyp
+ val dest_ctyp1: ctyp -> ctyp
+ val make_ctyp: ctyp -> ctyp list -> ctyp
(*certified terms*)
val term_of: cterm -> term
val typ_of_cterm: cterm -> typ
@@ -80,6 +84,7 @@
val trim_context_ctyp: ctyp -> ctyp
val trim_context_cterm: cterm -> cterm
val trim_context: thm -> thm
+ val transfer_ctyp: theory -> ctyp -> ctyp
val transfer_cterm: theory -> cterm -> cterm
val transfer: theory -> thm -> thm
val transfer': Proof.context -> thm -> thm
@@ -174,6 +179,37 @@
map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts
| dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
+fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) =
+ let fun err () = raise TYPE ("dest_ctypN", [T], []) in
+ (case T of
+ Type (_, Ts) =>
+ Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (),
+ maxidx = maxidx, sorts = sorts}
+ | _ => err ())
+ end;
+
+val dest_ctyp0 = dest_ctypN 0;
+val dest_ctyp1 = dest_ctypN 1;
+
+fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
+fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
+fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);
+
+fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs =
+ let
+ val As = map typ_of cargs;
+ fun err () = raise TYPE ("make_ctyp", T :: As, []);
+ in
+ (case T of
+ Type (a, args) =>
+ Ctyp {
+ cert = fold join_certificate_ctyp cargs cert,
+ maxidx = fold maxidx_ctyp cargs ~1,
+ sorts = fold union_sorts_ctyp cargs [],
+ T = if length args = length cargs then Type (a, As) else err ()}
+ | _ => err ())
+ end;
+
(** certified terms **)
@@ -444,6 +480,19 @@
{cert = Context.Certificate_Id (Context.theory_id thy),
tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}));
+fun transfer_ctyp thy' cT =
+ let
+ val Ctyp {cert, T, maxidx, sorts} = cT;
+ val _ =
+ Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
+ raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [],
+ SOME (Context.Theory thy'));
+ val cert' = Context.join_certificate (Context.Certificate thy', cert);
+ in
+ if Context.eq_certificate (cert, cert') then cT
+ else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts}
+ end;
+
fun transfer_cterm thy' ct =
let
val Cterm {cert, t, T, maxidx, sorts} = ct;