# HG changeset patch # User wenzelm # Date 1555186000 -7200 # Node ID 57503fe1b0ff293b56bf416d84f9e46e7e66b93d # Parent a3d5e561e18a3be10c976b410fa0db1d058754bc tuned signature; diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Library/positivstellensatz.ML --- 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>\Trueprop\ $ (Const(\<^const_name>\Ex\,_)$_) => 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) diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/Meson/meson_clausify.ML --- 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') diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/Qelim/qelim.ML --- 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>\All\, _)$_ => 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)) diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/Quickcheck/random_generators.ML --- 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}, diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/SMT/smt_normalize.ML --- 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>\pat\ (Thm.dest_ctyp_nth 0) + val pat = SMT_Util.mk_const_pat \<^theory> \<^const_name>\pat\ Thm.dest_ctyp0 fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct fun mk_clist T = diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/SMT/smt_util.ML --- 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>\Trueprop\ $ _ => Thm.dest_arg ct | _ => raise CTERM ("not a property", [ct])) -val equals = mk_const_pat \<^theory> \<^const_name>\Pure.eq\ (Thm.dest_ctyp_nth 0) +val equals = mk_const_pat \<^theory> \<^const_name>\Pure.eq\ Thm.dest_ctyp0 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 a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/SMT/z3_interface.ML --- 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>\HOL.eq\ (Thm.dest_ctyp_nth 0) +val eq = SMT_Util.mk_const_pat \<^theory> \<^const_name>\HOL.eq\ 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>\If\ (Thm.dest_ctyp_nth 0 o Thm.dest_ctyp_nth 1) + SMT_Util.mk_const_pat \<^theory> \<^const_name>\If\ (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>\fun_app\ (Thm.dest_ctyp_nth 0) +val access = SMT_Util.mk_const_pat \<^theory> \<^const_name>\fun_app\ 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>\fun_upd\ (Thm.dest_ctyp o Thm.dest_ctyp_nth 0) + SMT_Util.mk_const_pat \<^theory> \<^const_name>\fun_upd\ (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 diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/Transfer/transfer.ML --- 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} diff -r a3d5e561e18a -r 57503fe1b0ff src/HOL/Tools/groebner.ML --- 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>\Trueprop\ $ (Const(\<^const_name>\Ex\,_)$_) => 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) diff -r a3d5e561e18a -r 57503fe1b0ff src/Pure/more_thm.ML --- 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)); diff -r a3d5e561e18a -r 57503fe1b0ff src/Pure/thm.ML --- 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);