--- a/src/HOL/Library/positivstellensatz.ML Sat Apr 13 15:14:15 2019 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Sat Apr 13 16:26:19 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 = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
+ val T = Thm.dest_ctyp_nth 0 (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/Quickcheck/random_generators.ML Sat Apr 13 15:14:15 2019 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Apr 13 16:26:19 2019 +0200
@@ -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_ctyp_nth 1
|> 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 15:14:15 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Sat Apr 13 16:26:19 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> SMT_Util.destT1
+ val pat = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>pat\<close> (Thm.dest_ctyp_nth 0)
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 15:14:15 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Sat Apr 13 16:26:19 2019 +0200
@@ -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_ctyp_nth 0)
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 15:14:15 2019 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Sat Apr 13 16:26:19 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> SMT_Util.destT1
+val eq = SMT_Util.mk_const_pat \<^theory> \<^const_name>\<open>HOL.eq\<close> (Thm.dest_ctyp_nth 0)
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_ctyp_nth 0 o Thm.dest_ctyp_nth 1)
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_ctyp_nth 0)
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_ctyp_nth 0)
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/groebner.ML Sat Apr 13 15:14:15 2019 +0200
+++ b/src/HOL/Tools/groebner.ML Sat Apr 13 16:26:19 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 = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
+ val T = Thm.dest_ctyp_nth 0 (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/thm.ML Sat Apr 13 15:14:15 2019 +0200
+++ b/src/Pure/thm.ML Sat Apr 13 16:26:19 2019 +0200
@@ -25,6 +25,7 @@
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
(*certified terms*)
val term_of: cterm -> term
val typ_of_cterm: cterm -> typ
@@ -174,6 +175,10 @@
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 = Type (_, Ts), maxidx, sorts}) =
+ Ctyp {cert = cert, T = nth Ts i, maxidx = maxidx, sorts = sorts}
+ | dest_ctyp_nth _ cT = raise TYPE ("dest_ctyp_nth", [typ_of cT], []);
+
(** certified terms **)