modernized specifications ('definition', 'abbreviation', 'notation');
authorwenzelm
Sun Oct 21 14:21:48 2007 +0200 (2007-10-21)
changeset 251312c8caac48ade
parent 25130 d91391a8705b
child 25132 dffe405b090d
modernized specifications ('definition', 'abbreviation', 'notation');
src/HOLCF/Adm.thy
src/HOLCF/Cfun.thy
src/HOLCF/Cont.thy
src/HOLCF/Cprod.thy
src/HOLCF/Discrete.thy
src/HOLCF/Fix.thy
src/HOLCF/Fixrec.thy
src/HOLCF/IOA/ABP/Correctness.thy
src/HOLCF/IOA/ABP/Env.thy
src/HOLCF/IOA/ABP/Impl.thy
src/HOLCF/IOA/ABP/Impl_finite.thy
src/HOLCF/IOA/ABP/Packet.thy
src/HOLCF/IOA/ABP/Receiver.thy
src/HOLCF/IOA/ABP/Sender.thy
src/HOLCF/IOA/Modelcheck/Ring3.thy
src/HOLCF/IOA/NTP/Correctness.thy
src/HOLCF/IOA/NTP/Packet.thy
src/HOLCF/IOA/Storage/Correctness.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/Lift.thy
src/HOLCF/One.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tr.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Adm.thy	Sun Oct 21 14:21:45 2007 +0200
     1.2 +++ b/src/HOLCF/Adm.thy	Sun Oct 21 14:21:48 2007 +0200
     1.3 @@ -13,12 +13,13 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -constdefs
     1.8 -  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
     1.9 -  "adm P \<equiv> \<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i)"
    1.10 +definition
    1.11 +  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
    1.12 +  "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
    1.13  
    1.14 -  compact :: "'a::cpo \<Rightarrow> bool"
    1.15 -  "compact k \<equiv> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.16 +definition
    1.17 +  compact :: "'a::cpo \<Rightarrow> bool" where
    1.18 +  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.19  
    1.20  lemma admI:
    1.21     "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
     2.1 --- a/src/HOLCF/Cfun.thy	Sun Oct 21 14:21:45 2007 +0200
     2.2 +++ b/src/HOLCF/Cfun.thy	Sun Oct 21 14:21:48 2007 +0200
     2.3 @@ -28,14 +28,14 @@
     2.4  syntax (xsymbols)
     2.5    "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
     2.6  
     2.7 -syntax
     2.8 -  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_$/_)" [999,1000] 999)
     2.9 +notation
    2.10 +  Rep_CFun  ("(_$/_)" [999,1000] 999)
    2.11  
    2.12 -syntax (xsymbols)
    2.13 -  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>/_)" [999,1000] 999)
    2.14 +notation (xsymbols)
    2.15 +  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
    2.16  
    2.17 -syntax (HTML output)
    2.18 -  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>/_)" [999,1000] 999)
    2.19 +notation (HTML output)
    2.20 +  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
    2.21  
    2.22  subsection {* Syntax for continuous lambda abstraction *}
    2.23  
    2.24 @@ -43,7 +43,7 @@
    2.25  
    2.26  parse_translation {*
    2.27  (* rewrites (_cabs x t) => (Abs_CFun (%x. t)) *)
    2.28 -  [mk_binder_tr ("_cabs", "Abs_CFun")];
    2.29 +  [mk_binder_tr ("_cabs", @{const_syntax Abs_CFun})];
    2.30  *}
    2.31  
    2.32  text {* To avoid eta-contraction of body: *}
    2.33 @@ -59,7 +59,7 @@
    2.34            val (x,t') = atomic_abs_tr' abs';
    2.35          in Syntax.const "_cabs" $ x $ t' end;
    2.36  
    2.37 -  in [("Abs_CFun", cabs_tr')] end;
    2.38 +  in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
    2.39  *}
    2.40  
    2.41  text {* Syntax for nested abstractions *}
    2.42 @@ -95,7 +95,7 @@
    2.43  
    2.44  text {* Dummy patterns for continuous abstraction *}
    2.45  translations
    2.46 -  "\<Lambda> _. t" => "Abs_CFun (\<lambda> _. t)"
    2.47 +  "\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
    2.48  
    2.49  
    2.50  subsection {* Continuous function space is pointed *}
    2.51 @@ -439,9 +439,9 @@
    2.52    ID      :: "'a \<rightarrow> 'a"
    2.53    cfcomp  :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"
    2.54  
    2.55 -syntax  "@oo" :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100)
    2.56 -     
    2.57 -translations  "f oo g" == "cfcomp\<cdot>f\<cdot>g"
    2.58 +abbreviation
    2.59 +  cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c"  (infixr "oo" 100)  where
    2.60 +  "f oo g == cfcomp\<cdot>f\<cdot>g"
    2.61  
    2.62  defs
    2.63    ID_def: "ID \<equiv> (\<Lambda> x. x)"
    2.64 @@ -481,9 +481,9 @@
    2.65  
    2.66  defaultsort pcpo
    2.67  
    2.68 -constdefs
    2.69 -  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b"
    2.70 -  "strictify \<equiv> (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    2.71 +definition
    2.72 +  strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
    2.73 +  "strictify = (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
    2.74  
    2.75  text {* results about strictify *}
    2.76  
    2.77 @@ -526,15 +526,15 @@
    2.78  
    2.79  subsection {* Continuous let-bindings *}
    2.80  
    2.81 -constdefs
    2.82 -  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
    2.83 -  "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
    2.84 +definition
    2.85 +  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b" where
    2.86 +  "CLet = (\<Lambda> s f. f\<cdot>s)"
    2.87  
    2.88  syntax
    2.89    "_CLet" :: "[letbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
    2.90  
    2.91  translations
    2.92    "_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
    2.93 -  "Let x = a in e" == "CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
    2.94 +  "Let x = a in e" == "CONST CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
    2.95  
    2.96  end
     3.1 --- a/src/HOLCF/Cont.thy	Sun Oct 21 14:21:45 2007 +0200
     3.2 +++ b/src/HOLCF/Cont.thy	Sun Oct 21 14:21:48 2007 +0200
     3.3 @@ -20,15 +20,17 @@
     3.4  
     3.5  subsection {* Definitions *}
     3.6  
     3.7 -constdefs
     3.8 -  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"
     3.9 -  "monofun f \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
    3.10 +definition
    3.11 +  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
    3.12 +  "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
    3.13  
    3.14 -  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def"
    3.15 -  "contlub f \<equiv> \<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
    3.16 +definition
    3.17 +  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def" where
    3.18 +  "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
    3.19  
    3.20 -  cont    :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "secnd cont. def"
    3.21 -  "cont f    \<equiv> \<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
    3.22 +definition
    3.23 +  cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "secnd cont. def" where
    3.24 +  "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
    3.25  
    3.26  lemma contlubI:
    3.27    "\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f"
     4.1 --- a/src/HOLCF/Cprod.thy	Sun Oct 21 14:21:45 2007 +0200
     4.2 +++ b/src/HOLCF/Cprod.thy	Sun Oct 21 14:21:48 2007 +0200
     4.3 @@ -29,12 +29,12 @@
     4.4  instance unit :: pcpo
     4.5  by intro_classes simp
     4.6  
     4.7 -constdefs
     4.8 -  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
     4.9 -  "unit_when \<equiv> \<Lambda> a _. a"
    4.10 +definition
    4.11 +  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    4.12 +  "unit_when = (\<Lambda> a _. a)"
    4.13  
    4.14  translations
    4.15 -  "\<Lambda>(). t" == "unit_when\<cdot>t"
    4.16 +  "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    4.17  
    4.18  lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    4.19  by (simp add: unit_when_def)
    4.20 @@ -192,18 +192,21 @@
    4.21  
    4.22  subsection {* Continuous versions of constants *}
    4.23  
    4.24 -constdefs
    4.25 -  cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *)
    4.26 -  "cpair \<equiv> (\<Lambda> x y. (x, y))"
    4.27 +definition
    4.28 +  cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)"  -- {* continuous pairing *}  where
    4.29 +  "cpair = (\<Lambda> x y. (x, y))"
    4.30 +
    4.31 +definition
    4.32 +  cfst :: "('a * 'b) \<rightarrow> 'a" where
    4.33 +  "cfst = (\<Lambda> p. fst p)"
    4.34  
    4.35 -  cfst :: "('a * 'b) \<rightarrow> 'a"
    4.36 -  "cfst \<equiv> (\<Lambda> p. fst p)"
    4.37 +definition
    4.38 +  csnd :: "('a * 'b) \<rightarrow> 'b" where
    4.39 +  "csnd = (\<Lambda> p. snd p)"      
    4.40  
    4.41 -  csnd :: "('a * 'b) \<rightarrow> 'b"
    4.42 -  "csnd \<equiv> (\<Lambda> p. snd p)"      
    4.43 -
    4.44 -  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c"
    4.45 -  "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
    4.46 +definition
    4.47 +  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
    4.48 +  "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
    4.49  
    4.50  syntax
    4.51    "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
    4.52 @@ -213,10 +216,10 @@
    4.53  
    4.54  translations
    4.55    "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
    4.56 -  "\<langle>x, y\<rangle>"    == "cpair\<cdot>x\<cdot>y"
    4.57 +  "\<langle>x, y\<rangle>"    == "CONST cpair\<cdot>x\<cdot>y"
    4.58  
    4.59  translations
    4.60 -  "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
    4.61 +  "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
    4.62  
    4.63  
    4.64  subsection {* Convert all lemmas to the continuous versions *}
     5.1 --- a/src/HOLCF/Discrete.thy	Sun Oct 21 14:21:45 2007 +0200
     5.2 +++ b/src/HOLCF/Discrete.thy	Sun Oct 21 14:21:48 2007 +0200
     5.3 @@ -56,9 +56,9 @@
     5.4  
     5.5  subsection {* @{term undiscr} *}
     5.6  
     5.7 -constdefs
     5.8 -   undiscr :: "('a::type)discr => 'a"
     5.9 -  "undiscr x == (case x of Discr y => y)"
    5.10 +definition
    5.11 +  undiscr :: "('a::type)discr => 'a" where
    5.12 +  "undiscr x = (case x of Discr y => y)"
    5.13  
    5.14  lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
    5.15  by (simp add: undiscr_def)
     6.1 --- a/src/HOLCF/Fix.thy	Sun Oct 21 14:21:45 2007 +0200
     6.2 +++ b/src/HOLCF/Fix.thy	Sun Oct 21 14:21:48 2007 +0200
     6.3 @@ -49,9 +49,9 @@
     6.4  
     6.5  subsection {* Least fixed point operator *}
     6.6  
     6.7 -constdefs
     6.8 -  "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a"
     6.9 -  "fix \<equiv> \<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>"
    6.10 +definition
    6.11 +  "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
    6.12 +  "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
    6.13  
    6.14  text {* Binder syntax for @{term fix} *}
    6.15  
    6.16 @@ -62,7 +62,7 @@
    6.17    "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
    6.18  
    6.19  translations
    6.20 -  "\<mu> x. t" == "fix\<cdot>(\<Lambda> x. t)"
    6.21 +  "\<mu> x. t" == "CONST fix\<cdot>(\<Lambda> x. t)"
    6.22  
    6.23  text {* Properties of @{term fix} *}
    6.24  
    6.25 @@ -164,9 +164,9 @@
    6.26  
    6.27  subsection {* Recursive let bindings *}
    6.28  
    6.29 -constdefs
    6.30 -  CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b"
    6.31 -  "CLetrec \<equiv> \<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x)))"
    6.32 +definition
    6.33 +  CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
    6.34 +  "CLetrec = (\<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x))))"
    6.35  
    6.36  nonterminals
    6.37    recbinds recbindt recbind
    6.38 @@ -181,12 +181,12 @@
    6.39  
    6.40  translations
    6.41    (recbindt) "x = a, \<langle>y,ys\<rangle> = \<langle>b,bs\<rangle>" == (recbindt) "\<langle>x,y,ys\<rangle> = \<langle>a,b,bs\<rangle>"
    6.42 -  (recbindt) "x = a, y = b"           == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
    6.43 +  (recbindt) "x = a, y = b"          == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
    6.44  
    6.45  translations
    6.46    "_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
    6.47 -  "Letrec xs = a in \<langle>e,es\<rangle>"    == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
    6.48 -  "Letrec xs = a in e"         == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
    6.49 +  "Letrec xs = a in \<langle>e,es\<rangle>"    == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
    6.50 +  "Letrec xs = a in e"         == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
    6.51  
    6.52  text {*
    6.53    Bekic's Theorem: Simultaneous fixed points over pairs
    6.54 @@ -222,9 +222,9 @@
    6.55  
    6.56  subsection {* Weak admissibility *}
    6.57  
    6.58 -constdefs
    6.59 -  admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    6.60 -  "admw P \<equiv> \<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
    6.61 +definition
    6.62 +  admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    6.63 +  "admw P = (\<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>))"
    6.64  
    6.65  text {* an admissible formula is also weak admissible *}
    6.66  
     7.1 --- a/src/HOLCF/Fixrec.thy	Sun Oct 21 14:21:45 2007 +0200
     7.2 +++ b/src/HOLCF/Fixrec.thy	Sun Oct 21 14:21:48 2007 +0200
     7.3 @@ -21,11 +21,13 @@
     7.4    fail :: "'a maybe"
     7.5    "fail \<equiv> Abs_maybe (sinl\<cdot>ONE)"
     7.6  
     7.7 -  return :: "'a \<rightarrow> 'a maybe"
     7.8 +constdefs
     7.9 +  return :: "'a \<rightarrow> 'a maybe" where
    7.10    "return \<equiv> \<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x))"
    7.11  
    7.12 -  maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo"
    7.13 -  "maybe_when \<equiv> \<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m)"
    7.14 +definition
    7.15 +  maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo" where
    7.16 +  "maybe_when = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m))"
    7.17  
    7.18  lemma maybeE:
    7.19    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    7.20 @@ -57,14 +59,14 @@
    7.21                    cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
    7.22  
    7.23  translations
    7.24 -  "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
    7.25 +  "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
    7.26  
    7.27  
    7.28  subsubsection {* Monadic bind operator *}
    7.29  
    7.30 -constdefs
    7.31 -  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
    7.32 -  "bind \<equiv> \<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x"
    7.33 +definition
    7.34 +  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
    7.35 +  "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
    7.36  
    7.37  text {* monad laws *}
    7.38  
    7.39 @@ -86,9 +88,9 @@
    7.40  
    7.41  subsubsection {* Run operator *}
    7.42  
    7.43 -constdefs
    7.44 -  run:: "'a maybe \<rightarrow> 'a::pcpo"
    7.45 -  "run \<equiv> maybe_when\<cdot>\<bottom>\<cdot>ID"
    7.46 +definition
    7.47 +  run:: "'a maybe \<rightarrow> 'a::pcpo" where
    7.48 +  "run = maybe_when\<cdot>\<bottom>\<cdot>ID"
    7.49  
    7.50  text {* rewrite rules for run *}
    7.51  
    7.52 @@ -103,12 +105,13 @@
    7.53  
    7.54  subsubsection {* Monad plus operator *}
    7.55  
    7.56 -constdefs
    7.57 -  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
    7.58 -  "mplus \<equiv> \<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1"
    7.59 +definition
    7.60 +  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" where
    7.61 +  "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1)"
    7.62  
    7.63 -syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
    7.64 -translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
    7.65 +abbreviation
    7.66 +  mplus_syn :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe"  (infixr "+++" 65)  where
    7.67 +  "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2"
    7.68  
    7.69  text {* rewrite rules for mplus *}
    7.70  
    7.71 @@ -129,14 +132,13 @@
    7.72  
    7.73  subsubsection {* Fatbar combinator *}
    7.74  
    7.75 -constdefs
    7.76 -  fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
    7.77 -  "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
    7.78 +definition
    7.79 +  fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)" where
    7.80 +  "fatbar = (\<Lambda> a b x. a\<cdot>x +++ b\<cdot>x)"
    7.81  
    7.82 -syntax
    7.83 -  "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
    7.84 -translations
    7.85 -  "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
    7.86 +abbreviation
    7.87 +  fatbar_syn :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)  where
    7.88 +  "m1 \<parallel> m2 == fatbar\<cdot>m1\<cdot>m2"
    7.89  
    7.90  lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
    7.91  by (simp add: fatbar_def)
    7.92 @@ -201,15 +203,15 @@
    7.93    "_var" :: "'a"
    7.94  
    7.95  translations
    7.96 -  "_Case1 p r" => "branch (_pat p)\<cdot>(_var p r)"
    7.97 -  "_var (_args x y) r" => "csplit\<cdot>(_var x (_var y r))"
    7.98 -  "_var () r" => "unit_when\<cdot>r"
    7.99 +  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
   7.100 +  "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
   7.101 +  "_var () r" => "CONST unit_when\<cdot>r"
   7.102  
   7.103  parse_translation {*
   7.104  (* rewrites (_pat x) => (return) *)
   7.105  (* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
   7.106    [("_pat", K (Syntax.const "Fixrec.return")),
   7.107 -   mk_binder_tr ("_var", "Abs_CFun")];
   7.108 +   mk_binder_tr ("_var", @{const_syntax Abs_CFun})];
   7.109  *}
   7.110  
   7.111  text {* Printing Case expressions *}
   7.112 @@ -219,14 +221,14 @@
   7.113  
   7.114  print_translation {*
   7.115    let
   7.116 -    fun dest_LAM (Const ("Rep_CFun",_) $ Const ("unit_when",_) $ t) =
   7.117 -          (Syntax.const "Unity", t)
   7.118 -    |   dest_LAM (Const ("Rep_CFun",_) $ Const ("csplit",_) $ t) =
   7.119 +    fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
   7.120 +          (Syntax.const @{const_syntax Unity}, t)
   7.121 +    |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
   7.122            let
   7.123              val (v1, t1) = dest_LAM t;
   7.124              val (v2, t2) = dest_LAM t1;
   7.125            in (Syntax.const "_args" $ v1 $ v2, t2) end 
   7.126 -    |   dest_LAM (Const ("Abs_CFun",_) $ t) =
   7.127 +    |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
   7.128            let
   7.129              val abs = case t of Abs abs => abs
   7.130                  | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   7.131 @@ -234,11 +236,11 @@
   7.132            in (Syntax.const "_var" $ x, t') end
   7.133      |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
   7.134  
   7.135 -    fun Case1_tr' [Const("branch",_) $ p, r] =
   7.136 +    fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
   7.137            let val (v, t) = dest_LAM r;
   7.138            in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
   7.139  
   7.140 -  in [("Rep_CFun", Case1_tr')] end;
   7.141 +  in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
   7.142  *}
   7.143  
   7.144  translations
   7.145 @@ -249,67 +251,74 @@
   7.146  
   7.147  types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
   7.148  
   7.149 -constdefs
   7.150 -  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat"
   7.151 -  "cpair_pat p1 p2 \<equiv> \<Lambda>\<langle>x, y\<rangle>.
   7.152 -    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>))"
   7.153 +definition
   7.154 +  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
   7.155 +  "cpair_pat p1 p2 = (\<Lambda>\<langle>x, y\<rangle>.
   7.156 +    bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>)))"
   7.157  
   7.158 +definition
   7.159    spair_pat ::
   7.160 -  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat"
   7.161 -  "spair_pat p1 p2 \<equiv> \<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>"
   7.162 +  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
   7.163 +  "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>)"
   7.164  
   7.165 -  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
   7.166 -  "sinl_pat p \<equiv> sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
   7.167 +definition
   7.168 +  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
   7.169 +  "sinl_pat p = sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
   7.170  
   7.171 -  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
   7.172 -  "sinr_pat p \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
   7.173 +definition
   7.174 +  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
   7.175 +  "sinr_pat p = sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
   7.176  
   7.177 -  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat"
   7.178 -  "up_pat p \<equiv> fup\<cdot>p"
   7.179 +definition
   7.180 +  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where
   7.181 +  "up_pat p = fup\<cdot>p"
   7.182  
   7.183 -  TT_pat :: "(tr, unit) pat"
   7.184 -  "TT_pat \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
   7.185 +definition
   7.186 +  TT_pat :: "(tr, unit) pat" where
   7.187 +  "TT_pat = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
   7.188  
   7.189 -  FF_pat :: "(tr, unit) pat"
   7.190 -  "FF_pat \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
   7.191 +definition
   7.192 +  FF_pat :: "(tr, unit) pat" where
   7.193 +  "FF_pat = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
   7.194  
   7.195 -  ONE_pat :: "(one, unit) pat"
   7.196 -  "ONE_pat \<equiv> \<Lambda> ONE. return\<cdot>()"
   7.197 +definition
   7.198 +  ONE_pat :: "(one, unit) pat" where
   7.199 +  "ONE_pat = (\<Lambda> ONE. return\<cdot>())"
   7.200  
   7.201  text {* Parse translations (patterns) *}
   7.202  translations
   7.203 -  "_pat (cpair\<cdot>x\<cdot>y)" => "cpair_pat (_pat x) (_pat y)"
   7.204 -  "_pat (spair\<cdot>x\<cdot>y)" => "spair_pat (_pat x) (_pat y)"
   7.205 -  "_pat (sinl\<cdot>x)" => "sinl_pat (_pat x)"
   7.206 -  "_pat (sinr\<cdot>x)" => "sinr_pat (_pat x)"
   7.207 -  "_pat (up\<cdot>x)" => "up_pat (_pat x)"
   7.208 -  "_pat TT" => "TT_pat"
   7.209 -  "_pat FF" => "FF_pat"
   7.210 -  "_pat ONE" => "ONE_pat"
   7.211 +  "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
   7.212 +  "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
   7.213 +  "_pat (CONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
   7.214 +  "_pat (CONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
   7.215 +  "_pat (CONST up\<cdot>x)" => "CONST up_pat (_pat x)"
   7.216 +  "_pat (CONST TT)" => "CONST TT_pat"
   7.217 +  "_pat (CONST FF)" => "CONST FF_pat"
   7.218 +  "_pat (CONST ONE)" => "CONST ONE_pat"
   7.219  
   7.220  text {* Parse translations (variables) *}
   7.221  translations
   7.222 -  "_var (cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
   7.223 -  "_var (spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
   7.224 -  "_var (sinl\<cdot>x) r" => "_var x r"
   7.225 -  "_var (sinr\<cdot>x) r" => "_var x r"
   7.226 -  "_var (up\<cdot>x) r" => "_var x r"
   7.227 -  "_var TT r" => "_var () r"
   7.228 -  "_var FF r" => "_var () r"
   7.229 -  "_var ONE r" => "_var () r"
   7.230 +  "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
   7.231 +  "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
   7.232 +  "_var (CONST sinl\<cdot>x) r" => "_var x r"
   7.233 +  "_var (CONST sinr\<cdot>x) r" => "_var x r"
   7.234 +  "_var (CONST up\<cdot>x) r" => "_var x r"
   7.235 +  "_var (CONST TT) r" => "_var () r"
   7.236 +  "_var (CONST FF) r" => "_var () r"
   7.237 +  "_var (CONST ONE) r" => "_var () r"
   7.238  
   7.239  text {* Print translations *}
   7.240  translations
   7.241 -  "cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   7.242 -      <= "_match (cpair_pat p1 p2) (_args v1 v2)"
   7.243 -  "spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   7.244 -      <= "_match (spair_pat p1 p2) (_args v1 v2)"
   7.245 -  "sinl\<cdot>(_match p1 v1)" <= "_match (sinl_pat p1) v1"
   7.246 -  "sinr\<cdot>(_match p1 v1)" <= "_match (sinr_pat p1) v1"
   7.247 -  "up\<cdot>(_match p1 v1)" <= "_match (up_pat p1) v1"
   7.248 -  "TT" <= "_match TT_pat ()"
   7.249 -  "FF" <= "_match FF_pat ()"
   7.250 -  "ONE" <= "_match ONE_pat ()"
   7.251 +  "CONST cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   7.252 +      <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
   7.253 +  "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
   7.254 +      <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
   7.255 +  "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
   7.256 +  "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
   7.257 +  "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
   7.258 +  "CONST TT" <= "_match (CONST TT_pat) ()"
   7.259 +  "CONST FF" <= "_match (CONST FF_pat) ()"
   7.260 +  "CONST ONE" <= "_match (CONST ONE_pat) ()"
   7.261  
   7.262  lemma cpair_pat1:
   7.263    "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
   7.264 @@ -382,21 +391,23 @@
   7.265    "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
   7.266    "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
   7.267  
   7.268 -constdefs
   7.269 -  wild_pat :: "'a \<rightarrow> unit maybe"
   7.270 -  "wild_pat \<equiv> \<Lambda> x. return\<cdot>()"
   7.271 +definition
   7.272 +  wild_pat :: "'a \<rightarrow> unit maybe" where
   7.273 +  "wild_pat = (\<Lambda> x. return\<cdot>())"
   7.274  
   7.275 -  as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe"
   7.276 -  "as_pat p \<equiv> \<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>)"
   7.277 +definition
   7.278 +  as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
   7.279 +  "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>))"
   7.280  
   7.281 -  lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)"
   7.282 -  "lazy_pat p \<equiv> \<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x))"
   7.283 +definition
   7.284 +  lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
   7.285 +  "lazy_pat p = (\<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x)))"
   7.286  
   7.287  text {* Parse translations (patterns) *}
   7.288  translations
   7.289 -  "_pat _" => "wild_pat"
   7.290 -  "_pat (_as_pat x y)" => "as_pat (_pat y)"
   7.291 -  "_pat (_lazy_pat x)" => "lazy_pat (_pat x)"
   7.292 +  "_pat _" => "CONST wild_pat"
   7.293 +  "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
   7.294 +  "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
   7.295  
   7.296  text {* Parse translations (variables) *}
   7.297  translations
   7.298 @@ -406,13 +417,13 @@
   7.299  
   7.300  text {* Print translations *}
   7.301  translations
   7.302 -  "_" <= "_match wild_pat ()"
   7.303 -  "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
   7.304 -  "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
   7.305 +  "_" <= "_match (CONST wild_pat) ()"
   7.306 +  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
   7.307 +  "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
   7.308  
   7.309  text {* Lazy patterns in lambda abstractions *}
   7.310  translations
   7.311 -  "_cabs (_lazy_pat p) r" == "run oo (_Case1 (_lazy_pat p) r)"
   7.312 +  "_cabs (_lazy_pat p) r" == "CONST run oo (_Case1 (_lazy_pat p) r)"
   7.313  
   7.314  lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
   7.315  by (simp add: branch_def wild_pat_def)
   7.316 @@ -436,33 +447,41 @@
   7.317  
   7.318  defaultsort pcpo
   7.319  
   7.320 -constdefs
   7.321 -  match_UU :: "'a \<rightarrow> unit maybe"
   7.322 -  "match_UU \<equiv> \<Lambda> x. fail"
   7.323 +definition
   7.324 +  match_UU :: "'a \<rightarrow> unit maybe" where
   7.325 +  "match_UU = (\<Lambda> x. fail)"
   7.326 +
   7.327 +definition
   7.328 +  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe" where
   7.329 +  "match_cpair = csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   7.330  
   7.331 -  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
   7.332 -  "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   7.333 +definition
   7.334 +  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe" where
   7.335 +  "match_spair = ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   7.336  
   7.337 -  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
   7.338 -  "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
   7.339 -
   7.340 -  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
   7.341 -  "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
   7.342 +definition
   7.343 +  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe" where
   7.344 +  "match_sinl = sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
   7.345  
   7.346 -  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
   7.347 -  "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
   7.348 +definition
   7.349 +  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe" where
   7.350 +  "match_sinr = sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
   7.351  
   7.352 -  match_up :: "'a::cpo u \<rightarrow> 'a maybe"
   7.353 -  "match_up \<equiv> fup\<cdot>return"
   7.354 +definition
   7.355 +  match_up :: "'a::cpo u \<rightarrow> 'a maybe" where
   7.356 +  "match_up = fup\<cdot>return"
   7.357  
   7.358 -  match_ONE :: "one \<rightarrow> unit maybe"
   7.359 -  "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
   7.360 +definition
   7.361 +  match_ONE :: "one \<rightarrow> unit maybe" where
   7.362 +  "match_ONE = (\<Lambda> ONE. return\<cdot>())"
   7.363   
   7.364 -  match_TT :: "tr \<rightarrow> unit maybe"
   7.365 -  "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
   7.366 +definition
   7.367 +  match_TT :: "tr \<rightarrow> unit maybe" where
   7.368 +  "match_TT = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
   7.369   
   7.370 -  match_FF :: "tr \<rightarrow> unit maybe"
   7.371 -  "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
   7.372 +definition
   7.373 +  match_FF :: "tr \<rightarrow> unit maybe" where
   7.374 +  "match_FF = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
   7.375  
   7.376  lemma match_UU_simps [simp]:
   7.377    "match_UU\<cdot>x = fail"
   7.378 @@ -532,13 +551,6 @@
   7.379  lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
   7.380  by simp
   7.381  
   7.382 -ML {*
   7.383 -val cpair_equalI = thm "cpair_equalI";
   7.384 -val cpair_eqD1 = thm "cpair_eqD1";
   7.385 -val cpair_eqD2 = thm "cpair_eqD2";
   7.386 -val ssubst_lhs = thm "ssubst_lhs";
   7.387 -val branch_def = thm "branch_def";
   7.388 -*}
   7.389  
   7.390  subsection {* Initializing the fixrec package *}
   7.391  
     8.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy	Sun Oct 21 14:21:45 2007 +0200
     8.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Sun Oct 21 14:21:48 2007 +0200
     8.3 @@ -20,22 +20,23 @@
     8.4                                then reduce xs
     8.5                                else (x#(reduce xs))))"
     8.6  
     8.7 -constdefs
     8.8 +definition
     8.9    abs where
    8.10 -    "abs  ==
    8.11 +    "abs  =
    8.12        (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
    8.13         (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
    8.14  
    8.15 -  system_ioa       :: "('m action, bool * 'm impl_state)ioa"
    8.16 -  "system_ioa == (env_ioa || impl_ioa)"
    8.17 +definition
    8.18 +  system_ioa :: "('m action, bool * 'm impl_state)ioa" where
    8.19 +  "system_ioa = (env_ioa || impl_ioa)"
    8.20  
    8.21 -  system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
    8.22 -  "system_fin_ioa == (env_ioa || impl_fin_ioa)"
    8.23 +definition
    8.24 +  system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" where
    8.25 +  "system_fin_ioa = (env_ioa || impl_fin_ioa)"
    8.26  
    8.27  
    8.28 -axioms
    8.29 -
    8.30 -  sys_IOA:     "IOA system_ioa"
    8.31 +axiomatization where
    8.32 +  sys_IOA: "IOA system_ioa" and
    8.33    sys_fin_IOA: "IOA system_fin_ioa"
    8.34  
    8.35  
     9.1 --- a/src/HOLCF/IOA/ABP/Env.thy	Sun Oct 21 14:21:45 2007 +0200
     9.2 +++ b/src/HOLCF/IOA/ABP/Env.thy	Sun Oct 21 14:21:48 2007 +0200
     9.3 @@ -12,30 +12,32 @@
     9.4  types
     9.5    'm env_state = bool   -- {* give next bit to system *}
     9.6  
     9.7 -constdefs
     9.8 -env_asig   :: "'m action signature"
     9.9 -"env_asig == ({Next},
    9.10 -               UN m. {S_msg(m)},
    9.11 -               {})"
    9.12 +definition
    9.13 +  env_asig :: "'m action signature" where
    9.14 +  "env_asig == ({Next},
    9.15 +                 UN m. {S_msg(m)},
    9.16 +                 {})"
    9.17  
    9.18 -env_trans  :: "('m action, 'm env_state)transition set"
    9.19 -"env_trans ==
    9.20 - {tr. let s = fst(tr);
    9.21 -          t = snd(snd(tr))
    9.22 -      in case fst(snd(tr))
    9.23 -      of
    9.24 -      Next       => t=True |
    9.25 -      S_msg(m)   => s=True & t=False |
    9.26 -      R_msg(m)   => False |
    9.27 -      S_pkt(pkt) => False |
    9.28 -      R_pkt(pkt) => False |
    9.29 -      S_ack(b)   => False |
    9.30 -      R_ack(b)   => False}"
    9.31 +definition
    9.32 +  env_trans :: "('m action, 'm env_state)transition set" where
    9.33 +  "env_trans =
    9.34 +   {tr. let s = fst(tr);
    9.35 +            t = snd(snd(tr))
    9.36 +        in case fst(snd(tr))
    9.37 +        of
    9.38 +        Next       => t=True |
    9.39 +        S_msg(m)   => s=True & t=False |
    9.40 +        R_msg(m)   => False |
    9.41 +        S_pkt(pkt) => False |
    9.42 +        R_pkt(pkt) => False |
    9.43 +        S_ack(b)   => False |
    9.44 +        R_ack(b)   => False}"
    9.45  
    9.46 -env_ioa    :: "('m action, 'm env_state)ioa"
    9.47 -"env_ioa == (env_asig, {True}, env_trans,{},{})"
    9.48 +definition
    9.49 +  env_ioa :: "('m action, 'm env_state)ioa" where
    9.50 +  "env_ioa = (env_asig, {True}, env_trans,{},{})"
    9.51  
    9.52 -consts
    9.53 -  "next"     :: "'m env_state => bool"
    9.54 +axiomatization
    9.55 +  "next" :: "'m env_state => bool"
    9.56  
    9.57  end
    10.1 --- a/src/HOLCF/IOA/ABP/Impl.thy	Sun Oct 21 14:21:45 2007 +0200
    10.2 +++ b/src/HOLCF/IOA/ABP/Impl.thy	Sun Oct 21 14:21:48 2007 +0200
    10.3 @@ -13,21 +13,24 @@
    10.4    'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    10.5    (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
    10.6  
    10.7 -constdefs
    10.8 +definition
    10.9 + impl_ioa :: "('m action, 'm impl_state)ioa" where
   10.10 + "impl_ioa = (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
   10.11  
   10.12 - impl_ioa    :: "('m action, 'm impl_state)ioa"
   10.13 - "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
   10.14 -
   10.15 - sen         :: "'m impl_state => 'm sender_state"
   10.16 - "sen == fst"
   10.17 +definition
   10.18 + sen :: "'m impl_state => 'm sender_state" where
   10.19 + "sen = fst"
   10.20  
   10.21 - rec         :: "'m impl_state => 'm receiver_state"
   10.22 - "rec == fst o snd"
   10.23 +definition
   10.24 + rec :: "'m impl_state => 'm receiver_state" where
   10.25 + "rec = fst o snd"
   10.26  
   10.27 - srch        :: "'m impl_state => 'm packet list"
   10.28 - "srch == fst o snd o snd"
   10.29 +definition
   10.30 + srch :: "'m impl_state => 'm packet list" where
   10.31 + "srch = fst o snd o snd"
   10.32  
   10.33 - rsch        :: "'m impl_state => bool list"
   10.34 - "rsch == snd o snd o snd"
   10.35 +definition
   10.36 + rsch :: "'m impl_state => bool list" where
   10.37 + "rsch = snd o snd o snd"
   10.38  
   10.39  end
    11.1 --- a/src/HOLCF/IOA/ABP/Impl_finite.thy	Sun Oct 21 14:21:45 2007 +0200
    11.2 +++ b/src/HOLCF/IOA/ABP/Impl_finite.thy	Sun Oct 21 14:21:48 2007 +0200
    11.3 @@ -14,22 +14,25 @@
    11.4      = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    11.5  (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
    11.6  
    11.7 -constdefs
    11.8 +definition
    11.9 +  impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
   11.10 +  "impl_fin_ioa = (sender_ioa || receiver_ioa || srch_fin_ioa ||
   11.11 +                  rsch_fin_ioa)"
   11.12  
   11.13 - impl_fin_ioa    :: "('m action, 'm impl_fin_state)ioa"
   11.14 - "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
   11.15 -                   rsch_fin_ioa)"
   11.16 -
   11.17 - sen_fin         :: "'m impl_fin_state => 'm sender_state"
   11.18 - "sen_fin == fst"
   11.19 +definition
   11.20 +  sen_fin :: "'m impl_fin_state => 'm sender_state" where
   11.21 +  "sen_fin = fst"
   11.22  
   11.23 - rec_fin         :: "'m impl_fin_state => 'm receiver_state"
   11.24 - "rec_fin == fst o snd"
   11.25 +definition
   11.26 +  rec_fin :: "'m impl_fin_state => 'm receiver_state" where
   11.27 +  "rec_fin = fst o snd"
   11.28  
   11.29 - srch_fin        :: "'m impl_fin_state => 'm packet list"
   11.30 - "srch_fin == fst o snd o snd"
   11.31 +definition
   11.32 +  srch_fin :: "'m impl_fin_state => 'm packet list" where
   11.33 +  "srch_fin = fst o snd o snd"
   11.34  
   11.35 - rsch_fin        :: "'m impl_fin_state => bool list"
   11.36 - "rsch_fin == snd o snd o snd"
   11.37 +definition
   11.38 +  rsch_fin :: "'m impl_fin_state => bool list" where
   11.39 +  "rsch_fin = snd o snd o snd"
   11.40  
   11.41  end
    12.1 --- a/src/HOLCF/IOA/ABP/Packet.thy	Sun Oct 21 14:21:45 2007 +0200
    12.2 +++ b/src/HOLCF/IOA/ABP/Packet.thy	Sun Oct 21 14:21:48 2007 +0200
    12.3 @@ -12,11 +12,12 @@
    12.4  types
    12.5    'msg packet = "bool * 'msg"
    12.6  
    12.7 -constdefs
    12.8 -  hdr  :: "'msg packet => bool"
    12.9 -  "hdr == fst"
   12.10 +definition
   12.11 +  hdr :: "'msg packet => bool" where
   12.12 +  "hdr = fst"
   12.13  
   12.14 -  msg :: "'msg packet => 'msg"
   12.15 -  "msg == snd"
   12.16 +definition
   12.17 +  msg :: "'msg packet => 'msg" where
   12.18 +  "msg = snd"
   12.19  
   12.20  end
    13.1 --- a/src/HOLCF/IOA/ABP/Receiver.thy	Sun Oct 21 14:21:45 2007 +0200
    13.2 +++ b/src/HOLCF/IOA/ABP/Receiver.thy	Sun Oct 21 14:21:48 2007 +0200
    13.3 @@ -12,43 +12,47 @@
    13.4  types
    13.5    'm receiver_state = "'m list * bool"  -- {* messages, mode *}
    13.6  
    13.7 -constdefs
    13.8 -  rq            :: "'m receiver_state => 'm list"
    13.9 -  "rq == fst"
   13.10 +definition
   13.11 +  rq :: "'m receiver_state => 'm list" where
   13.12 +  "rq = fst"
   13.13  
   13.14 -  rbit          :: "'m receiver_state => bool"
   13.15 -  "rbit == snd"
   13.16 +definition
   13.17 +  rbit :: "'m receiver_state => bool" where
   13.18 +  "rbit = snd"
   13.19  
   13.20 -receiver_asig :: "'m action signature"
   13.21 -"receiver_asig ==
   13.22 -  (UN pkt. {R_pkt(pkt)},
   13.23 -  (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
   13.24 -  {})"
   13.25 +definition
   13.26 +  receiver_asig :: "'m action signature" where
   13.27 +  "receiver_asig =
   13.28 +    (UN pkt. {R_pkt(pkt)},
   13.29 +    (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
   13.30 +    {})"
   13.31  
   13.32 -receiver_trans :: "('m action, 'm receiver_state)transition set"
   13.33 -"receiver_trans ==
   13.34 - {tr. let s = fst(tr);
   13.35 -          t = snd(snd(tr))
   13.36 -      in
   13.37 -      case fst(snd(tr))
   13.38 -      of
   13.39 -      Next    =>  False |
   13.40 -      S_msg(m) => False |
   13.41 -      R_msg(m) => (rq(s) ~= [])  &
   13.42 -                   m = hd(rq(s))  &
   13.43 -                   rq(t) = tl(rq(s))   &
   13.44 -                  rbit(t)=rbit(s)  |
   13.45 -      S_pkt(pkt) => False |
   13.46 -      R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
   13.47 -                         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
   13.48 -                         rq(t) =rq(s) & rbit(t)=rbit(s)  |
   13.49 -      S_ack(b) => b = rbit(s)                        &
   13.50 -                      rq(t) = rq(s)                    &
   13.51 -                      rbit(t)=rbit(s) |
   13.52 -      R_ack(b) => False}"
   13.53 +definition
   13.54 +  receiver_trans :: "('m action, 'm receiver_state)transition set" where
   13.55 +  "receiver_trans =
   13.56 +   {tr. let s = fst(tr);
   13.57 +            t = snd(snd(tr))
   13.58 +        in
   13.59 +        case fst(snd(tr))
   13.60 +        of
   13.61 +        Next    =>  False |
   13.62 +        S_msg(m) => False |
   13.63 +        R_msg(m) => (rq(s) ~= [])  &
   13.64 +                     m = hd(rq(s))  &
   13.65 +                     rq(t) = tl(rq(s))   &
   13.66 +                    rbit(t)=rbit(s)  |
   13.67 +        S_pkt(pkt) => False |
   13.68 +        R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
   13.69 +                           rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
   13.70 +                           rq(t) =rq(s) & rbit(t)=rbit(s)  |
   13.71 +        S_ack(b) => b = rbit(s)                        &
   13.72 +                        rq(t) = rq(s)                    &
   13.73 +                        rbit(t)=rbit(s) |
   13.74 +        R_ack(b) => False}"
   13.75  
   13.76 -receiver_ioa :: "('m action, 'm receiver_state)ioa"
   13.77 -"receiver_ioa ==
   13.78 - (receiver_asig, {([],False)}, receiver_trans,{},{})"
   13.79 +definition
   13.80 +  receiver_ioa :: "('m action, 'm receiver_state)ioa" where
   13.81 +  "receiver_ioa =
   13.82 +   (receiver_asig, {([],False)}, receiver_trans,{},{})"
   13.83  
   13.84  end
    14.1 --- a/src/HOLCF/IOA/ABP/Sender.thy	Sun Oct 21 14:21:45 2007 +0200
    14.2 +++ b/src/HOLCF/IOA/ABP/Sender.thy	Sun Oct 21 14:21:48 2007 +0200
    14.3 @@ -12,41 +12,45 @@
    14.4  types
    14.5    'm sender_state = "'m list  *  bool"  -- {* messages, Alternating Bit *}
    14.6  
    14.7 -constdefs
    14.8 -sq            :: "'m sender_state => 'm list"
    14.9 -"sq == fst"
   14.10 +definition
   14.11 +  sq :: "'m sender_state => 'm list" where
   14.12 +  "sq = fst"
   14.13  
   14.14 -sbit          :: "'m sender_state => bool"
   14.15 -"sbit == snd"
   14.16 +definition
   14.17 +  sbit :: "'m sender_state => bool" where
   14.18 +  "sbit = snd"
   14.19  
   14.20 -sender_asig   :: "'m action signature"
   14.21 -"sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
   14.22 -                  UN pkt. {S_pkt(pkt)},
   14.23 -                  {})"
   14.24 +definition
   14.25 +  sender_asig :: "'m action signature" where
   14.26 +  "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
   14.27 +                   UN pkt. {S_pkt(pkt)},
   14.28 +                   {})"
   14.29  
   14.30 -sender_trans  :: "('m action, 'm sender_state)transition set"
   14.31 -"sender_trans ==
   14.32 - {tr. let s = fst(tr);
   14.33 -          t = snd(snd(tr))
   14.34 -      in case fst(snd(tr))
   14.35 -      of
   14.36 -      Next     => if sq(s)=[] then t=s else False |
   14.37 -      S_msg(m) => sq(t)=sq(s)@[m]   &
   14.38 -                  sbit(t)=sbit(s)  |
   14.39 -      R_msg(m) => False |
   14.40 -      S_pkt(pkt) => sq(s) ~= []  &
   14.41 -                     hdr(pkt) = sbit(s)      &
   14.42 -                    msg(pkt) = hd(sq(s))    &
   14.43 -                    sq(t) = sq(s)           &
   14.44 -                    sbit(t) = sbit(s) |
   14.45 -      R_pkt(pkt) => False |
   14.46 -      S_ack(b)   => False |
   14.47 -      R_ack(b)   => if b = sbit(s) then
   14.48 -                     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
   14.49 -                     sq(t)=sq(s) & sbit(t)=sbit(s)}"
   14.50 -
   14.51 -sender_ioa    :: "('m action, 'm sender_state)ioa"
   14.52 -"sender_ioa ==
   14.53 - (sender_asig, {([],True)}, sender_trans,{},{})"
   14.54 +definition
   14.55 +  sender_trans :: "('m action, 'm sender_state)transition set" where
   14.56 +  "sender_trans =
   14.57 +   {tr. let s = fst(tr);
   14.58 +            t = snd(snd(tr))
   14.59 +        in case fst(snd(tr))
   14.60 +        of
   14.61 +        Next     => if sq(s)=[] then t=s else False |
   14.62 +        S_msg(m) => sq(t)=sq(s)@[m]   &
   14.63 +                    sbit(t)=sbit(s)  |
   14.64 +        R_msg(m) => False |
   14.65 +        S_pkt(pkt) => sq(s) ~= []  &
   14.66 +                       hdr(pkt) = sbit(s)      &
   14.67 +                      msg(pkt) = hd(sq(s))    &
   14.68 +                      sq(t) = sq(s)           &
   14.69 +                      sbit(t) = sbit(s) |
   14.70 +        R_pkt(pkt) => False |
   14.71 +        S_ack(b)   => False |
   14.72 +        R_ack(b)   => if b = sbit(s) then
   14.73 +                       sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
   14.74 +                       sq(t)=sq(s) & sbit(t)=sbit(s)}"
   14.75 +  
   14.76 +definition
   14.77 +  sender_ioa :: "('m action, 'm sender_state)ioa" where
   14.78 +  "sender_ioa =
   14.79 +   (sender_asig, {([],True)}, sender_trans,{},{})"
   14.80  
   14.81  end
    15.1 --- a/src/HOLCF/IOA/Modelcheck/Ring3.thy	Sun Oct 21 14:21:45 2007 +0200
    15.2 +++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy	Sun Oct 21 14:21:48 2007 +0200
    15.3 @@ -11,9 +11,9 @@
    15.4    Zero_One token | One_Two token | Two_Zero token |
    15.5    Leader_Zero | Leader_One | Leader_Two
    15.6  
    15.7 -constdefs
    15.8 -  Greater :: "[token, token] => bool"
    15.9 -  "Greater x y ==
   15.10 +definition
   15.11 +  Greater :: "[token, token] => bool" where
   15.12 +  "Greater x y =
   15.13      (x~=Leader & x~=id0 & y=id0) | (x=id4 & y~=id4 & y~=Leader) |
   15.14      (x=id2 & y=id1) | (x=id3 & y=id1) | (x=id3 & y=id2)"
   15.15  
    16.1 --- a/src/HOLCF/IOA/NTP/Correctness.thy	Sun Oct 21 14:21:45 2007 +0200
    16.2 +++ b/src/HOLCF/IOA/NTP/Correctness.thy	Sun Oct 21 14:21:48 2007 +0200
    16.3 @@ -9,10 +9,10 @@
    16.4  imports Impl Spec
    16.5  begin
    16.6  
    16.7 -constdefs
    16.8 -  hom :: "'m impl_state => 'm list"
    16.9 -  "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
   16.10 -                           else tl(sq(sen s)))"
   16.11 +definition
   16.12 +  hom :: "'m impl_state => 'm list" where
   16.13 +  "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
   16.14 +                         else tl(sq(sen s)))"
   16.15  
   16.16  ML_setup {*
   16.17  (* repeated from Traces.ML *)
    17.1 --- a/src/HOLCF/IOA/NTP/Packet.thy	Sun Oct 21 14:21:45 2007 +0200
    17.2 +++ b/src/HOLCF/IOA/NTP/Packet.thy	Sun Oct 21 14:21:48 2007 +0200
    17.3 @@ -10,12 +10,12 @@
    17.4  types
    17.5    'msg packet = "bool * 'msg"
    17.6  
    17.7 -constdefs
    17.8 -
    17.9 -  hdr  :: "'msg packet => bool"
   17.10 +definition
   17.11 +  hdr :: "'msg packet => bool" where
   17.12    "hdr == fst"
   17.13  
   17.14 -  msg :: "'msg packet => 'msg"
   17.15 +definition
   17.16 +  msg :: "'msg packet => 'msg" where
   17.17    "msg == snd"
   17.18  
   17.19  
    18.1 --- a/src/HOLCF/IOA/Storage/Correctness.thy	Sun Oct 21 14:21:45 2007 +0200
    18.2 +++ b/src/HOLCF/IOA/Storage/Correctness.thy	Sun Oct 21 14:21:48 2007 +0200
    18.3 @@ -11,13 +11,13 @@
    18.4  
    18.5  defaultsort type
    18.6  
    18.7 -constdefs
    18.8 -  sim_relation   :: "((nat * bool) * (nat set * bool)) set"
    18.9 -  "sim_relation == {qua. let c = fst qua; a = snd qua ;
   18.10 -                             k = fst c;   b = snd c;
   18.11 -                             used = fst a; c = snd a
   18.12 -                         in
   18.13 -                         (! l:used. l < k) & b=c }"
   18.14 +definition
   18.15 +  sim_relation :: "((nat * bool) * (nat set * bool)) set" where
   18.16 +  "sim_relation = {qua. let c = fst qua; a = snd qua ;
   18.17 +                            k = fst c;   b = snd c;
   18.18 +                            used = fst a; c = snd a
   18.19 +                        in
   18.20 +                        (! l:used. l < k) & b=c}"
   18.21  
   18.22  declare split_paired_All [simp]
   18.23  declare split_paired_Ex [simp del]
    19.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Sun Oct 21 14:21:45 2007 +0200
    19.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Sun Oct 21 14:21:48 2007 +0200
    19.3 @@ -68,23 +68,6 @@
    19.4    rename_set    :: "'a set => ('c => 'a option) => 'c set"
    19.5    rename        :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
    19.6  
    19.7 -
    19.8 -syntax
    19.9 -
   19.10 -  "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"  ("_ -_--_-> _" [81,81,81,81] 100)
   19.11 -  "act"        :: "('a,'s)ioa => 'a set"
   19.12 -  "ext"        :: "('a,'s)ioa => 'a set"
   19.13 -  "int"        :: "('a,'s)ioa => 'a set"
   19.14 -  "inp"        :: "('a,'s)ioa => 'a set"
   19.15 -  "out"        :: "('a,'s)ioa => 'a set"
   19.16 -  "local"      :: "('a,'s)ioa => 'a set"
   19.17 -
   19.18 -
   19.19 -syntax (xsymbols)
   19.20 -
   19.21 -  "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"
   19.22 -                  ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
   19.23 -
   19.24  notation (xsymbols)
   19.25    par  (infixr "\<parallel>" 10)
   19.26  
   19.27 @@ -96,15 +79,19 @@
   19.28      reachable_0:  "s : starts_of C ==> reachable C s"
   19.29    | reachable_n:  "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t"
   19.30  
   19.31 +abbreviation
   19.32 +  trans_of_syn  ("_ -_--_-> _" [81,81,81,81] 100) where
   19.33 +  "s -a--A-> t == (s,a,t):trans_of A"
   19.34  
   19.35 -translations
   19.36 -  "s -a--A-> t"   == "(s,a,t):trans_of A"
   19.37 -  "act A"         == "actions (asig_of A)"
   19.38 -  "ext A"         == "externals (asig_of A)"
   19.39 -  "int A"         == "internals (asig_of A)"
   19.40 -  "inp A"         == "inputs (asig_of A)"
   19.41 -  "out A"         == "outputs (asig_of A)"
   19.42 -  "local A"       == "locals (asig_of A)"
   19.43 +notation (xsymbols)
   19.44 +  trans_of_syn  ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
   19.45 +
   19.46 +abbreviation "act A == actions (asig_of A)"
   19.47 +abbreviation "ext A == externals (asig_of A)"
   19.48 +abbreviation int where "int A == internals (asig_of A)"
   19.49 +abbreviation "inp A == inputs (asig_of A)"
   19.50 +abbreviation "out A == outputs (asig_of A)"
   19.51 +abbreviation "local A == locals (asig_of A)"
   19.52  
   19.53  defs
   19.54  
    20.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Oct 21 14:21:45 2007 +0200
    20.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Oct 21 14:21:48 2007 +0200
    20.3 @@ -27,24 +27,23 @@
    20.4  
    20.5    Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"
    20.6  
    20.7 -syntax
    20.8 +abbreviation
    20.9 +  Consq_syn  ("(_/>>_)"  [66,65] 65) where
   20.10 +  "a>>s == Consq a$s"
   20.11  
   20.12 - "@Consq"         ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
   20.13 - (* list Enumeration *)
   20.14 -  "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
   20.15 -  "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
   20.16 +notation (xsymbols)
   20.17 +  Consq_syn  ("(_\<leadsto>_)"  [66,65] 65)
   20.18  
   20.19  
   20.20 -syntax (xsymbols)
   20.21 -  "@Consq"     ::"'a => 'a Seq => 'a Seq"       ("(_\<leadsto>_)"  [66,65] 65)
   20.22 -
   20.23 -
   20.24 +(* list Enumeration *)
   20.25 +syntax
   20.26 +  "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
   20.27 +  "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
   20.28  translations
   20.29 -  "a>>s"         == "Consq a$s"
   20.30    "[x, xs!]"     == "x>>[xs!]"
   20.31 -  "[x!]"         == "x>>nil"
   20.32 +  "[x!]"         == "x>>CONST nil"
   20.33    "[x, xs?]"     == "x>>[xs?]"
   20.34 -  "[x?]"         == "x>>UU"
   20.35 +  "[x?]"         == "x>>CONST UU"
   20.36  
   20.37  defs
   20.38  
    21.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Sun Oct 21 14:21:45 2007 +0200
    21.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sun Oct 21 14:21:48 2007 +0200
    21.3 @@ -30,10 +30,10 @@
    21.4  Next         ::"'a temporal => 'a temporal"
    21.5  Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)
    21.6  
    21.7 -syntax (xsymbols)
    21.8 -   "Box"        ::"'a temporal => 'a temporal"   ("\<box> (_)" [80] 80)
    21.9 -   "Diamond"    ::"'a temporal => 'a temporal"   ("\<diamond> (_)" [80] 80)
   21.10 -   "Leadsto"    ::"'a temporal => 'a temporal => 'a temporal"  (infixr "\<leadsto>" 22)
   21.11 +notation (xsymbols)
   21.12 +  Box  ("\<box> (_)" [80] 80) and
   21.13 +  Diamond  ("\<diamond> (_)" [80] 80) and
   21.14 +  Leadsto  (infixr "\<leadsto>" 22)
   21.15  
   21.16  defs
   21.17  
    22.1 --- a/src/HOLCF/Lift.thy	Sun Oct 21 14:21:45 2007 +0200
    22.2 +++ b/src/HOLCF/Lift.thy	Sun Oct 21 14:21:48 2007 +0200
    22.3 @@ -16,9 +16,9 @@
    22.4  
    22.5  lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
    22.6  
    22.7 -constdefs
    22.8 -  Def :: "'a \<Rightarrow> 'a lift"
    22.9 -  "Def x \<equiv> Abs_lift (up\<cdot>(Discr x))"
   22.10 +definition
   22.11 +  Def :: "'a \<Rightarrow> 'a lift" where
   22.12 +  "Def x = Abs_lift (up\<cdot>(Discr x))"
   22.13  
   22.14  subsection {* Lift as a datatype *}
   22.15  
   22.16 @@ -110,15 +110,17 @@
   22.17  
   22.18  subsection {* Further operations *}
   22.19  
   22.20 -constdefs
   22.21 -  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10)
   22.22 -  "flift1 \<equiv> \<lambda>f. (\<Lambda> x. lift_case \<bottom> f x)"
   22.23 +definition
   22.24 +  flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
   22.25 +  "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
   22.26  
   22.27 -  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)"
   22.28 -  "flift2 f \<equiv> FLIFT x. Def (f x)"
   22.29 +definition
   22.30 +  flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
   22.31 +  "flift2 f = (FLIFT x. Def (f x))"
   22.32  
   22.33 -  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift"
   22.34 -  "liftpair x \<equiv> csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
   22.35 +definition
   22.36 +  liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" where
   22.37 +  "liftpair x = csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
   22.38  
   22.39  subsection {* Continuity Proofs for flift1, flift2 *}
   22.40  
    23.1 --- a/src/HOLCF/One.thy	Sun Oct 21 14:21:45 2007 +0200
    23.2 +++ b/src/HOLCF/One.thy	Sun Oct 21 14:21:48 2007 +0200
    23.3 @@ -12,13 +12,12 @@
    23.4  begin
    23.5  
    23.6  types one = "unit lift"
    23.7 +translations
    23.8 +  "one" <= (type) "unit lift" 
    23.9  
   23.10  constdefs
   23.11    ONE :: "one"
   23.12 -  "ONE \<equiv> Def ()"
   23.13 -
   23.14 -translations
   23.15 -  "one" <= (type) "unit lift" 
   23.16 +  "ONE == Def ()"
   23.17  
   23.18  text {* Exhaustion and Elimination for type @{typ one} *}
   23.19  
   23.20 @@ -50,13 +49,13 @@
   23.21  
   23.22  text {* Case analysis function for type @{typ one} *}
   23.23  
   23.24 -constdefs
   23.25 -  one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a"
   23.26 -  "one_when \<equiv> \<Lambda> a. strictify\<cdot>(\<Lambda> _. a)"
   23.27 +definition
   23.28 +  one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
   23.29 +  "one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))"
   23.30  
   23.31  translations
   23.32 -  "case x of ONE \<Rightarrow> t" == "one_when\<cdot>t\<cdot>x"
   23.33 -  "\<Lambda> ONE. t" == "one_when\<cdot>t"
   23.34 +  "case x of CONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
   23.35 +  "\<Lambda> (CONST ONE). t" == "CONST one_when\<cdot>t"
   23.36  
   23.37  lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
   23.38  by (simp add: one_when_def)
    24.1 --- a/src/HOLCF/Pcpo.thy	Sun Oct 21 14:21:45 2007 +0200
    24.2 +++ b/src/HOLCF/Pcpo.thy	Sun Oct 21 14:21:48 2007 +0200
    24.3 @@ -171,12 +171,12 @@
    24.4  axclass pcpo < cpo
    24.5    least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
    24.6  
    24.7 -constdefs
    24.8 -  UU :: "'a::pcpo"
    24.9 -  "UU \<equiv> THE x. \<forall>y. x \<sqsubseteq> y"
   24.10 +definition
   24.11 +  UU :: "'a::pcpo" where
   24.12 +  "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
   24.13  
   24.14 -syntax (xsymbols)
   24.15 -  UU :: "'a::pcpo" ("\<bottom>")
   24.16 +notation (xsymbols)
   24.17 +  UU  ("\<bottom>")
   24.18  
   24.19  text {* derive the old rule minimal *}
   24.20   
    25.1 --- a/src/HOLCF/Porder.thy	Sun Oct 21 14:21:45 2007 +0200
    25.2 +++ b/src/HOLCF/Porder.thy	Sun Oct 21 14:21:48 2007 +0200
    25.3 @@ -22,7 +22,7 @@
    25.4  
    25.5  axclass po < sq_ord
    25.6    refl_less [iff]: "x \<sqsubseteq> x"
    25.7 -  antisym_less:    "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"    
    25.8 +  antisym_less:    "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
    25.9    trans_less:      "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
   25.10  
   25.11  text {* minimal fixes least element *}
   25.12 @@ -58,32 +58,38 @@
   25.13  
   25.14  subsection {* Chains and least upper bounds *}
   25.15  
   25.16 -constdefs  
   25.17 +text {* class definitions *}
   25.18  
   25.19 -  -- {* class definitions *}
   25.20 -  is_ub :: "['a set, 'a::po] \<Rightarrow> bool"       (infixl "<|" 55)
   25.21 -  "S <| x \<equiv> \<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x"
   25.22 +definition
   25.23 +  is_ub :: "['a set, 'a::po] \<Rightarrow> bool"  (infixl "<|" 55)  where
   25.24 +  "(S <| x) = (\<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x)"
   25.25  
   25.26 -  is_lub :: "['a set, 'a::po] \<Rightarrow> bool"       (infixl "<<|" 55)
   25.27 -  "S <<| x \<equiv> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
   25.28 +definition
   25.29 +  is_lub :: "['a set, 'a::po] \<Rightarrow> bool"  (infixl "<<|" 55)  where
   25.30 +  "(S <<| x) = (S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u))"
   25.31  
   25.32 +definition
   25.33    -- {* Arbitrary chains are total orders *}
   25.34 -  tord :: "'a::po set \<Rightarrow> bool"
   25.35 -  "tord S \<equiv> \<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
   25.36 +  tord :: "'a::po set \<Rightarrow> bool" where
   25.37 +  "tord S = (\<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x))"
   25.38  
   25.39 +definition
   25.40    -- {* Here we use countable chains and I prefer to code them as functions! *}
   25.41 -  chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
   25.42 -  "chain F \<equiv> \<forall>i. F i \<sqsubseteq> F (Suc i)"
   25.43 +  chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
   25.44 +  "chain F = (\<forall>i. F i \<sqsubseteq> F (Suc i))"
   25.45  
   25.46 +definition
   25.47    -- {* finite chains, needed for monotony of continuous functions *}
   25.48 -  max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool"
   25.49 -  "max_in_chain i C \<equiv> \<forall>j. i \<le> j \<longrightarrow> C i = C j" 
   25.50 +  max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool" where
   25.51 +  "max_in_chain i C = (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
   25.52  
   25.53 -  finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
   25.54 -  "finite_chain C \<equiv> chain(C) \<and> (\<exists>i. max_in_chain i C)"
   25.55 +definition
   25.56 +  finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
   25.57 +  "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
   25.58  
   25.59 -  lub :: "'a set \<Rightarrow> 'a::po"
   25.60 -  "lub S \<equiv> THE x. S <<| x"
   25.61 +definition
   25.62 +  lub :: "'a set \<Rightarrow> 'a::po" where
   25.63 +  "lub S = (THE x. S <<| x)"
   25.64  
   25.65  abbreviation
   25.66    Lub  (binder "LUB " 10) where
   25.67 @@ -124,8 +130,6 @@
   25.68  
   25.69  text {* technical lemmas about @{term lub} and @{term is_lub} *}
   25.70  
   25.71 -lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard]
   25.72 -
   25.73  lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
   25.74  apply (unfold lub_def)
   25.75  apply (rule theI)
   25.76 @@ -201,7 +205,7 @@
   25.77  apply (erule ub_rangeD)
   25.78  done
   25.79  
   25.80 -lemma lub_finch2: 
   25.81 +lemma lub_finch2:
   25.82          "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
   25.83  apply (unfold finite_chain_def)
   25.84  apply (erule conjE)
    26.1 --- a/src/HOLCF/Sprod.thy	Sun Oct 21 14:21:45 2007 +0200
    26.2 +++ b/src/HOLCF/Sprod.thy	Sun Oct 21 14:21:48 2007 +0200
    26.3 @@ -48,10 +48,10 @@
    26.4  
    26.5  translations
    26.6    "(:x, y, z:)" == "(:x, (:y, z:):)"
    26.7 -  "(:x, y:)"    == "spair\<cdot>x\<cdot>y"
    26.8 +  "(:x, y:)"    == "CONST spair\<cdot>x\<cdot>y"
    26.9  
   26.10  translations
   26.11 -  "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)"
   26.12 +  "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
   26.13  
   26.14  subsection {* Case analysis *}
   26.15  
    27.1 --- a/src/HOLCF/Ssum.thy	Sun Oct 21 14:21:45 2007 +0200
    27.2 +++ b/src/HOLCF/Ssum.thy	Sun Oct 21 14:21:48 2007 +0200
    27.3 @@ -27,12 +27,13 @@
    27.4  
    27.5  subsection {* Definitions of constructors *}
    27.6  
    27.7 -constdefs
    27.8 -  sinl :: "'a \<rightarrow> ('a ++ 'b)"
    27.9 -  "sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>"
   27.10 +definition
   27.11 +  sinl :: "'a \<rightarrow> ('a ++ 'b)" where
   27.12 +  "sinl = (\<Lambda> a. Abs_Ssum <a, \<bottom>>)"
   27.13  
   27.14 -  sinr :: "'b \<rightarrow> ('a ++ 'b)"
   27.15 -  "sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>"
   27.16 +definition
   27.17 +  sinr :: "'b \<rightarrow> ('a ++ 'b)" where
   27.18 +  "sinr = (\<Lambda> b. Abs_Ssum <\<bottom>, b>)"
   27.19  
   27.20  subsection {* Properties of @{term sinl} and @{term sinr} *}
   27.21  
   27.22 @@ -169,11 +170,11 @@
   27.23  
   27.24  subsection {* Definitions of constants *}
   27.25  
   27.26 -constdefs
   27.27 -  Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c"
   27.28 -  "Iwhen \<equiv> \<lambda>f g s.
   27.29 +definition
   27.30 +  Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c" where
   27.31 +  "Iwhen = (\<lambda>f g s.
   27.32      if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else
   27.33 -    if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>"
   27.34 +    if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>)"
   27.35  
   27.36  text {* rewrites for @{term Iwhen} *}
   27.37  
   27.38 @@ -213,16 +214,16 @@
   27.39  
   27.40  subsection {* Continuous versions of constants *}
   27.41  
   27.42 -constdefs
   27.43 -  sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
   27.44 -  "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
   27.45 +definition
   27.46 +  sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
   27.47 +  "sscase = (\<Lambda> f g s. Iwhen f g s)"
   27.48  
   27.49  translations
   27.50 -  "case s of sinl\<cdot>x \<Rightarrow> t1 | sinr\<cdot>y \<Rightarrow> t2" == "sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
   27.51 +  "case s of CONST sinl\<cdot>x \<Rightarrow> t1 | CONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
   27.52  
   27.53  translations
   27.54 -  "\<Lambda>(sinl\<cdot>x). t" == "sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
   27.55 -  "\<Lambda>(sinr\<cdot>y). t" == "sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
   27.56 +  "\<Lambda>(CONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
   27.57 +  "\<Lambda>(CONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
   27.58  
   27.59  text {* continuous versions of lemmas for @{term sscase} *}
   27.60  
    28.1 --- a/src/HOLCF/Tr.thy	Sun Oct 21 14:21:45 2007 +0200
    28.2 +++ b/src/HOLCF/Tr.thy	Sun Oct 21 14:21:48 2007 +0200
    28.3 @@ -28,17 +28,19 @@
    28.4    neg    :: "tr \<rightarrow> tr"
    28.5    If2    :: "[tr, 'c, 'c] \<Rightarrow> 'c"
    28.6  
    28.7 -syntax
    28.8 -  "@cifte"   :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60)
    28.9 -  "@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ andalso _" [36,35] 35)
   28.10 -  "@orelse"  :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ orelse _"  [31,30] 30)
   28.11 +abbreviation
   28.12 +  cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
   28.13 +  "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
   28.14 +
   28.15 +abbreviation
   28.16 +  andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ andalso _" [36,35] 35)  where
   28.17 +  "x andalso y == trand\<cdot>x\<cdot>y"
   28.18 +
   28.19 +abbreviation
   28.20 +  orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr"  ("_ orelse _"  [31,30] 30)  where
   28.21 +  "x orelse y == tror\<cdot>x\<cdot>y"
   28.22   
   28.23  translations
   28.24 -  "x andalso y" == "trand\<cdot>x\<cdot>y"
   28.25 -  "x orelse y"  == "tror\<cdot>x\<cdot>y"
   28.26 -  "If b then e1 else e2 fi" == "trifte\<cdot>e1\<cdot>e2\<cdot>b"
   28.27 -
   28.28 -translations
   28.29    "\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>"
   28.30    "\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t"
   28.31  
    29.1 --- a/src/HOLCF/Up.thy	Sun Oct 21 14:21:45 2007 +0200
    29.2 +++ b/src/HOLCF/Up.thy	Sun Oct 21 14:21:48 2007 +0200
    29.3 @@ -115,7 +115,7 @@
    29.4  by (rule ext, rule up_lemma3 [symmetric])
    29.5  
    29.6  lemma up_lemma6:
    29.7 -  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
    29.8 +  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
    29.9        \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
   29.10  apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
   29.11  apply assumption
   29.12 @@ -197,16 +197,17 @@
   29.13  
   29.14  subsection {* Continuous versions of constants *}
   29.15  
   29.16 -constdefs  
   29.17 -  up  :: "'a \<rightarrow> 'a u"
   29.18 -  "up \<equiv> \<Lambda> x. Iup x"
   29.19 +definition
   29.20 +  up  :: "'a \<rightarrow> 'a u" where
   29.21 +  "up = (\<Lambda> x. Iup x)"
   29.22  
   29.23 -  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
   29.24 -  "fup \<equiv> \<Lambda> f p. Ifup f p"
   29.25 +definition
   29.26 +  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
   29.27 +  "fup = (\<Lambda> f p. Ifup f p)"
   29.28  
   29.29  translations
   29.30 -  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   29.31 -  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
   29.32 +  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   29.33 +  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
   29.34  
   29.35  text {* continuous versions of lemmas for @{typ "('a)u"} *}
   29.36