--- a/src/HOL/Data_Structures/Define_Time_Function.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Wed Aug 07 20:56:31 2024 +0200
@@ -543,9 +543,9 @@
(* Print result if print *)
val _ = if not print then () else
let
- val nms = map (fst o dest_Const) term
+ val nms = map dest_Const_name term
val used = map (used_for_const orig_used) term
- val typs = map (snd o dest_Const) term
+ val typs = map dest_Const_type term
in
print_timing' print_ctxt { names=nms, terms=terms, typs=typs } { names=timing_names, terms=T_terms, typs=map (fn (used, typ) => change_typ' used 0 typ) (zip used typs) }
end
--- a/src/HOL/Finite_Set.thy Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Finite_Set.thy Wed Aug 07 20:56:31 2024 +0200
@@ -199,12 +199,12 @@
val Eq_TrueI = @{thm Eq_TrueI}
fun is_subset A th = case Thm.prop_of th of
- (_ $ (Const (\<^const_name>\<open>less_eq\<close>, Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>set\<close>, _), _])) $ A' $ B))
+ (_ $ \<^Const_>\<open>less_eq \<^Type>\<open>set _\<close> for A' B\<close>)
=> if A aconv A' then SOME(B,th) else NONE
| _ => NONE;
fun is_finite th = case Thm.prop_of th of
- (_ $ (Const (\<^const_name>\<open>finite\<close>, _) $ A)) => SOME(A,th)
+ (_ $ \<^Const_>\<open>finite _ for A\<close>) => SOME(A,th)
| _ => NONE;
fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths
--- a/src/HOL/Fun.thy Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Fun.thy Wed Aug 07 20:56:31 2024 +0200
@@ -1377,32 +1377,28 @@
simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>
let
- fun gen_fun_upd NONE T _ _ = NONE
- | gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y)
- fun dest_fun_T1 (Type (_, T :: Ts)) = T
- fun find_double (t as Const (\<^const_name>\<open>fun_upd\<close>,T) $ f $ x $ y) =
+ fun gen_fun_upd _ _ _ _ NONE = NONE
+ | gen_fun_upd A B x y (SOME f) = SOME \<^Const>\<open>fun_upd A B for f x y\<close>
+ fun find_double (t as \<^Const_>\<open>fun_upd A B for f x y\<close>) =
let
- fun find (Const (\<^const_name>\<open>fun_upd\<close>,T) $ g $ v $ w) =
- if v aconv x then SOME g else gen_fun_upd (find g) T v w
+ fun find \<^Const_>\<open>fun_upd _ _ for g v w\<close> =
+ if v aconv x then SOME g
+ else gen_fun_upd A B v w (find g)
| find t = NONE
- in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
+ in gen_fun_upd A B x y (find f) end
val ss = simpset_of \<^context>
-
- fun proc ctxt ct =
- let
- val t = Thm.term_of ct
- in
- (case find_double t of
- (T, NONE) => NONE
- | (T, SOME rhs) =>
- SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
- (fn _ =>
- resolve_tac ctxt [eq_reflection] 1 THEN
- resolve_tac ctxt @{thms ext} 1 THEN
- simp_tac (put_simpset ss ctxt) 1)))
+ in
+ fn _ => fn ctxt => fn ct =>
+ let val t = Thm.term_of ct in
+ find_double t |> Option.map (fn rhs =>
+ Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
+ (fn _ =>
+ resolve_tac ctxt [eq_reflection] 1 THEN
+ resolve_tac ctxt @{thms ext} 1 THEN
+ simp_tac (put_simpset ss ctxt) 1))
end
- in K proc end
+ end
\<close>
--- a/src/HOL/HOL.thy Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOL.thy Wed Aug 07 20:56:31 2024 +0200
@@ -818,11 +818,11 @@
setup \<open>
(*prevent substitution on bool*)
let
- fun non_bool_eq (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) = T <> \<^typ>\<open>bool\<close>
+ fun non_bool_eq \<^Const_>\<open>HOL.eq T\<close> = T <> \<^Type>\<open>bool\<close>
| non_bool_eq _ = false;
fun hyp_subst_tac' ctxt =
SUBGOAL (fn (goal, i) =>
- if Term.exists_Const non_bool_eq goal
+ if Term.exists_subterm non_bool_eq goal
then Hypsubst.hyp_subst_tac ctxt i
else no_tac);
in
@@ -1263,7 +1263,7 @@
| count_loose (s $ t) k = count_loose s k + count_loose t k
| count_loose (Abs (_, _, t)) k = count_loose t (k + 1)
| count_loose _ _ = 0;
- fun is_trivial_let (Const (\<^const_name>\<open>Let\<close>, _) $ x $ t) =
+ fun is_trivial_let \<^Const_>\<open>Let _ _ for x t\<close> =
(case t of
Abs (_, _, t') => count_loose t' 0 <= 1
| _ => true);
@@ -1277,7 +1277,7 @@
val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt;
in
Option.map (hd o Variable.export ctxt' ctxt o single)
- (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *)
+ (case t' of \<^Const_>\<open>Let _ _ for x f\<close> => (* x and f are already in normal form *)
if is_Free x orelse is_Bound x orelse is_Const x
then SOME @{thm Let_def}
else
@@ -1334,26 +1334,28 @@
"(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
by (rule swap_prems_eq)
-ML \<open>
-fun eliminate_false_implies ct =
+simproc_setup eliminate_false_implies ("False \<Longrightarrow> PROP P") = \<open>
let
- val (prems, concl) = Logic.strip_horn (Thm.term_of ct)
- fun go n =
+ fun conv n =
if n > 1 then
Conv.rewr_conv @{thm Pure.swap_prems_eq}
- then_conv Conv.arg_conv (go (n - 1))
+ then_conv Conv.arg_conv (conv (n - 1))
then_conv Conv.rewr_conv @{thm HOL.implies_True_equals}
else
Conv.rewr_conv @{thm HOL.False_implies_equals}
in
- case concl of
- Const (@{const_name HOL.Trueprop}, _) $ _ => SOME (go (length prems) ct)
- | _ => NONE
+ fn _ => fn _ => fn ct =>
+ let
+ val t = Thm.term_of ct
+ val n = length (Logic.strip_imp_prems t)
+ in
+ (case Logic.strip_imp_concl t of
+ \<^Const_>\<open>Trueprop for _\<close> => SOME (conv n ct)
+ | _ => NONE)
+ end
end
\<close>
-simproc_setup eliminate_false_implies ("False \<Longrightarrow> PROP P") = \<open>K (K eliminate_false_implies)\<close>
-
lemma ex_simps:
"\<And>P Q. (\<exists>x. P x \<and> Q) = ((\<exists>x. P x) \<and> Q)"
@@ -1536,7 +1538,7 @@
val rulify = @{thms induct_rulify'}
val rulify_fallback = @{thms induct_rulify_fallback}
val equal_def = @{thm induct_equal_def}
- fun dest_def (Const (\<^const_name>\<open>induct_equal\<close>, _) $ t $ u) = SOME (t, u)
+ fun dest_def \<^Const_>\<open>induct_equal _ for t u\<close> = SOME (t, u)
| dest_def _ = NONE
fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
)
@@ -1937,7 +1939,7 @@
simproc_setup passive equal (HOL.eq) =
\<open>fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
- Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
+ \<^Const_>\<open>HOL.eq T\<close> => if is_Type T then SOME @{thm eq_equal} else NONE
| _ => NONE)\<close>
setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>equal\<close>])\<close>
@@ -2153,7 +2155,7 @@
ML \<open>
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
local
- fun wrong_prem (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = wrong_prem t
+ fun wrong_prem \<^Const_>\<open>All _ for \<open>Abs (_, _, t)\<close>\<close> = wrong_prem t
| wrong_prem (Bound _) = true
| wrong_prem _ = false;
val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Aug 07 20:56:31 2024 +0200
@@ -112,7 +112,7 @@
: (term list * term list) =
let
val Ts = map snd args
- val ns = Name.variant_list taken (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list taken (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
in
@@ -167,7 +167,7 @@
fun vars_of args =
let
val Ts = map snd args
- val ns = Old_Datatype_Prop.make_tnames Ts
+ val ns = Case_Translation.make_tnames Ts
in
map Free (ns ~~ Ts)
end
@@ -409,7 +409,7 @@
val tns = map fst (Term.add_tfreesT lhsT [])
val resultT = TFree (singleton (Name.variant_list tns) "'t", \<^sort>\<open>pcpo\<close>)
fun fTs T = map (fn (_, args) => map snd args -->> T) spec
- val fns = Old_Datatype_Prop.indexify_names (map (K "f") spec)
+ val fns = Case_Translation.indexify_names (map (K "f") spec)
val fs = map Free (fns ~~ fTs resultT)
fun caseT T = fTs T -->> (lhsT ->> T)
@@ -424,7 +424,7 @@
fun one_con f (_, args) =
let
val Ts = map snd args
- val ns = Name.variant_list fns (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list fns (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
in
lambda_args (map fst args ~~ vs) (list_ccomb (f, vs))
@@ -606,7 +606,7 @@
fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
let
val Ts : typ list = map #3 args
- val ns : string list = Old_Datatype_Prop.make_tnames Ts
+ val ns : string list = Case_Translation.make_tnames Ts
val vs : term list = map Free (ns ~~ Ts)
val con_app : term = list_ccomb (con, vs)
val vs' : (bool * term) list = map #1 args ~~ vs
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Aug 07 20:56:31 2024 +0200
@@ -63,7 +63,7 @@
fun prove_take_app (con_const, args) =
let
val Ts = map snd args
- val ns = Name.variant_list ["n"] (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list ["n"] (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs))
val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts)
@@ -108,8 +108,8 @@
val {take_consts, take_induct_thms, ...} = take_info
val newTs = map #absT iso_infos
- val P_names = Old_Datatype_Prop.indexify_names (map (K "P") newTs)
- val x_names = Old_Datatype_Prop.indexify_names (map (K "x") newTs)
+ val P_names = Case_Translation.indexify_names (map (K "P") newTs)
+ val x_names = Case_Translation.indexify_names (map (K "x") newTs)
val P_types = map (fn T => T --> \<^Type>\<open>bool\<close>) newTs
val Ps = map Free (P_names ~~ P_types)
val xs = map Free (x_names ~~ newTs)
@@ -118,7 +118,7 @@
fun con_assm defined p (con, args) =
let
val Ts = map snd args
- val ns = Name.variant_list P_names (Old_Datatype_Prop.make_tnames Ts)
+ val ns = Name.variant_list P_names (Case_Translation.make_tnames Ts)
val vs = map Free (ns ~~ Ts)
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
fun ind_hyp (v, T) t =
@@ -256,7 +256,7 @@
val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info
- val R_names = Old_Datatype_Prop.indexify_names (map (K "R") newTs)
+ val R_names = Case_Translation.indexify_names (map (K "R") newTs)
val R_types = map (fn T => T --> T --> \<^Type>\<open>bool\<close>) newTs
val Rs = map Free (R_names ~~ R_types)
val n = Free ("n", \<^Type>\<open>nat\<close>)
@@ -273,7 +273,7 @@
fun one_con T (con, args) =
let
val Ts = map snd args
- val ns1 = Name.variant_list reserved (Old_Datatype_Prop.make_tnames Ts)
+ val ns1 = Name.variant_list reserved (Case_Translation.make_tnames Ts)
val ns2 = map (fn n => n^"'") ns1
val vs1 = map Free (ns1 ~~ Ts)
val vs2 = map Free (ns2 ~~ Ts)
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Aug 07 20:56:31 2024 +0200
@@ -422,7 +422,7 @@
: (term list * term list) =
let
val Ts = map snd args;
- val ns = Name.variant_list taken (Old_Datatype_Prop.make_tnames Ts);
+ val ns = Name.variant_list taken (Case_Translation.make_tnames Ts);
val vs = map Free (ns ~~ Ts);
val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
in
@@ -469,10 +469,10 @@
val Ts = map snd args;
val Vs =
(map (K "'t") args)
- |> Old_Datatype_Prop.indexify_names
+ |> Case_Translation.indexify_names
|> Name.variant_list tns
|> map (fn t => TFree (t, \<^sort>\<open>pcpo\<close>));
- val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args);
+ val patNs = Case_Translation.indexify_names (map (K "pat") args);
val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
val pats = map Free (patNs ~~ patTs);
val fail = mk_fail (mk_tupleT Vs);
@@ -535,10 +535,10 @@
val Ts = map snd args;
val Vs =
(map (K "'t") args)
- |> Old_Datatype_Prop.indexify_names
+ |> Case_Translation.indexify_names
|> Name.variant_list (rn::tns)
|> map (fn t => TFree (t, \<^sort>\<open>pcpo\<close>));
- val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args);
+ val patNs = Case_Translation.indexify_names (map (K "pat") args);
val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
val pats = map Free (patNs ~~ patTs);
val k = Free ("rhs", mk_tupleT Vs ->> R);
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Aug 07 20:56:31 2024 +0200
@@ -214,7 +214,7 @@
val perm_types = map (fn (i, _) =>
let val T = nth_dtyp i
in permT --> T --> T end) descr;
- val perm_names' = Old_Datatype_Prop.indexify_names (map (fn (i, _) =>
+ val perm_names' = Case_Translation.indexify_names (map (fn (i, _) =>
"perm_" ^ Old_Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
val perm_names = replicate (length new_type_names) \<^const_name>\<open>Nominal.perm\<close> @
map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
@@ -226,7 +226,7 @@
in map (fn (cname, dts) =>
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) dts;
- val names = Name.variant_list ["pi"] (Old_Datatype_Prop.make_tnames Ts);
+ val names = Name.variant_list ["pi"] (Case_Translation.make_tnames Ts);
val args = map Free (names ~~ Ts);
val c = Const (cname, Ts ---> T);
fun perm_arg (dt, x) =
@@ -264,7 +264,7 @@
val _ = warning ("length descr: " ^ string_of_int (length descr));
val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
- val perm_indnames = Old_Datatype_Prop.make_tnames (map body_type perm_types);
+ val perm_indnames = Case_Translation.make_tnames (map body_type perm_types);
val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
val unfolded_perm_eq_thms =
@@ -465,10 +465,10 @@
val _ = warning "representing sets";
val rep_set_names =
- Old_Datatype_Prop.indexify_names
+ Case_Translation.indexify_names
(map (fn (i, _) => Old_Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
val big_rep_name =
- space_implode "_" (Old_Datatype_Prop.indexify_names (map_filter
+ space_implode "_" (Case_Translation.indexify_names (map_filter
(fn (i, (\<^type_name>\<open>noption\<close>, _, _)) => NONE
| (i, _) => SOME (Old_Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
val _ = warning ("big_rep_name: " ^ big_rep_name);
@@ -1084,7 +1084,7 @@
val _ = warning "proving finite support for the new datatype";
- val indnames = Old_Datatype_Prop.make_tnames recTs;
+ val indnames = Case_Translation.make_tnames recTs;
val abs_supp = Global_Theory.get_thms thy8 "abs_supp";
val supp_atm = Global_Theory.get_thms thy8 "supp_atm";
@@ -1147,7 +1147,7 @@
val fsT' = TFree ("'n", \<^sort>\<open>type\<close>);
val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
- (Old_Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
+ (Case_Translation.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
fun make_pred fsT i T = Free (nth pnames i, fsT --> T --> HOLogic.boolT);
@@ -1168,7 +1168,7 @@
val recs = filter Old_Datatype_Aux.is_rec_type cargs;
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr'') cargs;
val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr'') recs;
- val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
+ val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val frees' = partition_cargs idxs frees;
@@ -1202,7 +1202,7 @@
map (make_ind_prem fsT (fn T => fn t => fn u =>
fresh_const T fsT $ t $ u) i T)
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
- val tnames = Old_Datatype_Prop.make_tnames recTs;
+ val tnames = Case_Translation.make_tnames recTs;
val zs = Name.variant_list tnames (replicate (length descr'') "z");
val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
(map (fn ((((i, _), T), tname), z) =>
@@ -1226,7 +1226,7 @@
val induct' = Logic.list_implies (ind_prems', ind_concl');
val aux_ind_vars =
- (Old_Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
+ (Case_Translation.indexify_names (replicate (length dt_atomTs) "pi") ~~
map mk_permT dt_atomTs) @ [("z", fsT')];
val aux_ind_Ts = rev (map snd aux_ind_vars);
val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
@@ -1679,10 +1679,10 @@
val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
val fun_tupleT = fastype_of fun_tuple;
val rec_unique_frees =
- Old_Datatype_Prop.indexify_names (replicate (length recTs) "x") ~~ recTs;
+ Case_Translation.indexify_names (replicate (length recTs) "x") ~~ recTs;
val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
val rec_unique_frees' =
- Old_Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
+ Case_Translation.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
val rec_unique_concls = map (fn ((x, U), R) =>
Const (\<^const_name>\<open>Ex1\<close>, (U --> HOLogic.boolT) --> HOLogic.boolT) $
Abs ("y", U, R $ Free x $ Bound 0))
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Aug 07 20:56:31 2024 +0200
@@ -250,7 +250,7 @@
end) prems);
val ind_vars =
- (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+ (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~
map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
val ind_Ts = rev (map snd ind_vars);
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Aug 07 20:56:31 2024 +0200
@@ -267,7 +267,7 @@
in abs_params params' prem end) prems);
val ind_vars =
- (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+ (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~
map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
val ind_Ts = rev (map snd ind_vars);
--- a/src/HOL/Product_Type.thy Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Product_Type.thy Wed Aug 07 20:56:31 2024 +0200
@@ -1334,22 +1334,22 @@
simproc_setup Collect_mem ("Collect t") = \<open>
K (fn ctxt => fn ct =>
(case Thm.term_of ct of
- S as Const (\<^const_name>\<open>Collect\<close>, Type (\<^type_name>\<open>fun\<close>, [_, T])) $ t =>
+ S as \<^Const_>\<open>Collect A for t\<close> =>
let val (u, _, ps) = HOLogic.strip_ptupleabs t in
(case u of
- (c as Const (\<^const_name>\<open>Set.member\<close>, _)) $ q $ S' =>
+ (c as \<^Const_>\<open>Set.member _ for q S'\<close>) =>
(case try (HOLogic.strip_ptuple ps) q of
NONE => NONE
| SOME ts =>
if not (Term.is_open S') andalso
ts = map Bound (length ps downto 0)
then
- let val simp =
- full_simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
+ let
+ val simp =
+ full_simp_tac (put_simpset HOL_basic_ss ctxt
+ addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
in
- SOME (Goal.prove ctxt [] []
- (Const (\<^const_name>\<open>Pure.eq\<close>, T --> T --> propT) $ S $ S')
+ SOME (Goal.prove ctxt [] [] \<^Const>\<open>Pure.eq \<^Type>\<open>set A\<close> for S S'\<close>
(K (EVERY
[resolve_tac ctxt [eq_reflection] 1,
resolve_tac ctxt @{thms subset_antisym} 1,
--- a/src/HOL/Set.thy Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Set.thy Wed Aug 07 20:56:31 2024 +0200
@@ -251,7 +251,7 @@
else raise Match;
fun tr' q = (q, fn _ =>
- (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, Type (\<^type_name>\<open>set\<close>, _)),
+ (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, \<^Type>\<open>set _\<close>),
Const (c, _) $
(Const (d, _) $ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v', T)) $ n) $ P] =>
(case AList.lookup (=) trans (q, c, d) of
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Aug 07 20:56:31 2024 +0200
@@ -417,9 +417,7 @@
fold safe_instantiate_bound bindings' ([], HOLogic.dest_Trueprop orig_parent_fmla)
|> snd (*discard var typing context*)
|> close_formula
- |> single
- |> Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy))
- |> the_single
+ |> singleton (Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy)))
|> HOLogic.mk_Trueprop
|> rpair bindings'
end
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Aug 07 20:56:31 2024 +0200
@@ -1028,8 +1028,7 @@
val deadfixed_T =
build_map lthy [] [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
- |> singleton (Type_Infer_Context.infer_types lthy)
- |> singleton (Type_Infer.fixate lthy false)
+ |> singleton (Type_Infer_Context.infer_types_finished lthy)
|> type_of
|> dest_funT
|-> generalize_types 1
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Aug 07 20:56:31 2024 +0200
@@ -731,7 +731,7 @@
| rename t _ = t
val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
- val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
+ val new_names = Case_Translation.make_tnames (all_typs fixed_def_t)
in
rename term new_names
end
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 07 20:56:31 2024 +0200
@@ -58,8 +58,8 @@
lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
fun polish_hol_terms ctxt (lifted, old_skolems) =
- map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
- #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
+ map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) #>
+ Type_Infer_Context.infer_types_finished (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
Metis_Thm.clause
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Aug 07 20:56:31 2024 +0200
@@ -157,7 +157,7 @@
let
val goal = Thm.term_of cgoal;
val params = Logic.strip_params goal;
- val (_, Type (tname, _)) = hd (rev params);
+ val tname = dest_Type_name (#2 (hd (rev params)));
val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname);
val prem' = hd (Thm.prems_of exhaustion);
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
@@ -228,25 +228,32 @@
fun mk_fun_dtyp [] U = U
| mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
-fun name_of_typ (Type (s, Ts)) =
- let val s' = Long_Name.base_name s in
- space_implode "_"
- (filter_out (equal "") (map name_of_typ Ts) @
- [if Symbol_Pos.is_identifier s' then s' else "x"])
- end
- | name_of_typ _ = "";
+fun name_of_typ ty =
+ if is_Type ty then
+ let
+ val name = Long_Name.base_name (dest_Type_name ty)
+ val Ts = dest_Type_args ty
+ in
+ space_implode "_"
+ (filter_out (equal "") (map name_of_typ Ts) @
+ [if Symbol_Pos.is_identifier name then name else "x"])
+ end
+ else "";
fun dtyp_of_typ _ (TFree a) = DtTFree a
- | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
- | dtyp_of_typ new_dts (Type (tname, Ts)) =
- (case AList.lookup (op =) new_dts tname of
- NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
- | SOME vs =>
- if map (try dest_TFree) Ts = map SOME vs then
- DtRec (find_index (curry op = tname o fst) new_dts)
- else error ("Illegal occurrence of recursive type " ^ quote tname));
+ | dtyp_of_typ new_dts T =
+ if is_TVar T then error "Illegal schematic type variable(s)"
+ else
+ let val (tname, Ts) = dest_Type T in
+ (case AList.lookup (op =) new_dts tname of
+ NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
+ | SOME vs =>
+ if map (try dest_TFree) Ts = map SOME vs then
+ DtRec (find_index (curry op = tname o fst) new_dts)
+ else error ("Illegal occurrence of recursive type " ^ quote tname))
+ end;
-fun typ_of_dtyp descr (DtTFree a) = TFree a
+fun typ_of_dtyp _ (DtTFree a) = TFree a
| typ_of_dtyp descr (DtRec i) =
let val (s, ds, _) = the (AList.lookup (op =) descr i)
in Type (s, map (typ_of_dtyp descr) ds) end
--- a/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML Wed Aug 07 20:56:31 2024 +0200
@@ -15,7 +15,7 @@
let
val ctxt = Proof_Context.init_global thy
val SOME {ctrs, injects, distincts, case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt fcT_name
- val Type (_, As) = body_type (fastype_of (hd ctrs))
+ val As = dest_Type_args (body_type (fastype_of (hd ctrs)))
in
Ctr_Sugar_Code.add_ctr_code fcT_name As (map dest_Const ctrs) injects distincts case_thms thy
end;
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Aug 07 20:56:31 2024 +0200
@@ -63,19 +63,17 @@
let
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
in
- (case body_type T of
- Type (tyco, _) => AList.lookup (op =) tab tyco
- | _ => NONE)
+ try (dest_Type_name o body_type) T
+ |> Option.mapPartial (AList.lookup (op =) tab)
end;
fun info_of_constr_permissive thy (c, T) =
let
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
- val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE);
val default = if null tab then NONE else SOME (snd (List.last tab));
(*conservative wrt. overloaded constructors*)
in
- (case hint of
+ (case try (dest_Type_name o body_type) T of
NONE => default
| SOME tyco =>
(case AList.lookup (op =) tab tyco of
@@ -185,8 +183,9 @@
fun all_distincts thy Ts =
let
- fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
- | add_tycos _ = I;
+ fun add_tycos T =
+ if is_Type T
+ then insert (op =) (dest_Type_name T) #> fold add_tycos (dest_Type_args T) else I;
val tycos = fold add_tycos Ts [];
in map_filter (Option.map #distinct o get_info thy) tycos end;
@@ -221,7 +220,7 @@
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
fun induct_cases descr =
- Old_Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr));
+ Case_Translation.indexify_names (maps (dt_cases descr) (map #2 descr));
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
--- a/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Wed Aug 07 20:56:31 2024 +0200
@@ -7,8 +7,6 @@
signature OLD_DATATYPE_PROP =
sig
type descr = Old_Datatype_Aux.descr
- val indexify_names: string list -> string list
- val make_tnames: typ list -> string list
val make_injs : descr list -> term list list
val make_distincts : descr list -> term list list (*no symmetric inequalities*)
val make_ind : descr list -> term
@@ -29,18 +27,6 @@
type descr = Old_Datatype_Aux.descr;
-val indexify_names = Case_Translation.indexify_names;
-val make_tnames = Case_Translation.make_tnames;
-
-fun make_tnames Ts =
- let
- fun type_name (TFree (name, _)) = unprefix "'" name
- | type_name (Type (name, _)) =
- let val name' = Long_Name.base_name name
- in if Symbol_Pos.is_identifier name' then name' else "x" end;
- in indexify_names (map type_name Ts) end;
-
-
(************************* injectivity of constructors ************************)
fun make_injs descr =
@@ -52,7 +38,7 @@
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
val constr_t = Const (cname, Ts ---> T);
- val tnames = make_tnames Ts;
+ val tnames = Case_Translation.make_tnames Ts;
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (map (suffix "'") tnames ~~ Ts);
in
@@ -80,12 +66,13 @@
fun make_distincts' _ [] = []
| make_distincts' T ((cname, cargs) :: constrs) =
let
- val frees = map Free (make_tnames cargs ~~ cargs);
+ val frees = map Free (Case_Translation.make_tnames cargs ~~ cargs);
val t = list_comb (Const (cname, cargs ---> T), frees);
fun make_distincts'' (cname', cargs') =
let
- val frees' = map Free (map (suffix "'") (make_tnames cargs') ~~ cargs');
+ val frees' =
+ map Free (map (suffix "'") (Case_Translation.make_tnames cargs') ~~ cargs');
val t' = list_comb (Const (cname', cargs' ---> T), frees');
in
HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t'))
@@ -107,9 +94,7 @@
if length descr' = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
- fun make_pred i T =
- let val T' = T --> HOLogic.boolT
- in Free (nth pnames i, T') end;
+ fun make_pred i T = Free (nth pnames i, T --> \<^Type>\<open>bool\<close>);
fun make_ind_prem k T (cname, cargs) =
let
@@ -125,7 +110,7 @@
val recs = filter Old_Datatype_Aux.is_rec_type cargs;
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr') recs;
- val tnames = Name.variant_list pnames (make_tnames Ts);
+ val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
@@ -138,7 +123,7 @@
val prems =
maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs);
- val tnames = make_tnames recTs;
+ val tnames = Case_Translation.make_tnames recTs;
val concl =
HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
@@ -155,18 +140,18 @@
fun make_casedist_prem T (cname, cargs) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
+ val frees = Name.variant_list ["P", "y"] (Case_Translation.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
in
fold_rev (Logic.all o Free) frees
(Logic.mk_implies (HOLogic.mk_Trueprop
(HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
- HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
+ HOLogic.mk_Trueprop (Free ("P", \<^Type>\<open>bool\<close>))))
end;
fun make_casedist ((_, (_, _, constrs))) T =
let val prems = map (make_casedist_prem T) constrs
- in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))) end;
+ in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", \<^Type>\<open>bool\<close>))) end;
in
map2 make_casedist (hd descr)
@@ -219,7 +204,7 @@
val recs = filter Old_Datatype_Aux.is_rec_type cargs;
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr') recs;
- val tnames = make_tnames Ts;
+ val tnames = Case_Translation.make_tnames Ts;
val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (rec_tnames ~~ recTs');
@@ -276,7 +261,7 @@
fun make_case T comb_t ((cname, cargs), f) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val frees = map Free ((make_tnames Ts) ~~ Ts);
+ val frees = map Free ((Case_Translation.make_tnames Ts) ~~ Ts);
in
HOLogic.mk_Trueprop
(HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
@@ -298,7 +283,7 @@
val used' = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used') "'t", \<^sort>\<open>type\<close>);
- val P = Free ("P", T' --> HOLogic.boolT);
+ val P = Free ("P", T' --> \<^Type>\<open>bool\<close>);
fun make_split (((_, (_, _, constrs)), T), comb_t) =
let
@@ -308,7 +293,7 @@
fun process_constr ((cname, cargs), f) (t1s, t2s) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
+ val frees = map Free (Name.variant_list used (Case_Translation.make_tnames Ts) ~~ Ts);
val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees));
val P' = P $ list_comb (f, frees);
in
@@ -337,7 +322,7 @@
fun mk_case_cong comb =
let
- val Type ("fun", [T, _]) = fastype_of comb;
+ val \<^Type>\<open>fun T _\<close> = fastype_of comb;
val M = Free ("M", T);
val M' = Free ("M'", T);
in
@@ -367,7 +352,7 @@
fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
let
- val Type ("fun", [T, _]) = fastype_of comb;
+ val \<^Type>\<open>fun T _\<close> = fastype_of comb;
val (_, fs) = strip_comb comb;
val (_, gs) = strip_comb comb';
val used = ["M", "M'"] @ map (fst o dest_Free) (fs @ gs);
@@ -377,7 +362,7 @@
fun mk_clause ((f, g), (cname, _)) =
let
val Ts = binder_types (fastype_of f);
- val tnames = Name.variant_list used (make_tnames Ts);
+ val tnames = Name.variant_list used (Case_Translation.make_tnames Ts);
val frees = map Free (tnames ~~ Ts);
in
fold_rev Logic.all frees
@@ -411,7 +396,7 @@
fun mk_eqn T (cname, cargs) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val tnames = Name.variant_list ["v"] (make_tnames Ts);
+ val tnames = Name.variant_list ["v"] (Case_Translation.make_tnames Ts);
val frees = tnames ~~ Ts;
in
fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Wed Aug 07 20:56:31 2024 +0200
@@ -144,7 +144,7 @@
(case AList.lookup (op =) eqns cname of
NONE => (warning ("No equation for constructor " ^ quote cname ^
"\nin definition of function " ^ quote fname);
- (fnames', fnss', (Const (\<^const_name>\<open>undefined\<close>, dummyT)) :: fns))
+ (fnames', fnss', \<^Const>\<open>undefined dummyT\<close> :: fns))
| SOME (ls, cargs', rs, rhs, eq) =>
let
val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
@@ -183,9 +183,9 @@
(case AList.lookup (op =) fns i of
NONE =>
let
- val dummy_fns = map (fn (_, cargs) => Const (\<^const_name>\<open>undefined\<close>,
- replicate (length cargs + length (filter Old_Datatype_Aux.is_rec_type cargs))
- dummyT ---> HOLogic.unitT)) constrs;
+ val dummy_fns = map (fn (_, cargs) => \<^Const>\<open>undefined
+ \<open>replicate (length cargs + length (filter Old_Datatype_Aux.is_rec_type cargs))
+ dummyT ---> HOLogic.unitT\<close>\<close>) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)
in
(dummy_fns @ fs, defs)
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Aug 07 20:56:31 2024 +0200
@@ -40,11 +40,10 @@
fun prove_casedist_thm (i, (T, t)) =
let
- val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
- Abs ("z", T', Const (\<^const_name>\<open>True\<close>, T''))) induct_Ps;
+ val dummyPs = map (fn Var (_, \<^Type>\<open>fun A _\<close>) => Abs ("z", A, \<^Const>\<open>True\<close>)) induct_Ps;
val P =
Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
- Var (("P", 0), HOLogic.boolT));
+ Var (("P", 0), \<^Type>\<open>bool\<close>));
val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
in
Goal.prove_sorry_global thy []
@@ -102,7 +101,7 @@
val (rec_result_Ts, reccomb_fn_Ts) = Old_Datatype_Prop.make_primrec_Ts descr used;
val rec_set_Ts =
- map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
+ map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> \<^Type>\<open>bool\<close>) (recTs ~~ rec_result_Ts);
val rec_fns =
map (uncurry (Old_Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto length reccomb_fn_Ts));
@@ -204,8 +203,8 @@
let
val rec_unique_ts =
map (fn (((set_t, T1), T2), i) =>
- Const (\<^const_name>\<open>Ex1\<close>, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
- absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
+ \<^Const>\<open>Ex1 T2 for
+ \<open>absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2))\<close>\<close>)
(rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
val insts =
map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
@@ -248,8 +247,7 @@
(fn ((((name, comb), set), T), T') =>
(Binding.name (Thm.def_name (Long_Name.base_name name)),
Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
- (Const (\<^const_name>\<open>The\<close>, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
- (set $ Free ("x", T) $ Free ("y", T')))))))
+ \<^Const>\<open>The T' for \<open>absfree ("y", T') (set $ Free ("x", T) $ Free ("y", T'))\<close>\<close>))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
||> Sign.parent_path;
@@ -303,43 +301,45 @@
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
val Ts' = map mk_dummyT (filter Old_Datatype_Aux.is_rec_type cargs)
- in Const (\<^const_name>\<open>undefined\<close>, Ts @ Ts' ---> T') end) constrs) descr';
+ in \<^Const>\<open>undefined \<open>Ts @ Ts' ---> T'\<close>\<close> end) constrs) descr';
val case_names0 = map (fn s => Sign.full_bname thy1 ("case_" ^ s)) new_type_names;
(* define case combinators via primrec combinators *)
- fun def_case ((((i, (_, _, constrs)), T as Type (Tcon, _)), name), recname) (defs, thy) =
- if is_some (Ctr_Sugar.ctr_sugar_of ctxt Tcon) then
- (defs, thy)
- else
- let
- val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
- let
- val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
- val Ts' = Ts @ map mk_dummyT (filter Old_Datatype_Aux.is_rec_type cargs);
- val frees' = map2 (Old_Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
- val frees = take (length cargs) frees';
- val free = Old_Datatype_Aux.mk_Free "f" (Ts ---> T') j;
- in
- (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
- end) (constrs ~~ (1 upto length constrs)));
+ fun def_case ((((i, (_, _, constrs)), T), name), recname) (defs, thy) =
+ let val Tcon = dest_Type_name T in
+ if is_some (Ctr_Sugar.ctr_sugar_of ctxt Tcon) then
+ (defs, thy)
+ else
+ let
+ val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
+ let
+ val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
+ val Ts' = Ts @ map mk_dummyT (filter Old_Datatype_Aux.is_rec_type cargs);
+ val frees' = map2 (Old_Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
+ val frees = take (length cargs) frees';
+ val free = Old_Datatype_Aux.mk_Free "f" (Ts ---> T') j;
+ in
+ (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
+ end) (constrs ~~ (1 upto length constrs)));
- val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
- val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
- val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
- val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
- val def =
- (Binding.name (Thm.def_name (Long_Name.base_name name)),
- Logic.mk_equals (Const (name, caseT),
- fold_rev lambda fns1
- (list_comb (reccomb,
- flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
- val (def_thm, thy') =
- thy
- |> Sign.declare_const_global decl |> snd
- |> Global_Theory.add_def def;
- in (defs @ [def_thm], thy') end;
+ val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
+ val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
+ val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
+ val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
+ val def =
+ (Binding.name (Thm.def_name (Long_Name.base_name name)),
+ Logic.mk_equals (Const (name, caseT),
+ fold_rev lambda fns1
+ (list_comb (reccomb,
+ flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
+ val (def_thm, thy') =
+ thy
+ |> Sign.declare_const_global decl |> snd
+ |> Global_Theory.add_def def;
+ in (defs @ [def_thm], thy') end
+ end;
val (case_defs, thy2) =
fold def_case (hd descr ~~ newTs ~~ case_names0 ~~ take (length newTs) reccomb_names)
@@ -350,8 +350,8 @@
EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms),
resolve_tac ctxt [refl] 1]);
- fun prove_cases (Type (Tcon, _)) ts =
- (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
+ fun prove_cases T ts =
+ (case Ctr_Sugar.ctr_sugar_of ctxt (dest_Type_name T) of
SOME {case_thms, ...} => case_thms
| NONE => map prove_case ts);
@@ -455,8 +455,8 @@
let
fun prove_case_cong ((t, nchotomy), case_rewrites) =
let
- val Const (\<^const_name>\<open>Pure.imp\<close>, _) $ tm $ _ = t;
- val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Ma) = tm;
+ val \<^Const_>\<open>Pure.imp for tm _\<close> = t;
+ val \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for _ Ma\<close>\<close> = tm;
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_var_names (Thm.concl_of nchotomy') [];
in
--- a/src/HOL/Tools/SMT/smtlib_proof.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML Wed Aug 07 20:56:31 2024 +0200
@@ -97,9 +97,7 @@
val needs_inferT = equal Term.dummyT orf Term.is_TVar
val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT)
- fun infer_types ctxt =
- singleton (Type_Infer_Context.infer_types ctxt) #>
- singleton (Proof_Context.standard_term_check_finish ctxt)
+ fun infer_types ctxt = singleton (Type_Infer_Context.infer_types_finished ctxt)
fun infer ctxt t = if needs_infer t then infer_types ctxt t else t
val (t, {ctxt = ctxt', extra = names, ...}: ((string * (string * typ)) list, 'b) context) =
--- a/src/HOL/Tools/datatype_realizer.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Aug 07 20:56:31 2024 +0200
@@ -49,7 +49,7 @@
(fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
- val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
+ val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
val frees = tnames ~~ Ts;
@@ -88,7 +88,7 @@
else if (j: int) = i then HOLogic.mk_fst t
else mk_proj j is (HOLogic.mk_snd t);
- val tnames = Old_Datatype_Prop.make_tnames recTs;
+ val tnames = Case_Translation.make_tnames recTs;
val fTs = map fastype_of rec_fns;
val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
@@ -168,7 +168,7 @@
fun make_casedist_prem T (cname, cargs) =
let
val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
- val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts;
+ val frees = Name.variant_list ["P", "y"] (Case_Translation.make_tnames Ts) ~~ Ts;
val free_ts = map Free frees;
val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
in
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed Aug 07 20:56:31 2024 +0200
@@ -461,21 +461,16 @@
|> Option.map (fn thm => thm RS @{thm eq_reflection})
end;
-fun instantiate_arg_cong ctxt pred =
- let
- val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
- val (Var (f, _) $ _, _) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong))
- in
- infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong
- end;
-
fun proc ctxt redex =
let
- val pred $ set_compr = Thm.term_of redex
- val arg_cong' = instantiate_arg_cong ctxt pred
+ val (f, set_compr) = Thm.dest_comb redex
+ val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm f)
+ val cong =
+ \<^instantiate>\<open>'a = A and 'b = B and f
+ in lemma (schematic) "x = y \<Longrightarrow> f x \<equiv> f y" by simp\<close>
in
- conv ctxt set_compr
- |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection})
+ conv ctxt (Thm.term_of set_compr)
+ |> Option.map (fn thm => thm RS cong)
end;
fun code_proc ctxt redex =
--- a/src/Provers/splitter.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/Provers/splitter.ML Wed Aug 07 20:56:31 2024 +0200
@@ -428,9 +428,12 @@
(* add_split / del_split *)
-fun string_of_typ (Type (s, Ts)) =
- (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
- | string_of_typ _ = "_";
+fun string_of_typ T =
+ if is_Type T then
+ (case dest_Type_args T of
+ [] => ""
+ | Ts => enclose "(" ")" (commas (map string_of_typ Ts))) ^ dest_Type_name T
+ else "_";
fun split_name (name, T) asm = "split " ^
(if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Aug 07 12:39:09 2024 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Aug 07 20:56:31 2024 +0200
@@ -16,7 +16,7 @@
object Isabelle_Cronjob {
/* global resources: owned by main cronjob */
- val backup = "lxbroy10:cronjob"
+ val backup = "isabelle.in.tum.de:cronjob"
val main_dir: Path = Path.explode("~/cronjob")
val main_state_file: Path = main_dir + Path.explode("run/main.state")
val build_release_log: Path = main_dir + Path.explode("run/build_release.log")
--- a/src/Pure/type_infer_context.ML Wed Aug 07 12:39:09 2024 +0100
+++ b/src/Pure/type_infer_context.ML Wed Aug 07 20:56:31 2024 +0200
@@ -11,6 +11,7 @@
val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
val prepare: Proof.context -> term list -> int * term list
val infer_types: Proof.context -> term list -> term list
+ val infer_types_finished: Proof.context -> term list -> term list
end;
structure Type_Infer_Context: TYPE_INFER_CONTEXT =
@@ -304,4 +305,7 @@
val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
in ts' end;
+fun infer_types_finished ctxt =
+ infer_types ctxt #> Proof_Context.standard_term_check_finish ctxt;
+
end;