--- a/src/HOL/HOLCF/Pcpo.thy Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy Sun Sep 12 22:31:51 2021 +0200
@@ -156,7 +156,7 @@
translations "UU" \<rightharpoonup> "CONST bottom"
text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
-setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close>
+setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close>
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Sun Sep 12 22:31:51 2021 +0200
@@ -75,7 +75,7 @@
(thy : theory)
: thm * theory =
let
- val i = Free ("i", natT)
+ val i = Free ("i", \<^Type>\<open>nat\<close>)
val T = (fst o dest_cfunT o range_type o fastype_of) take_const
val lub_take_eqn =
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sun Sep 12 22:31:51 2021 +0200
@@ -42,13 +42,13 @@
val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy
val n = Free ("n", \<^typ>\<open>nat\<close>)
- val n' = \<^const>\<open>Suc\<close> $ n
+ val n' = \<^Const>\<open>Suc for n\<close>
local
val newTs = map (#absT o #iso_info) constr_infos
val subs = newTs ~~ map (fn t => t $ n) take_consts
- fun is_ID (Const (c, _)) = (c = \<^const_name>\<open>ID\<close>)
- | is_ID _ = false
+ fun is_ID \<^Const_>\<open>ID _\<close> = true
+ | is_ID _ = false
in
fun map_of_arg thy v T =
let val m = Domain_Take_Proofs.map_of_typ thy subs T
@@ -110,10 +110,10 @@
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_types = map (fn T => T --> HOLogic.boolT) 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)
- val n = Free ("n", HOLogic.natT)
+ val n = Free ("n", \<^Type>\<open>nat\<close>)
fun con_assm defined p (con, args) =
let
@@ -257,14 +257,14 @@
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_types = map (fn T => T --> T --> boolT) 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", natT)
+ val n = Free ("n", \<^Type>\<open>nat\<close>)
val reserved = "x" :: "y" :: R_names
(* declare bisimulation predicate *)
val bisim_bind = Binding.suffix_name "_bisim" comp_dbind
- val bisim_type = R_types ---> boolT
+ val bisim_type = R_types ---> \<^Type>\<open>bool\<close>
val (bisim_const, thy) =
Sign.declare_const_global ((bisim_bind, bisim_type), NoSyn) thy
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Sep 12 22:31:51 2021 +0200
@@ -53,32 +53,29 @@
val deflT = \<^typ>\<open>udom defl\<close>
val udeflT = \<^typ>\<open>udom u defl\<close>
-fun mk_DEFL T =
- Const (\<^const_name>\<open>defl\<close>, Term.itselfT T --> deflT) $ Logic.mk_type T
+fun mk_DEFL T = \<^Const>\<open>defl T for \<open>Logic.mk_type T\<close>\<close>
-fun dest_DEFL (Const (\<^const_name>\<open>defl\<close>, _) $ t) = Logic.dest_type t
+fun dest_DEFL \<^Const_>\<open>defl _ for t\<close> = Logic.dest_type t
| dest_DEFL t = raise TERM ("dest_DEFL", [t])
-fun mk_LIFTDEFL T =
- Const (\<^const_name>\<open>liftdefl\<close>, Term.itselfT T --> udeflT) $ Logic.mk_type T
+fun mk_LIFTDEFL T = \<^Const>\<open>liftdefl T for \<open>Logic.mk_type T\<close>\<close>
-fun dest_LIFTDEFL (Const (\<^const_name>\<open>liftdefl\<close>, _) $ t) = Logic.dest_type t
+fun dest_LIFTDEFL \<^Const_>\<open>liftdefl _ for t\<close> = Logic.dest_type t
| dest_LIFTDEFL t = raise TERM ("dest_LIFTDEFL", [t])
-fun mk_u_defl t = mk_capply (\<^const>\<open>u_defl\<close>, t)
+fun mk_u_defl t = mk_capply (\<^Const>\<open>u_defl\<close>, t)
-fun emb_const T = Const (\<^const_name>\<open>emb\<close>, T ->> udomT)
-fun prj_const T = Const (\<^const_name>\<open>prj\<close>, udomT ->> T)
+fun emb_const T = \<^Const>\<open>emb T\<close>
+fun prj_const T = \<^Const>\<open>prj T\<close>
fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)
-fun isodefl_const T =
- Const (\<^const_name>\<open>isodefl\<close>, (T ->> T) --> deflT --> HOLogic.boolT)
+fun isodefl_const T = \<^Const>\<open>isodefl T\<close>
-fun isodefl'_const T =
- Const (\<^const_name>\<open>isodefl'\<close>, (T ->> T) --> udeflT --> HOLogic.boolT)
+fun isodefl'_const T = \<^Const>\<open>isodefl' T\<close>
fun mk_deflation t =
- Const (\<^const_name>\<open>deflation\<close>, Term.fastype_of t --> boolT) $ t
+ let val T = #1 (dest_cfunT (Term.fastype_of t))
+ in \<^Const>\<open>deflation T for t\<close> end
(* splits a cterm into the right and lefthand sides of equality *)
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
@@ -121,10 +118,10 @@
(* convert parameters to lambda abstractions *)
fun mk_eqn (lhs, rhs) =
case lhs of
- Const (\<^const_name>\<open>Rep_cfun\<close>, _) $ f $ (x as Free _) =>
+ \<^Const_>\<open>Rep_cfun _ _ for f \<open>x as Free _\<close>\<close> =>
mk_eqn (f, big_lambda x rhs)
- | f $ Const (\<^const_name>\<open>Pure.type\<close>, T) =>
- mk_eqn (f, Abs ("t", T, rhs))
+ | f $ \<^Const_>\<open>Pure.type T\<close> =>
+ mk_eqn (f, Abs ("t", \<^Type>\<open>itself T\<close>, rhs))
| Const _ => Logic.mk_equals (lhs, rhs)
| _ => raise TERM ("lhs not of correct form", [lhs, rhs])
val eqns = map mk_eqn projs
@@ -710,7 +707,7 @@
(* prove lub of take equals ID *)
fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =
let
- val n = Free ("n", natT)
+ val n = Free ("n", \<^Type>\<open>nat\<close>)
val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
fun tac ctxt =
EVERY
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun Sep 12 22:31:51 2021 +0200
@@ -149,7 +149,8 @@
infix 9 `
fun mk_deflation t =
- Const (\<^const_name>\<open>deflation\<close>, Term.fastype_of t --> boolT) $ t
+ let val T = #1 (dest_cfunT (Term.fastype_of t))
+ in \<^Const>\<open>deflation T for t\<close> end
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
@@ -235,7 +236,7 @@
(mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)))
val take_rhss =
let
- val n = Free ("n", HOLogic.natT)
+ val n = Free ("n", \<^Type>\<open>nat\<close>)
val rhs = mk_iterate (n, take_functional)
in
map (lambda n o snd) (mk_projs dbinds rhs)
@@ -244,7 +245,7 @@
(* define take constants *)
fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy =
let
- val take_type = HOLogic.natT --> lhsT ->> lhsT
+ val take_type = \<^Type>\<open>nat\<close> --> lhsT ->> lhsT
val take_bind = Binding.suffix_name "_take" dbind
val (take_const, thy) =
Sign.declare_const_global ((take_bind, take_type), NoSyn) thy
@@ -284,7 +285,7 @@
fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy
(* prove take_Suc lemmas *)
- val n = Free ("n", natT)
+ val n = Free ("n", \<^Type>\<open>nat\<close>)
val take_is = map (fn t => t $ n) take_consts
fun prove_take_Suc
(((take_const, rep_abs), dbind), (_, rhsT)) thy =
@@ -308,7 +309,7 @@
val deflation_abs_rep_thms = map deflation_abs_rep iso_infos
val deflation_take_thm =
let
- val n = Free ("n", natT)
+ val n = Free ("n", \<^Type>\<open>nat\<close>)
fun mk_goal take_const = mk_deflation (take_const $ n)
val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts))
val bottom_rules =
@@ -380,14 +381,14 @@
(* define finiteness predicates *)
fun define_finite_const ((dbind, take_const), (lhsT, _)) thy =
let
- val finite_type = lhsT --> boolT
+ val finite_type = lhsT --> \<^Type>\<open>bool\<close>
val finite_bind = Binding.suffix_name "_finite" dbind
val (finite_const, thy) =
Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy
val x = Free ("x", lhsT)
- val n = Free ("n", natT)
+ val n = Free ("n", \<^Type>\<open>nat\<close>)
val finite_rhs =
- lambda x (HOLogic.exists_const natT $
+ lambda x (HOLogic.exists_const \<^Type>\<open>nat\<close> $
(lambda n (mk_eq (mk_capply (take_const $ n, x), x))))
val finite_eqn = Logic.mk_equals (finite_const, finite_rhs)
val (finite_def_thm, thy) =
@@ -436,7 +437,8 @@
map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms
val n = Free ("n", \<^typ>\<open>nat\<close>)
fun mk_decisive t =
- Const (\<^const_name>\<open>decisive\<close>, fastype_of t --> boolT) $ t
+ let val T = #1 (dest_cfunT (fastype_of t))
+ in \<^Const>\<open>decisive T for t\<close> end
fun f take_const = mk_decisive (take_const $ n)
val goal = mk_trp (foldr1 mk_conj (map f take_consts))
val rules0 = @{thm decisive_bottom} :: take_0_thms
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Sun Sep 12 22:31:51 2021 +0200
@@ -18,7 +18,7 @@
(* misc utils *)
fun change_arrow 0 T = T
- | change_arrow n (Type (_, [S, T])) = Type ("fun", [S, change_arrow (n - 1) T])
+ | change_arrow n (Type (_, [S, T])) = \<^Type>\<open>fun S \<open>change_arrow (n - 1) T\<close>\<close>
| change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], [])
fun trans_rules name2 name1 n mx =
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Sun Sep 12 22:31:51 2021 +0200
@@ -24,12 +24,9 @@
val cont_R = @{thm cont_Rep_cfun2}
(* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const (\<^const_name>\<open>Rep_cfun\<close>, _) $ t $ u) =
- is_lcf_term t andalso is_lcf_term u
- | is_lcf_term (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ Abs (_, _, t)) =
- is_lcf_term t
- | is_lcf_term (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ t) =
- is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
+fun is_lcf_term \<^Const_>\<open>Rep_cfun _ _ for t u\<close> = is_lcf_term t andalso is_lcf_term u
+ | is_lcf_term \<^Const_>\<open>Abs_cfun _ _ for \<open>Abs (_, _, t)\<close>\<close> = is_lcf_term t
+ | is_lcf_term \<^Const_>\<open>Abs_cfun _ _ for t\<close> = is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
| is_lcf_term (Bound _) = true
| is_lcf_term t = not (Term.is_open t)
@@ -64,17 +61,17 @@
(* first list: cont thm for each dangling bound variable *)
(* second list: cont thm for each LAM in t *)
(* if b = false, only return cont thm for outermost LAMs *)
- fun cont_thms1 b (Const (\<^const_name>\<open>Rep_cfun\<close>, _) $ f $ t) =
+ fun cont_thms1 b \<^Const_>\<open>Rep_cfun _ _ for f t\<close> =
let
val (cs1,ls1) = cont_thms1 b f
val (cs2,ls2) = cont_thms1 b t
in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
- | cont_thms1 b (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ Abs (_, _, t)) =
+ | cont_thms1 b \<^Const_>\<open>Abs_cfun _ _ for \<open>Abs (_, _, t)\<close>\<close> =
let
val (cs, ls) = cont_thms1 b t
val (cs', l) = lam cs
in (cs', l::ls) end
- | cont_thms1 b (Const (\<^const_name>\<open>Abs_cfun\<close>, _) $ t) =
+ | cont_thms1 b \<^Const_>\<open>Abs_cfun _ _ for t\<close> =
let
val t' = Term.incr_boundvars 1 t $ Bound 0
val (cs, ls) = cont_thms1 b t'
@@ -104,9 +101,9 @@
[] => no_tac
| (c::_) => resolve_tac ctxt [c] i
- fun cont_tac_of_term (Const (\<^const_name>\<open>cont\<close>, _) $ f) =
+ fun cont_tac_of_term \<^Const_>\<open>cont _ _ for f\<close> =
let
- val f' = Const (\<^const_name>\<open>Abs_cfun\<close>, dummyT) $ f
+ val f' = \<^Const>\<open>Abs_cfun dummyT dummyT for f\<close>
in
if is_lcf_term f'
then new_cont_tac f'
--- a/src/HOL/HOLCF/Tools/cpodef.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sun Sep 12 22:31:51 2021 +0200
@@ -53,10 +53,10 @@
(* building terms *)
-fun adm_const T = Const (\<^const_name>\<open>adm\<close>, (T --> HOLogic.boolT) --> HOLogic.boolT)
+fun adm_const T = \<^Const>\<open>adm T\<close>
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P
-fun below_const T = Const (\<^const_name>\<open>below\<close>, T --> T --> HOLogic.boolT)
+fun below_const T = \<^Const>\<open>below T\<close>
(* proving class instances *)
@@ -229,7 +229,7 @@
val (newT, oldT, set) = prepare prep_term name typ raw_set thy
val goal_bottom_mem =
- HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (\<^const_name>\<open>bottom\<close>, oldT), set))
+ HOLogic.mk_Trueprop (HOLogic.mk_mem (\<^Const>\<open>bottom oldT\<close>, set))
val goal_admissible =
HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)))
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun Sep 12 22:31:51 2021 +0200
@@ -50,19 +50,17 @@
val udomT = \<^typ>\<open>udom\<close>
val deflT = \<^typ>\<open>udom defl\<close>
-val udeflT = \<^typ>\<open>udom u defl\<close>
-fun emb_const T = Const (\<^const_name>\<open>emb\<close>, T ->> udomT)
-fun prj_const T = Const (\<^const_name>\<open>prj\<close>, udomT ->> T)
-fun defl_const T = Const (\<^const_name>\<open>defl\<close>, Term.itselfT T --> deflT)
-fun liftemb_const T = Const (\<^const_name>\<open>liftemb\<close>, mk_upT T ->> mk_upT udomT)
-fun liftprj_const T = Const (\<^const_name>\<open>liftprj\<close>, mk_upT udomT ->> mk_upT T)
-fun liftdefl_const T = Const (\<^const_name>\<open>liftdefl\<close>, Term.itselfT T --> udeflT)
+fun emb_const T = \<^Const>\<open>emb T\<close>
+fun prj_const T = \<^Const>\<open>prj T\<close>
+fun defl_const T = \<^Const>\<open>defl T\<close>
+fun liftemb_const T = \<^Const>\<open>liftemb T\<close>
+fun liftprj_const T = \<^Const>\<open>liftprj T\<close>
+fun liftdefl_const T = \<^Const>\<open>liftdefl T\<close>
fun mk_u_map t =
let
val (T, U) = dest_cfunT (fastype_of t)
- val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U)
- val u_map_const = Const (\<^const_name>\<open>u_map\<close>, u_map_type)
+ val u_map_const = \<^Const>\<open>u_map T U\<close>
in
mk_capply (u_map_const, t)
end
@@ -124,7 +122,7 @@
val liftdefl_eqn =
Logic.mk_equals (liftdefl_const newT,
Abs ("t", Term.itselfT newT,
- mk_capply (\<^const>\<open>liftdefl_of\<close>, defl_const newT $ Logic.mk_type newT)))
+ mk_capply (\<^Const>\<open>liftdefl_of\<close>, defl_const newT $ Logic.mk_type newT)))
val name_def = Thm.def_binding tname
val emb_bind = (Binding.prefix_name "emb_" name_def, [])
--- a/src/HOL/HOLCF/Tools/fixrec.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Sun Sep 12 22:31:51 2021 +0200
@@ -34,12 +34,12 @@
local
-fun binder_cfun (Type(\<^type_name>\<open>cfun\<close>,[T, U])) = T :: binder_cfun U
- | binder_cfun (Type(\<^type_name>\<open>fun\<close>,[T, U])) = T :: binder_cfun U
+fun binder_cfun \<^Type>\<open>cfun T U\<close> = T :: binder_cfun U
+ | binder_cfun \<^Type>\<open>fun T U\<close> = T :: binder_cfun U
| binder_cfun _ = []
-fun body_cfun (Type(\<^type_name>\<open>cfun\<close>,[_, U])) = body_cfun U
- | body_cfun (Type(\<^type_name>\<open>fun\<close>,[_, U])) = body_cfun U
+fun body_cfun \<^Type>\<open>cfun _ U\<close> = body_cfun U
+ | body_cfun \<^Type>\<open>fun _ U\<close> = body_cfun U
| body_cfun T = T
in
@@ -59,24 +59,23 @@
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
(* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(\<^const_name>\<open>Rep_cfun\<close>,_)$f$_) = chead_of f
+fun chead_of \<^Const_>\<open>Rep_cfun _ _ for f _\<close> = chead_of f
| chead_of u = u
infix 1 === val (op ===) = HOLogic.mk_eq
fun mk_mplus (t, u) =
- let val mT = Term.fastype_of t
- in Const(\<^const_name>\<open>Fixrec.mplus\<close>, mT ->> mT ->> mT) ` t ` u end
+ let val T = dest_matchT (Term.fastype_of t)
+ in \<^Const>\<open>Fixrec.mplus T\<close> ` t ` u end
fun mk_run t =
let
val mT = Term.fastype_of t
val T = dest_matchT mT
- val run = Const(\<^const_name>\<open>Fixrec.run\<close>, mT ->> T)
+ val run = \<^Const>\<open>Fixrec.run T\<close>
in
case t of
- Const(\<^const_name>\<open>Rep_cfun\<close>, _) $
- Const(\<^const_name>\<open>Fixrec.succeed\<close>, _) $ u => u
+ \<^Const_>\<open>Rep_cfun _ _\<close> $ \<^Const_>\<open>Fixrec.succeed _\<close> $ u => u
| _ => run ` t
end
@@ -150,7 +149,7 @@
|> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs)
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]
val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms)
- val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT)
+ val P = Var (("P", 0), map Term.fastype_of lhss ---> \<^Type>\<open>bool\<close>)
val predicate = lambda_tuple lhss (list_comb (P, lhss))
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
|> Thm.instantiate' [] [SOME (Thm.global_cterm_of thy predicate)]
@@ -219,7 +218,7 @@
(* compiles a monadic term for a constructor pattern *)
and comp_con T p rhs vs taken =
case p of
- Const(\<^const_name>\<open>Rep_cfun\<close>,_) $ f $ x =>
+ \<^Const_>\<open>Rep_cfun _ _ for f x\<close> =>
let val (rhs', v, taken') = comp_pat x rhs taken
in comp_con T f rhs' (v::vs) taken' end
| f $ x =>
@@ -243,7 +242,7 @@
(* returns (constant, (vars, matcher)) *)
fun compile_lhs match_name pat rhs vs taken =
case pat of
- Const(\<^const_name>\<open>Rep_cfun\<close>, _) $ f $ x =>
+ \<^Const_>\<open>Rep_cfun _ _ for f x\<close> =>
let val (rhs', v, taken') = compile_pat match_name x rhs taken
in compile_lhs match_name f rhs' (v::vs) taken' end
| Free(_,_) => (pat, (vs, rhs))
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML Sun Sep 12 22:31:51 2021 +0200
@@ -13,10 +13,6 @@
(*** Operations from Isabelle/HOL ***)
-val boolT = HOLogic.boolT
-val natT = HOLogic.natT
-val mk_setT = HOLogic.mk_setT
-
val mk_equals = Logic.mk_equals
val mk_eq = HOLogic.mk_eq
val mk_trp = HOLogic.mk_Trueprop
@@ -33,9 +29,9 @@
(*** Basic HOLCF concepts ***)
-fun mk_bottom T = Const (\<^const_name>\<open>bottom\<close>, T)
+fun mk_bottom T = \<^Const>\<open>bottom T\<close>
-fun below_const T = Const (\<^const_name>\<open>below\<close>, [T, T] ---> boolT)
+fun below_const T = \<^Const>\<open>below T\<close>
fun mk_below (t, u) = below_const (fastype_of t) $ t $ u
fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t))
@@ -43,44 +39,40 @@
fun mk_defined t = mk_not (mk_undef t)
fun mk_adm t =
- Const (\<^const_name>\<open>adm\<close>, fastype_of t --> boolT) $ t
+ let val T = Term.domain_type (fastype_of t)
+ in \<^Const>\<open>adm T for t\<close> end
fun mk_compact t =
- Const (\<^const_name>\<open>compact\<close>, fastype_of t --> boolT) $ t
+ let val T = fastype_of t
+ in \<^Const>\<open>compact T for t\<close> end
fun mk_cont t =
- Const (\<^const_name>\<open>cont\<close>, fastype_of t --> boolT) $ t
+ let val \<^Type>\<open>fun A B\<close> = fastype_of t
+ in \<^Const>\<open>cont A B for t\<close> end
fun mk_chain t =
- Const (\<^const_name>\<open>chain\<close>, Term.fastype_of t --> boolT) $ t
+ let val T = Term.range_type (Term.fastype_of t)
+ in \<^Const>\<open>chain T for t\<close> end
fun mk_lub t =
let
val T = Term.range_type (Term.fastype_of t)
- val lub_const = Const (\<^const_name>\<open>lub\<close>, mk_setT T --> T)
val UNIV_const = \<^term>\<open>UNIV :: nat set\<close>
- val image_type = (natT --> T) --> mk_setT natT --> mk_setT T
- val image_const = Const (\<^const_name>\<open>image\<close>, image_type)
- in
- lub_const $ (image_const $ t $ UNIV_const)
- end
+ in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end
(*** Continuous function space ***)
-fun mk_cfunT (T, U) = Type(\<^type_name>\<open>cfun\<close>, [T, U])
+fun mk_cfunT (T, U) = \<^Type>\<open>cfun T U\<close>
val (op ->>) = mk_cfunT
val (op -->>) = Library.foldr mk_cfunT
-fun dest_cfunT (Type(\<^type_name>\<open>cfun\<close>, [T, U])) = (T, U)
+fun dest_cfunT \<^Type>\<open>cfun T U\<close> = (T, U)
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], [])
-fun capply_const (S, T) =
- Const(\<^const_name>\<open>Rep_cfun\<close>, (S ->> T) --> (S --> T))
-
-fun cabs_const (S, T) =
- Const(\<^const_name>\<open>Abs_cfun\<close>, (S --> T) --> (S ->> T))
+fun capply_const (S, T) = \<^Const>\<open>Rep_cfun S T\<close>
+fun cabs_const (S, T) = \<^Const>\<open>Abs_cfun S T\<close>
fun mk_cabs t =
let val T = fastype_of t
@@ -101,7 +93,7 @@
fun mk_capply (t, u) =
let val (S, T) =
case fastype_of t of
- Type(\<^type_name>\<open>cfun\<close>, [S, T]) => (S, T)
+ \<^Type>\<open>cfun S T\<close> => (S, T)
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u])
in capply_const (S, T) $ t $ u end
@@ -109,10 +101,7 @@
val list_ccomb : term * term list -> term = Library.foldl mk_capply
-fun mk_ID T = Const (\<^const_name>\<open>ID\<close>, T ->> T)
-
-fun cfcomp_const (T, U, V) =
- Const (\<^const_name>\<open>cfcomp\<close>, (U ->> V) ->> (T ->> U) ->> (T ->> V))
+fun mk_ID T = \<^Const>\<open>ID T\<close>
fun mk_cfcomp (f, g) =
let
@@ -120,12 +109,13 @@
val (T, U') = dest_cfunT (fastype_of g)
in
if U = U'
- then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
+ then mk_capply (mk_capply (\<^Const>\<open>cfcomp U V T\<close>, f), g)
else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
end
-fun strictify_const T = Const (\<^const_name>\<open>strictify\<close>, T ->> T)
-fun mk_strictify t = strictify_const (fastype_of t) ` t
+fun mk_strictify t =
+ let val (T, U) = dest_cfunT (fastype_of t)
+ in \<^Const>\<open>strictify T U\<close> ` t end;
fun mk_strict t =
let val (T, U) = dest_cfunT (fastype_of t)
@@ -154,17 +144,16 @@
(*** Lifted cpo type ***)
-fun mk_upT T = Type(\<^type_name>\<open>u\<close>, [T])
+fun mk_upT T = \<^Type>\<open>u T\<close>
-fun dest_upT (Type(\<^type_name>\<open>u\<close>, [T])) = T
+fun dest_upT \<^Type>\<open>u T\<close> = T
| dest_upT T = raise TYPE ("dest_upT", [T], [])
-fun up_const T = Const(\<^const_name>\<open>up\<close>, T ->> mk_upT T)
+fun up_const T = \<^Const>\<open>up T\<close>
fun mk_up t = up_const (fastype_of t) ` t
-fun fup_const (T, U) =
- Const(\<^const_name>\<open>fup\<close>, (T ->> U) ->> mk_upT T ->> U)
+fun fup_const (T, U) = \<^Const>\<open>fup T U\<close>
fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t
@@ -175,19 +164,18 @@
val oneT = \<^typ>\<open>one\<close>
-fun one_case_const T = Const (\<^const_name>\<open>one_case\<close>, T ->> oneT ->> T)
+fun one_case_const T = \<^Const>\<open>one_case T\<close>
fun mk_one_case t = one_case_const (fastype_of t) ` t
(*** Strict product type ***)
-fun mk_sprodT (T, U) = Type(\<^type_name>\<open>sprod\<close>, [T, U])
+fun mk_sprodT (T, U) = \<^Type>\<open>sprod T U\<close>
-fun dest_sprodT (Type(\<^type_name>\<open>sprod\<close>, [T, U])) = (T, U)
+fun dest_sprodT \<^Type>\<open>sprod T U\<close> = (T, U)
| dest_sprodT T = raise TYPE ("dest_sprodT", [T], [])
-fun spair_const (T, U) =
- Const(\<^const_name>\<open>spair\<close>, T ->> U ->> mk_sprodT (T, U))
+fun spair_const (T, U) = \<^Const>\<open>spair T U\<close>
(* builds the expression (:t, u:) *)
fun mk_spair (t, u) =
@@ -198,14 +186,11 @@
| mk_stuple (t::[]) = t
| mk_stuple (t::ts) = mk_spair (t, mk_stuple ts)
-fun sfst_const (T, U) =
- Const(\<^const_name>\<open>sfst\<close>, mk_sprodT (T, U) ->> T)
+fun sfst_const (T, U) = \<^Const>\<open>sfst T U\<close>
-fun ssnd_const (T, U) =
- Const(\<^const_name>\<open>ssnd\<close>, mk_sprodT (T, U) ->> U)
+fun ssnd_const (T, U) = \<^Const>\<open>ssnd T U\<close>
-fun ssplit_const (T, U, V) =
- Const (\<^const_name>\<open>ssplit\<close>, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V)
+fun ssplit_const (T, U, V) = \<^Const>\<open>ssplit T U V\<close>
fun mk_ssplit t =
let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t))
@@ -214,13 +199,13 @@
(*** Strict sum type ***)
-fun mk_ssumT (T, U) = Type(\<^type_name>\<open>ssum\<close>, [T, U])
+fun mk_ssumT (T, U) = \<^Type>\<open>ssum T U\<close>
-fun dest_ssumT (Type(\<^type_name>\<open>ssum\<close>, [T, U])) = (T, U)
+fun dest_ssumT \<^Type>\<open>ssum T U\<close> = (T, U)
| dest_ssumT T = raise TYPE ("dest_ssumT", [T], [])
-fun sinl_const (T, U) = Const(\<^const_name>\<open>sinl\<close>, T ->> mk_ssumT (T, U))
-fun sinr_const (T, U) = Const(\<^const_name>\<open>sinr\<close>, U ->> mk_ssumT (T, U))
+fun sinl_const (T, U) = \<^Const>\<open>sinl T U\<close>
+fun sinr_const (T, U) = \<^Const>\<open>sinr U T\<close>
(* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *)
fun mk_sinjects ts =
@@ -240,9 +225,7 @@
fst (inj (ts ~~ Ts))
end
-fun sscase_const (T, U, V) =
- Const(\<^const_name>\<open>sscase\<close>,
- (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V)
+fun sscase_const (T, U, V) = \<^Const>\<open>sscase T V U\<close>
fun mk_sscase (t, u) =
let val (T, _) = dest_cfunT (fastype_of t)
@@ -258,14 +241,14 @@
(*** pattern match monad type ***)
-fun mk_matchT T = Type (\<^type_name>\<open>match\<close>, [T])
+fun mk_matchT T = \<^Type>\<open>match T\<close>
-fun dest_matchT (Type(\<^type_name>\<open>match\<close>, [T])) = T
+fun dest_matchT \<^Type>\<open>match T\<close> = T
| dest_matchT T = raise TYPE ("dest_matchT", [T], [])
-fun mk_fail T = Const (\<^const_name>\<open>Fixrec.fail\<close>, mk_matchT T)
+fun mk_fail T = \<^Const>\<open>Fixrec.fail T\<close>
-fun succeed_const T = Const (\<^const_name>\<open>Fixrec.succeed\<close>, T ->> mk_matchT T)
+fun succeed_const T = \<^Const>\<open>Fixrec.succeed T\<close>
fun mk_succeed t = succeed_const (fastype_of t) ` t
@@ -278,10 +261,9 @@
fun mk_fix t =
let val (T, _) = dest_cfunT (fastype_of t)
- in mk_capply (Const(\<^const_name>\<open>fix\<close>, (T ->> T) ->> T), t) end
+ in mk_capply (\<^Const>\<open>fix T\<close>, t) end
-fun iterate_const T =
- Const (\<^const_name>\<open>iterate\<close>, natT --> (T ->> T) ->> (T ->> T))
+fun iterate_const T = \<^Const>\<open>iterate T\<close>
fun mk_iterate (n, f) =
let val (T, _) = dest_cfunT (Term.fastype_of f)
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Sep 12 22:31:51 2021 +0200
@@ -457,11 +457,8 @@
in
pat_const $ p1 $ p2
end;
- fun mk_tuple_pat [] = succeed_const HOLogic.unitT
+ fun mk_tuple_pat [] = succeed_const \<^Type>\<open>unit\<close>
| mk_tuple_pat ps = foldr1 mk_pair_pat ps;
- fun branch_const (T,U,V) =
- Const (\<^const_name>\<open>branch\<close>,
- (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V);
(* define pattern combinators *)
local
@@ -546,9 +543,9 @@
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);
- val branch1 = branch_const (lhsT, mk_tupleT Vs, R);
+ val branch1 = \<^Const>\<open>branch lhsT \<open>mk_tupleT Vs\<close> R\<close>;
val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
- val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R);
+ val branch2 = \<^Const>\<open>branch \<open>mk_tupleT Ts\<close> \<open>mk_tupleT Vs\<close> R\<close>;
val fun2 = (branch2 $ mk_tuple_pat pats) ` k;
val taken = "rhs" :: patNs;
in (fun1, fun2, taken) end;