--- a/src/HOLCF/Bifinite.thy Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Bifinite.thy Tue Mar 02 17:21:10 2010 -0800
@@ -295,7 +295,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-instantiation "->" :: (profinite, profinite) profinite
+instantiation cfun :: (profinite, profinite) profinite
begin
definition
@@ -325,7 +325,7 @@
end
-instance "->" :: (profinite, bifinite) bifinite ..
+instance cfun :: (profinite, bifinite) bifinite ..
lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
by (simp add: approx_cfun_def)
--- a/src/HOLCF/Cfun.thy Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Cfun.thy Tue Mar 02 17:21:10 2010 -0800
@@ -20,11 +20,11 @@
lemma adm_cont: "adm cont"
by (rule admI, rule cont_lub_fun)
-cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
+cpodef (CFun) ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
by (simp_all add: Ex_cont adm_cont)
-syntax (xsymbols)
- "->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)
+type_notation (xsymbols)
+ cfun ("(_ \<rightarrow>/ _)" [1, 0] 0)
notation
Rep_CFun ("(_$/_)" [999,1000] 999)
@@ -103,16 +103,16 @@
lemma UU_CFun: "\<bottom> \<in> CFun"
by (simp add: CFun_def inst_fun_pcpo cont_const)
-instance "->" :: (finite_po, finite_po) finite_po
+instance cfun :: (finite_po, finite_po) finite_po
by (rule typedef_finite_po [OF type_definition_CFun])
-instance "->" :: (finite_po, chfin) chfin
+instance cfun :: (finite_po, chfin) chfin
by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
-instance "->" :: (cpo, discrete_cpo) discrete_cpo
+instance cfun :: (cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
-instance "->" :: (cpo, pcpo) pcpo
+instance cfun :: (cpo, pcpo) pcpo
by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
lemmas Rep_CFun_strict =
--- a/src/HOLCF/Representable.thy Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Representable.thy Tue Mar 02 17:21:10 2010 -0800
@@ -416,7 +416,7 @@
text "Functions between representable types are representable."
-instantiation "->" :: (rep, rep) rep
+instantiation cfun :: (rep, rep) rep
begin
definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
@@ -431,7 +431,7 @@
text "Strict products of representable types are representable."
-instantiation "**" :: (rep, rep) rep
+instantiation sprod :: (rep, rep) rep
begin
definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
@@ -446,7 +446,7 @@
text "Strict sums of representable types are representable."
-instantiation "++" :: (rep, rep) rep
+instantiation ssum :: (rep, rep) rep
begin
definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
@@ -784,13 +784,13 @@
setup {*
fold Domain_Isomorphism.add_type_constructor
- [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
+ [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
@{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
- (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
+ (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
@{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
- (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
+ (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
@{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
(@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
--- a/src/HOLCF/Sprod.thy Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Sprod.thy Tue Mar 02 17:21:10 2010 -0800
@@ -12,20 +12,20 @@
subsection {* Definition of strict product type *}
-pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) =
+pcpodef (Sprod) ('a, 'b) sprod (infixr "**" 20) =
"{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
by simp_all
-instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
by (rule typedef_finite_po [OF type_definition_Sprod])
-instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
syntax (xsymbols)
- "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
+ sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
syntax (HTML output)
- "**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
+ sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
lemma spair_lemma:
"(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
@@ -80,11 +80,11 @@
apply fast
done
-lemma sprodE [cases type: **]:
+lemma sprodE [cases type: sprod]:
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (cut_tac z=p in Exh_Sprod, auto)
-lemma sprod_induct [induct type: **]:
+lemma sprod_induct [induct type: sprod]:
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
by (cases x, simp_all)
@@ -221,7 +221,7 @@
subsection {* Strict product preserves flatness *}
-instance "**" :: (flat, flat) flat
+instance sprod :: (flat, flat) flat
proof
fix x y :: "'a \<otimes> 'b"
assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
@@ -312,7 +312,7 @@
subsection {* Strict product is a bifinite domain *}
-instantiation "**" :: (bifinite, bifinite) bifinite
+instantiation sprod :: (bifinite, bifinite) bifinite
begin
definition
--- a/src/HOLCF/Ssum.thy Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Ssum.thy Tue Mar 02 17:21:10 2010 -0800
@@ -12,22 +12,22 @@
subsection {* Definition of strict sum type *}
-pcpodef (Ssum) ('a, 'b) "++" (infixr "++" 10) =
+pcpodef (Ssum) ('a, 'b) ssum (infixr "++" 10) =
"{p :: tr \<times> ('a \<times> 'b).
(fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
(fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
by simp_all
-instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
by (rule typedef_finite_po [OF type_definition_Ssum])
-instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
syntax (xsymbols)
- "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
+ ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
syntax (HTML output)
- "++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
+ ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
subsection {* Definitions of constructors *}
@@ -150,13 +150,13 @@
apply (simp add: sinr_Abs_Ssum Ssum_def)
done
-lemma ssumE [cases type: ++]:
+lemma ssumE [cases type: ssum]:
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
\<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
\<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (cut_tac z=p in Exh_Ssum, auto)
-lemma ssum_induct [induct type: ++]:
+lemma ssum_induct [induct type: ssum]:
"\<lbrakk>P \<bottom>;
\<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
\<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
@@ -203,7 +203,7 @@
subsection {* Strict sum preserves flatness *}
-instance "++" :: (flat, flat) flat
+instance ssum :: (flat, flat) flat
apply (intro_classes, clarify)
apply (case_tac x, simp)
apply (case_tac y, simp_all add: flat_below_iff)
@@ -296,7 +296,7 @@
subsection {* Strict sum is a bifinite domain *}
-instantiation "++" :: (bifinite, bifinite) bifinite
+instantiation ssum :: (bifinite, bifinite) bifinite
begin
definition
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 17:21:10 2010 -0800
@@ -31,9 +31,9 @@
(* FIXME: use theory data for this *)
val copy_tab : string Symtab.table =
- Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
- (@{type_name "++"}, @{const_name "ssum_map"}),
- (@{type_name "**"}, @{const_name "sprod_map"}),
+ Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}),
+ (@{type_name ssum}, @{const_name "ssum_map"}),
+ (@{type_name sprod}, @{const_name "sprod_map"}),
(@{type_name "*"}, @{const_name "cprod_map"}),
(@{type_name "u"}, @{const_name "u_map"})];
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 17:21:10 2010 -0800
@@ -79,7 +79,9 @@
| rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
| rm_sorts (TVar(s,_)) = TVar(s,[])
and remove_sorts l = map rm_sorts l;
- val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+ val indirect_ok =
+ [@{type_name "*"}, @{type_name cfun}, @{type_name ssum},
+ @{type_name sprod}, @{type_name u}];
fun analyse indirect (TFree(v,s)) =
(case AList.lookup (op =) tvars v of
NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
--- a/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Tue Mar 02 17:21:10 2010 -0800
@@ -213,8 +213,8 @@
(* ----- combinators for making dtyps ----- *)
fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
-fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name "**"}, [T, U]);
-fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name "++"}, [T, U]);
+fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name sprod}, [T, U]);
+fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name ssum}, [T, U]);
fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []);
@@ -231,9 +231,9 @@
(* ----- support for type and mixfix expressions ----- *)
fun mk_uT T = Type(@{type_name "u"}, [T]);
-fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
-fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
val oneT = @{typ one};
val op ->> = mk_cfunT;
--- a/src/HOLCF/Tools/cont_consts.ML Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Tools/cont_consts.ML Tue Mar 02 17:21:10 2010 -0800
@@ -56,7 +56,7 @@
trans_rules (syntax c2) (syntax c1) n mx)
end;
-fun cfun_arity (Type (n, [_, T])) = if n = @{type_name "->"} then 1 + cfun_arity T else 0
+fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0
| cfun_arity _ = 0;
fun is_contconst (_, _, NoSyn) = false
--- a/src/HOLCF/Tools/fixrec.ML Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Tools/fixrec.ML Tue Mar 02 17:21:10 2010 -0800
@@ -35,11 +35,11 @@
(*************************************************************************)
(* ->> is taken from holcf_logic.ML *)
-fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
infixr 6 ->>; val (op ->>) = cfunT;
-fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
fun maybeT T = Type(@{type_name "maybe"}, [T]);
@@ -53,11 +53,11 @@
local
-fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
+fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U
| binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
| binder_cfun _ = [];
-fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
+fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
| body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
| body_cfun T = T;
@@ -99,7 +99,7 @@
fun mk_capply (t, u) =
let val (S, T) =
case Term.fastype_of t of
- Type(@{type_name "->"}, [S, T]) => (S, T)
+ Type(@{type_name cfun}, [S, T]) => (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;
@@ -288,7 +288,7 @@
| Const(c,T) =>
let
val n = Name.variant taken "v";
- fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
+ fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
| result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
| result_type T _ = T;
val v = Free(n, result_type T vs);
--- a/src/HOLCF/Tools/holcf_library.ML Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Tools/holcf_library.ML Tue Mar 02 17:21:10 2010 -0800
@@ -51,12 +51,12 @@
(*** Continuous function space ***)
(* ->> is taken from holcf_logic.ML *)
-fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
val (op ->>) = mk_cfunT;
val (op -->>) = Library.foldr mk_cfunT;
-fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
fun capply_const (S, T) =
@@ -84,7 +84,7 @@
fun mk_capply (t, u) =
let val (S, T) =
case fastype_of t of
- Type(@{type_name "->"}, [S, T]) => (S, T)
+ Type(@{type_name cfun}, [S, T]) => (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;
@@ -153,9 +153,9 @@
val oneT = @{typ "one"};
-fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
-fun dest_sprodT (Type(@{type_name "**"}, [T, U])) = (T, U)
+fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U)
| dest_sprodT T = raise TYPE ("dest_sprodT", [T], []);
fun spair_const (T, U) =
@@ -179,9 +179,9 @@
(*** Strict sum type ***)
-fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
-fun dest_ssumT (Type(@{type_name "++"}, [T, U])) = (T, U)
+fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U)
| dest_ssumT T = raise TYPE ("dest_ssumT", [T], []);
fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U));
--- a/src/HOLCF/Tools/repdef.ML Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Tools/repdef.ML Tue Mar 02 17:21:10 2010 -0800
@@ -35,7 +35,7 @@
val natT = @{typ nat};
val udomT = @{typ udom};
fun alg_deflT T = Type (@{type_name alg_defl}, [T]);
-fun cfunT (T, U) = Type (@{type_name "->"}, [T, U]);
+fun cfunT (T, U) = Type (@{type_name cfun}, [T, U]);
fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT));
fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T));
fun approx_const T = Const (@{const_name approx}, natT --> cfunT (T, T));