# HG changeset patch # User wenzelm # Date 1555165579 -7200 # Node ID cf408ea5f5057aa3223dc35af52a2770d5245f83 # Parent 5e60443f5ad4d6e2e141abbc2c23ad1d57bda7b0 tuned signature -- more ctyp operations; diff -r 5e60443f5ad4 -r cf408ea5f505 src/HOL/Library/positivstellensatz.ML --- 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>\Trueprop\ $ (Const(\<^const_name>\Ex\,_)$_) => 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) diff -r 5e60443f5ad4 -r cf408ea5f505 src/HOL/Tools/Quickcheck/random_generators.ML --- 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}, diff -r 5e60443f5ad4 -r cf408ea5f505 src/HOL/Tools/SMT/smt_normalize.ML --- 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>\pat\ SMT_Util.destT1 + val pat = SMT_Util.mk_const_pat \<^theory> \<^const_name>\pat\ (Thm.dest_ctyp_nth 0) fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct fun mk_clist T = diff -r 5e60443f5ad4 -r cf408ea5f505 src/HOL/Tools/SMT/smt_util.ML --- 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>\Trueprop\ $ _ => Thm.dest_arg ct | _ => raise CTERM ("not a property", [ct])) -val equals = mk_const_pat \<^theory> \<^const_name>\Pure.eq\ destT1 +val equals = mk_const_pat \<^theory> \<^const_name>\Pure.eq\ (Thm.dest_ctyp_nth 0) fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu val dest_prop = (fn \<^const>\Trueprop\ $ t => t | t => t) diff -r 5e60443f5ad4 -r cf408ea5f505 src/HOL/Tools/SMT/z3_interface.ML --- 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>\HOL.eq\ SMT_Util.destT1 +val eq = SMT_Util.mk_const_pat \<^theory> \<^const_name>\HOL.eq\ (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>\If\ (SMT_Util.destT1 o SMT_Util.destT2) + SMT_Util.mk_const_pat \<^theory> \<^const_name>\If\ (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>\fun_app\ SMT_Util.destT1 +val access = SMT_Util.mk_const_pat \<^theory> \<^const_name>\fun_app\ (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>\fun_upd\ (Thm.dest_ctyp o SMT_Util.destT1) + SMT_Util.mk_const_pat \<^theory> \<^const_name>\fun_upd\ (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 diff -r 5e60443f5ad4 -r cf408ea5f505 src/HOL/Tools/groebner.ML --- 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>\Trueprop\ $ (Const(\<^const_name>\Ex\,_)$_) => 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) diff -r 5e60443f5ad4 -r cf408ea5f505 src/Pure/thm.ML --- 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 **)