--- a/src/HOL/Library/positivstellensatz.ML Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Sat Apr 13 22:06:40 2019 +0200
@@ -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 = Thm.dest_ctyp_nth 0 (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/Tools/Meson/meson_clausify.ML Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Apr 13 22:06:40 2019 +0200
@@ -98,7 +98,7 @@
let
val Abs (_, _, body) = Thm.term_of ct
val (x, cbody) = Thm.dest_abs NONE ct
- val (A, cbodyT) = Thm.dest_ctyp_fun (Thm.ctyp_of_cterm 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
@@ -111,7 +111,7 @@
if Term.is_dependent rand then (*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_ctyp_fun (Thm.dest_ctyp_nth 1 (Thm.ctyp_of_cterm crator))
+ 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')
@@ -121,7 +121,7 @@
else (*C*)
let val crator = Thm.lambda x (Thm.dest_fun cbody)
val crand = Thm.dest_arg cbody
- val (C, B) = Thm.dest_ctyp_fun (Thm.dest_ctyp_nth 1 (Thm.ctyp_of_cterm crator))
+ 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')
@@ -133,7 +133,7 @@
else (*B*)
let val crator = Thm.dest_fun cbody
val crand = Thm.lambda x (Thm.dest_arg cbody)
- val (C, B) = Thm.dest_ctyp_fun (Thm.ctyp_of_cterm crator)
+ 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')
--- a/src/HOL/Tools/Qelim/qelim.ML Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Sat Apr 13 22:06:40 2019 +0200
@@ -44,7 +44,7 @@
| Const(\<^const_name>\<open>All\<close>, _)$_ =>
let
val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
- val T = Thm.dest_ctyp_nth 0 (Thm.dest_ctyp_nth 0 allT)
+ 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 Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Apr 13 22:06:40 2019 +0200
@@ -75,7 +75,7 @@
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 |> Thm.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 Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Sat Apr 13 22:06:40 2019 +0200
@@ -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> (Thm.dest_ctyp_nth 0)
+ 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 Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Sat Apr 13 22:06:40 2019 +0200
@@ -203,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> (Thm.dest_ctyp_nth 0)
+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 Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Sat Apr 13 22:06:40 2019 +0200
@@ -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> (Thm.dest_ctyp_nth 0)
+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> (Thm.dest_ctyp_nth 0 o Thm.dest_ctyp_nth 1)
+ 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> (Thm.dest_ctyp_nth 0)
+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 Thm.dest_ctyp_nth 0)
+ 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 Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Sat Apr 13 22:06:40 2019 +0200
@@ -214,8 +214,8 @@
val Rel_rule = Thm.symmetric @{thm Rel_def}
fun Rel_conv ct =
- let val (cT, cT') = Thm.dest_ctyp_fun (Thm.ctyp_of_cterm ct)
- val (cU, _) = Thm.dest_ctyp_fun 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 *)
@@ -461,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 Thm.dest_ctyp_fun (Thm.dest_ctyp_fun (Thm.ctyp_of_cterm r1))
- val (a2, (b2, _)) = apsnd Thm.dest_ctyp_fun (Thm.dest_ctyp_fun (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 Sat Apr 13 21:51:24 2019 +0200
+++ b/src/HOL/Tools/groebner.ML Sat Apr 13 22:06:40 2019 +0200
@@ -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 = Thm.dest_ctyp_nth 0 (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/more_thm.ML Sat Apr 13 21:51:24 2019 +0200
+++ b/src/Pure/more_thm.ML Sat Apr 13 22:06:40 2019 +0200
@@ -28,7 +28,7 @@
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_ctyp_fun: ctyp -> ctyp * ctyp
+ 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
@@ -146,17 +146,17 @@
(* ctyp operations *)
-fun dest_ctyp_fun cT =
+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_ctyp_fun", [T], []));
+ | 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_ctyp_fun cT;
+ val (cT1, cT2) = dest_funT cT;
val (cTs, cT') = strip_type cT2
in (cT1 :: cTs, cT') end
| _ => ([], cT));
--- a/src/Pure/thm.ML Sat Apr 13 21:51:24 2019 +0200
+++ b/src/Pure/thm.ML Sat Apr 13 22:06:40 2019 +0200
@@ -25,7 +25,9 @@
val global_ctyp_of: theory -> typ -> ctyp
val ctyp_of: Proof.context -> typ -> ctyp
val dest_ctyp: ctyp -> ctyp list
- val dest_ctyp_nth: int -> ctyp -> ctyp
+ 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
@@ -177,15 +179,18 @@
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_ctyp_nth i (Ctyp {cert, T, maxidx, sorts}) =
- let fun err () = raise TYPE ("dest_ctyp_nth", [T], []) in
+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 i handle General.Subscript => err (),
+ 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);