# HG changeset patch # User huffman # Date 1267579270 28800 # Node ID fa231b86cb1e7ef78ad31fc67cddf1f3059cfe87 # Parent a2a59e92b02eed4a5506226a0f53f88c9b2353d4 proper names for types cfun, sprod, ssum diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Bifinite.thy --- 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\f\x = approx n\(f\(approx n\x))" by (simp add: approx_cfun_def) diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Cfun.thy --- 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" ("(_ \/ _)" [1,0]0) +type_notation (xsymbols) + cfun ("(_ \/ _)" [1, 0] 0) notation Rep_CFun ("(_$/_)" [999,1000] 999) @@ -103,16 +103,16 @@ lemma UU_CFun: "\ \ 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 = diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Representable.thy --- 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\prj\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\emb\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\emb\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}, diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Sprod.thy --- 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 \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" 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" ("(_ \/ _)" [21,20] 20) + sprod :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) syntax (HTML output) - "**" :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) + sprod :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) lemma spair_lemma: "(strictify\(\ b. a)\b, strictify\(\ a. b)\a) \ Sprod" @@ -80,11 +80,11 @@ apply fast done -lemma sprodE [cases type: **]: +lemma sprodE [cases type: sprod]: "\p = \ \ Q; \x y. \p = (:x, y:); x \ \; y \ \\ \ Q\ \ Q" by (cut_tac z=p in Exh_Sprod, auto) -lemma sprod_induct [induct type: **]: +lemma sprod_induct [induct type: sprod]: "\P \; \x y. \x \ \; y \ \\ \ P (:x, y:)\ \ 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 \ 'b" assume "x \ y" thus "x = \ \ x = y" @@ -312,7 +312,7 @@ subsection {* Strict product is a bifinite domain *} -instantiation "**" :: (bifinite, bifinite) bifinite +instantiation sprod :: (bifinite, bifinite) bifinite begin definition diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Ssum.thy --- 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 \ ('a \ 'b). (fst p \ TT \ snd (snd p) = \) \ (fst p \ FF \ fst (snd p) = \)}" 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" ("(_ \/ _)" [21, 20] 20) + ssum :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) syntax (HTML output) - "++" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) + ssum :: "[type, type] => type" ("(_ \/ _)" [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]: "\p = \ \ Q; \x. \p = sinl\x; x \ \\ \ Q; \y. \p = sinr\y; y \ \\ \ Q\ \ Q" by (cut_tac z=p in Exh_Ssum, auto) -lemma ssum_induct [induct type: ++]: +lemma ssum_induct [induct type: ssum]: "\P \; \x. x \ \ \ P (sinl\x); \y. y \ \ \ P (sinr\y)\ \ 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 diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Tools/Domain/domain_axioms.ML --- 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"})]; diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Tools/Domain/domain_extender.ML --- 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.") diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Tools/Domain/domain_library.ML --- 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; diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Tools/cont_consts.ML --- 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 diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Tools/fixrec.ML --- 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); diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Tools/holcf_library.ML --- 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)); diff -r a2a59e92b02e -r fa231b86cb1e src/HOLCF/Tools/repdef.ML --- 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));