--- a/src/HOLCF/Adm.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Adm.thy Sun Oct 21 14:21:48 2007 +0200
@@ -13,12 +13,13 @@
subsection {* Definitions *}
-constdefs
- adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
- "adm P \<equiv> \<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i)"
+definition
+ adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
+ "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
- compact :: "'a::cpo \<Rightarrow> bool"
- "compact k \<equiv> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
+definition
+ compact :: "'a::cpo \<Rightarrow> bool" where
+ "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
lemma admI:
"(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
--- a/src/HOLCF/Cfun.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Cfun.thy Sun Oct 21 14:21:48 2007 +0200
@@ -28,14 +28,14 @@
syntax (xsymbols)
"->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)
-syntax
- Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_$/_)" [999,1000] 999)
+notation
+ Rep_CFun ("(_$/_)" [999,1000] 999)
-syntax (xsymbols)
- Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>/_)" [999,1000] 999)
+notation (xsymbols)
+ Rep_CFun ("(_\<cdot>/_)" [999,1000] 999)
-syntax (HTML output)
- Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>/_)" [999,1000] 999)
+notation (HTML output)
+ Rep_CFun ("(_\<cdot>/_)" [999,1000] 999)
subsection {* Syntax for continuous lambda abstraction *}
@@ -43,7 +43,7 @@
parse_translation {*
(* rewrites (_cabs x t) => (Abs_CFun (%x. t)) *)
- [mk_binder_tr ("_cabs", "Abs_CFun")];
+ [mk_binder_tr ("_cabs", @{const_syntax Abs_CFun})];
*}
text {* To avoid eta-contraction of body: *}
@@ -59,7 +59,7 @@
val (x,t') = atomic_abs_tr' abs';
in Syntax.const "_cabs" $ x $ t' end;
- in [("Abs_CFun", cabs_tr')] end;
+ in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
*}
text {* Syntax for nested abstractions *}
@@ -95,7 +95,7 @@
text {* Dummy patterns for continuous abstraction *}
translations
- "\<Lambda> _. t" => "Abs_CFun (\<lambda> _. t)"
+ "\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
subsection {* Continuous function space is pointed *}
@@ -439,9 +439,9 @@
ID :: "'a \<rightarrow> 'a"
cfcomp :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"
-syntax "@oo" :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100)
-
-translations "f oo g" == "cfcomp\<cdot>f\<cdot>g"
+abbreviation
+ cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100) where
+ "f oo g == cfcomp\<cdot>f\<cdot>g"
defs
ID_def: "ID \<equiv> (\<Lambda> x. x)"
@@ -481,9 +481,9 @@
defaultsort pcpo
-constdefs
- strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b"
- "strictify \<equiv> (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+definition
+ strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
+ "strictify = (\<Lambda> f x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
text {* results about strictify *}
@@ -526,15 +526,15 @@
subsection {* Continuous let-bindings *}
-constdefs
- CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
- "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
+definition
+ CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b" where
+ "CLet = (\<Lambda> s f. f\<cdot>s)"
syntax
"_CLet" :: "[letbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
translations
"_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
- "Let x = a in e" == "CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
+ "Let x = a in e" == "CONST CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
end
--- a/src/HOLCF/Cont.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Cont.thy Sun Oct 21 14:21:48 2007 +0200
@@ -20,15 +20,17 @@
subsection {* Definitions *}
-constdefs
- monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity"
- "monofun f \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
+definition
+ monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" -- "monotonicity" where
+ "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
- contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def"
- "contlub f \<equiv> \<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
+definition
+ contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "first cont. def" where
+ "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
- cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "secnd cont. def"
- "cont f \<equiv> \<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)"
+definition
+ cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" -- "secnd cont. def" where
+ "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))"
lemma contlubI:
"\<lbrakk>\<And>Y. chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))\<rbrakk> \<Longrightarrow> contlub f"
--- a/src/HOLCF/Cprod.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Cprod.thy Sun Oct 21 14:21:48 2007 +0200
@@ -29,12 +29,12 @@
instance unit :: pcpo
by intro_classes simp
-constdefs
- unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
- "unit_when \<equiv> \<Lambda> a _. a"
+definition
+ unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
+ "unit_when = (\<Lambda> a _. a)"
translations
- "\<Lambda>(). t" == "unit_when\<cdot>t"
+ "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
by (simp add: unit_when_def)
@@ -192,18 +192,21 @@
subsection {* Continuous versions of constants *}
-constdefs
- cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *)
- "cpair \<equiv> (\<Lambda> x y. (x, y))"
+definition
+ cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" -- {* continuous pairing *} where
+ "cpair = (\<Lambda> x y. (x, y))"
+
+definition
+ cfst :: "('a * 'b) \<rightarrow> 'a" where
+ "cfst = (\<Lambda> p. fst p)"
- cfst :: "('a * 'b) \<rightarrow> 'a"
- "cfst \<equiv> (\<Lambda> p. fst p)"
+definition
+ csnd :: "('a * 'b) \<rightarrow> 'b" where
+ "csnd = (\<Lambda> p. snd p)"
- csnd :: "('a * 'b) \<rightarrow> 'b"
- "csnd \<equiv> (\<Lambda> p. snd p)"
-
- csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c"
- "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
+definition
+ csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
+ "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
syntax
"_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(1<_,/ _>)")
@@ -213,10 +216,10 @@
translations
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
- "\<langle>x, y\<rangle>" == "cpair\<cdot>x\<cdot>y"
+ "\<langle>x, y\<rangle>" == "CONST cpair\<cdot>x\<cdot>y"
translations
- "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
+ "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
subsection {* Convert all lemmas to the continuous versions *}
--- a/src/HOLCF/Discrete.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Discrete.thy Sun Oct 21 14:21:48 2007 +0200
@@ -56,9 +56,9 @@
subsection {* @{term undiscr} *}
-constdefs
- undiscr :: "('a::type)discr => 'a"
- "undiscr x == (case x of Discr y => y)"
+definition
+ undiscr :: "('a::type)discr => 'a" where
+ "undiscr x = (case x of Discr y => y)"
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
by (simp add: undiscr_def)
--- a/src/HOLCF/Fix.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Fix.thy Sun Oct 21 14:21:48 2007 +0200
@@ -49,9 +49,9 @@
subsection {* Least fixed point operator *}
-constdefs
- "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a"
- "fix \<equiv> \<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>"
+definition
+ "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
+ "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
text {* Binder syntax for @{term fix} *}
@@ -62,7 +62,7 @@
"_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
translations
- "\<mu> x. t" == "fix\<cdot>(\<Lambda> x. t)"
+ "\<mu> x. t" == "CONST fix\<cdot>(\<Lambda> x. t)"
text {* Properties of @{term fix} *}
@@ -164,9 +164,9 @@
subsection {* Recursive let bindings *}
-constdefs
- CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b"
- "CLetrec \<equiv> \<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x)))"
+definition
+ CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
+ "CLetrec = (\<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x))))"
nonterminals
recbinds recbindt recbind
@@ -181,12 +181,12 @@
translations
(recbindt) "x = a, \<langle>y,ys\<rangle> = \<langle>b,bs\<rangle>" == (recbindt) "\<langle>x,y,ys\<rangle> = \<langle>a,b,bs\<rangle>"
- (recbindt) "x = a, y = b" == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
+ (recbindt) "x = a, y = b" == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
translations
"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
- "Letrec xs = a in \<langle>e,es\<rangle>" == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
- "Letrec xs = a in e" == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
+ "Letrec xs = a in \<langle>e,es\<rangle>" == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
+ "Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
text {*
Bekic's Theorem: Simultaneous fixed points over pairs
@@ -222,9 +222,9 @@
subsection {* Weak admissibility *}
-constdefs
- admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
- "admw P \<equiv> \<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
+definition
+ admw :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "admw P = (\<forall>F. (\<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)) \<longrightarrow> P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>))"
text {* an admissible formula is also weak admissible *}
--- a/src/HOLCF/Fixrec.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Fixrec.thy Sun Oct 21 14:21:48 2007 +0200
@@ -21,11 +21,13 @@
fail :: "'a maybe"
"fail \<equiv> Abs_maybe (sinl\<cdot>ONE)"
- return :: "'a \<rightarrow> 'a maybe"
+constdefs
+ return :: "'a \<rightarrow> 'a maybe" where
"return \<equiv> \<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x))"
- maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo"
- "maybe_when \<equiv> \<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m)"
+definition
+ maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo" where
+ "maybe_when = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m))"
lemma maybeE:
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
@@ -57,14 +59,14 @@
cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
translations
- "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
+ "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
subsubsection {* Monadic bind operator *}
-constdefs
- bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
- "bind \<equiv> \<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x"
+definition
+ bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" where
+ "bind = (\<Lambda> m f. case m of fail \<Rightarrow> fail | return\<cdot>x \<Rightarrow> f\<cdot>x)"
text {* monad laws *}
@@ -86,9 +88,9 @@
subsubsection {* Run operator *}
-constdefs
- run:: "'a maybe \<rightarrow> 'a::pcpo"
- "run \<equiv> maybe_when\<cdot>\<bottom>\<cdot>ID"
+definition
+ run:: "'a maybe \<rightarrow> 'a::pcpo" where
+ "run = maybe_when\<cdot>\<bottom>\<cdot>ID"
text {* rewrite rules for run *}
@@ -103,12 +105,13 @@
subsubsection {* Monad plus operator *}
-constdefs
- mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
- "mplus \<equiv> \<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1"
+definition
+ mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" where
+ "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | return\<cdot>x \<Rightarrow> m1)"
-syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
-translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
+abbreviation
+ mplus_syn :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65) where
+ "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2"
text {* rewrite rules for mplus *}
@@ -129,14 +132,13 @@
subsubsection {* Fatbar combinator *}
-constdefs
- fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
- "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
+definition
+ fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)" where
+ "fatbar = (\<Lambda> a b x. a\<cdot>x +++ b\<cdot>x)"
-syntax
- "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
-translations
- "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
+abbreviation
+ fatbar_syn :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60) where
+ "m1 \<parallel> m2 == fatbar\<cdot>m1\<cdot>m2"
lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
by (simp add: fatbar_def)
@@ -201,15 +203,15 @@
"_var" :: "'a"
translations
- "_Case1 p r" => "branch (_pat p)\<cdot>(_var p r)"
- "_var (_args x y) r" => "csplit\<cdot>(_var x (_var y r))"
- "_var () r" => "unit_when\<cdot>r"
+ "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
+ "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
+ "_var () r" => "CONST unit_when\<cdot>r"
parse_translation {*
(* rewrites (_pat x) => (return) *)
(* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
[("_pat", K (Syntax.const "Fixrec.return")),
- mk_binder_tr ("_var", "Abs_CFun")];
+ mk_binder_tr ("_var", @{const_syntax Abs_CFun})];
*}
text {* Printing Case expressions *}
@@ -219,14 +221,14 @@
print_translation {*
let
- fun dest_LAM (Const ("Rep_CFun",_) $ Const ("unit_when",_) $ t) =
- (Syntax.const "Unity", t)
- | dest_LAM (Const ("Rep_CFun",_) $ Const ("csplit",_) $ t) =
+ fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
+ (Syntax.const @{const_syntax Unity}, t)
+ | dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
let
val (v1, t1) = dest_LAM t;
val (v2, t2) = dest_LAM t1;
in (Syntax.const "_args" $ v1 $ v2, t2) end
- | dest_LAM (Const ("Abs_CFun",_) $ t) =
+ | dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
let
val abs = case t of Abs abs => abs
| _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
@@ -234,11 +236,11 @@
in (Syntax.const "_var" $ x, t') end
| dest_LAM _ = raise Match; (* too few vars: abort translation *)
- fun Case1_tr' [Const("branch",_) $ p, r] =
+ fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
let val (v, t) = dest_LAM r;
in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
- in [("Rep_CFun", Case1_tr')] end;
+ in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
*}
translations
@@ -249,67 +251,74 @@
types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
-constdefs
- cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat"
- "cpair_pat p1 p2 \<equiv> \<Lambda>\<langle>x, y\<rangle>.
- bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>))"
+definition
+ cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where
+ "cpair_pat p1 p2 = (\<Lambda>\<langle>x, y\<rangle>.
+ bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>)))"
+definition
spair_pat ::
- "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat"
- "spair_pat p1 p2 \<equiv> \<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>"
+ "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" where
+ "spair_pat p1 p2 = (\<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>)"
- sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
- "sinl_pat p \<equiv> sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
+definition
+ sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
+ "sinl_pat p = sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
- sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
- "sinr_pat p \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
+definition
+ sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" where
+ "sinr_pat p = sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
- up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat"
- "up_pat p \<equiv> fup\<cdot>p"
+definition
+ up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where
+ "up_pat p = fup\<cdot>p"
- TT_pat :: "(tr, unit) pat"
- "TT_pat \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
+definition
+ TT_pat :: "(tr, unit) pat" where
+ "TT_pat = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
- FF_pat :: "(tr, unit) pat"
- "FF_pat \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
+definition
+ FF_pat :: "(tr, unit) pat" where
+ "FF_pat = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
- ONE_pat :: "(one, unit) pat"
- "ONE_pat \<equiv> \<Lambda> ONE. return\<cdot>()"
+definition
+ ONE_pat :: "(one, unit) pat" where
+ "ONE_pat = (\<Lambda> ONE. return\<cdot>())"
text {* Parse translations (patterns) *}
translations
- "_pat (cpair\<cdot>x\<cdot>y)" => "cpair_pat (_pat x) (_pat y)"
- "_pat (spair\<cdot>x\<cdot>y)" => "spair_pat (_pat x) (_pat y)"
- "_pat (sinl\<cdot>x)" => "sinl_pat (_pat x)"
- "_pat (sinr\<cdot>x)" => "sinr_pat (_pat x)"
- "_pat (up\<cdot>x)" => "up_pat (_pat x)"
- "_pat TT" => "TT_pat"
- "_pat FF" => "FF_pat"
- "_pat ONE" => "ONE_pat"
+ "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
+ "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
+ "_pat (CONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
+ "_pat (CONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
+ "_pat (CONST up\<cdot>x)" => "CONST up_pat (_pat x)"
+ "_pat (CONST TT)" => "CONST TT_pat"
+ "_pat (CONST FF)" => "CONST FF_pat"
+ "_pat (CONST ONE)" => "CONST ONE_pat"
text {* Parse translations (variables) *}
translations
- "_var (cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
- "_var (spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
- "_var (sinl\<cdot>x) r" => "_var x r"
- "_var (sinr\<cdot>x) r" => "_var x r"
- "_var (up\<cdot>x) r" => "_var x r"
- "_var TT r" => "_var () r"
- "_var FF r" => "_var () r"
- "_var ONE r" => "_var () r"
+ "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+ "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+ "_var (CONST sinl\<cdot>x) r" => "_var x r"
+ "_var (CONST sinr\<cdot>x) r" => "_var x r"
+ "_var (CONST up\<cdot>x) r" => "_var x r"
+ "_var (CONST TT) r" => "_var () r"
+ "_var (CONST FF) r" => "_var () r"
+ "_var (CONST ONE) r" => "_var () r"
text {* Print translations *}
translations
- "cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
- <= "_match (cpair_pat p1 p2) (_args v1 v2)"
- "spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
- <= "_match (spair_pat p1 p2) (_args v1 v2)"
- "sinl\<cdot>(_match p1 v1)" <= "_match (sinl_pat p1) v1"
- "sinr\<cdot>(_match p1 v1)" <= "_match (sinr_pat p1) v1"
- "up\<cdot>(_match p1 v1)" <= "_match (up_pat p1) v1"
- "TT" <= "_match TT_pat ()"
- "FF" <= "_match FF_pat ()"
- "ONE" <= "_match ONE_pat ()"
+ "CONST cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
+ <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
+ "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
+ <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"
+ "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
+ "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
+ "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
+ "CONST TT" <= "_match (CONST TT_pat) ()"
+ "CONST FF" <= "_match (CONST FF_pat) ()"
+ "CONST ONE" <= "_match (CONST ONE_pat) ()"
lemma cpair_pat1:
"branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
@@ -382,21 +391,23 @@
"_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
"_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
-constdefs
- wild_pat :: "'a \<rightarrow> unit maybe"
- "wild_pat \<equiv> \<Lambda> x. return\<cdot>()"
+definition
+ wild_pat :: "'a \<rightarrow> unit maybe" where
+ "wild_pat = (\<Lambda> x. return\<cdot>())"
- as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe"
- "as_pat p \<equiv> \<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>)"
+definition
+ as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" where
+ "as_pat p = (\<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>))"
- lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)"
- "lazy_pat p \<equiv> \<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x))"
+definition
+ lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
+ "lazy_pat p = (\<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x)))"
text {* Parse translations (patterns) *}
translations
- "_pat _" => "wild_pat"
- "_pat (_as_pat x y)" => "as_pat (_pat y)"
- "_pat (_lazy_pat x)" => "lazy_pat (_pat x)"
+ "_pat _" => "CONST wild_pat"
+ "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
+ "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
text {* Parse translations (variables) *}
translations
@@ -406,13 +417,13 @@
text {* Print translations *}
translations
- "_" <= "_match wild_pat ()"
- "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
- "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
+ "_" <= "_match (CONST wild_pat) ()"
+ "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
+ "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
text {* Lazy patterns in lambda abstractions *}
translations
- "_cabs (_lazy_pat p) r" == "run oo (_Case1 (_lazy_pat p) r)"
+ "_cabs (_lazy_pat p) r" == "CONST run oo (_Case1 (_lazy_pat p) r)"
lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
by (simp add: branch_def wild_pat_def)
@@ -436,33 +447,41 @@
defaultsort pcpo
-constdefs
- match_UU :: "'a \<rightarrow> unit maybe"
- "match_UU \<equiv> \<Lambda> x. fail"
+definition
+ match_UU :: "'a \<rightarrow> unit maybe" where
+ "match_UU = (\<Lambda> x. fail)"
+
+definition
+ match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe" where
+ "match_cpair = csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
- match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
- "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
+definition
+ match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe" where
+ "match_spair = ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
- match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
- "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
-
- match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
- "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
+definition
+ match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe" where
+ "match_sinl = sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
- match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
- "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
+definition
+ match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe" where
+ "match_sinr = sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
- match_up :: "'a::cpo u \<rightarrow> 'a maybe"
- "match_up \<equiv> fup\<cdot>return"
+definition
+ match_up :: "'a::cpo u \<rightarrow> 'a maybe" where
+ "match_up = fup\<cdot>return"
- match_ONE :: "one \<rightarrow> unit maybe"
- "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
+definition
+ match_ONE :: "one \<rightarrow> unit maybe" where
+ "match_ONE = (\<Lambda> ONE. return\<cdot>())"
- match_TT :: "tr \<rightarrow> unit maybe"
- "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
+definition
+ match_TT :: "tr \<rightarrow> unit maybe" where
+ "match_TT = (\<Lambda> b. If b then return\<cdot>() else fail fi)"
- match_FF :: "tr \<rightarrow> unit maybe"
- "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
+definition
+ match_FF :: "tr \<rightarrow> unit maybe" where
+ "match_FF = (\<Lambda> b. If b then fail else return\<cdot>() fi)"
lemma match_UU_simps [simp]:
"match_UU\<cdot>x = fail"
@@ -532,13 +551,6 @@
lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
by simp
-ML {*
-val cpair_equalI = thm "cpair_equalI";
-val cpair_eqD1 = thm "cpair_eqD1";
-val cpair_eqD2 = thm "cpair_eqD2";
-val ssubst_lhs = thm "ssubst_lhs";
-val branch_def = thm "branch_def";
-*}
subsection {* Initializing the fixrec package *}
--- a/src/HOLCF/IOA/ABP/Correctness.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Sun Oct 21 14:21:48 2007 +0200
@@ -20,22 +20,23 @@
then reduce xs
else (x#(reduce xs))))"
-constdefs
+definition
abs where
- "abs ==
+ "abs =
(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
(reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
- system_ioa :: "('m action, bool * 'm impl_state)ioa"
- "system_ioa == (env_ioa || impl_ioa)"
+definition
+ system_ioa :: "('m action, bool * 'm impl_state)ioa" where
+ "system_ioa = (env_ioa || impl_ioa)"
- system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
- "system_fin_ioa == (env_ioa || impl_fin_ioa)"
+definition
+ system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" where
+ "system_fin_ioa = (env_ioa || impl_fin_ioa)"
-axioms
-
- sys_IOA: "IOA system_ioa"
+axiomatization where
+ sys_IOA: "IOA system_ioa" and
sys_fin_IOA: "IOA system_fin_ioa"
--- a/src/HOLCF/IOA/ABP/Env.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Env.thy Sun Oct 21 14:21:48 2007 +0200
@@ -12,30 +12,32 @@
types
'm env_state = bool -- {* give next bit to system *}
-constdefs
-env_asig :: "'m action signature"
-"env_asig == ({Next},
- UN m. {S_msg(m)},
- {})"
+definition
+ env_asig :: "'m action signature" where
+ "env_asig == ({Next},
+ UN m. {S_msg(m)},
+ {})"
-env_trans :: "('m action, 'm env_state)transition set"
-"env_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- Next => t=True |
- S_msg(m) => s=True & t=False |
- R_msg(m) => False |
- S_pkt(pkt) => False |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => False}"
+definition
+ env_trans :: "('m action, 'm env_state)transition set" where
+ "env_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ Next => t=True |
+ S_msg(m) => s=True & t=False |
+ R_msg(m) => False |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False}"
-env_ioa :: "('m action, 'm env_state)ioa"
-"env_ioa == (env_asig, {True}, env_trans,{},{})"
+definition
+ env_ioa :: "('m action, 'm env_state)ioa" where
+ "env_ioa = (env_asig, {True}, env_trans,{},{})"
-consts
- "next" :: "'m env_state => bool"
+axiomatization
+ "next" :: "'m env_state => bool"
end
--- a/src/HOLCF/IOA/ABP/Impl.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Impl.thy Sun Oct 21 14:21:48 2007 +0200
@@ -13,21 +13,24 @@
'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
(* sender_state * receiver_state * srch_state * rsch_state *)
-constdefs
+definition
+ impl_ioa :: "('m action, 'm impl_state)ioa" where
+ "impl_ioa = (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
- impl_ioa :: "('m action, 'm impl_state)ioa"
- "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
-
- sen :: "'m impl_state => 'm sender_state"
- "sen == fst"
+definition
+ sen :: "'m impl_state => 'm sender_state" where
+ "sen = fst"
- rec :: "'m impl_state => 'm receiver_state"
- "rec == fst o snd"
+definition
+ rec :: "'m impl_state => 'm receiver_state" where
+ "rec = fst o snd"
- srch :: "'m impl_state => 'm packet list"
- "srch == fst o snd o snd"
+definition
+ srch :: "'m impl_state => 'm packet list" where
+ "srch = fst o snd o snd"
- rsch :: "'m impl_state => bool list"
- "rsch == snd o snd o snd"
+definition
+ rsch :: "'m impl_state => bool list" where
+ "rsch = snd o snd o snd"
end
--- a/src/HOLCF/IOA/ABP/Impl_finite.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Impl_finite.thy Sun Oct 21 14:21:48 2007 +0200
@@ -14,22 +14,25 @@
= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
(* sender_state * receiver_state * srch_state * rsch_state *)
-constdefs
+definition
+ impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
+ "impl_fin_ioa = (sender_ioa || receiver_ioa || srch_fin_ioa ||
+ rsch_fin_ioa)"
- impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa"
- "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
- rsch_fin_ioa)"
-
- sen_fin :: "'m impl_fin_state => 'm sender_state"
- "sen_fin == fst"
+definition
+ sen_fin :: "'m impl_fin_state => 'm sender_state" where
+ "sen_fin = fst"
- rec_fin :: "'m impl_fin_state => 'm receiver_state"
- "rec_fin == fst o snd"
+definition
+ rec_fin :: "'m impl_fin_state => 'm receiver_state" where
+ "rec_fin = fst o snd"
- srch_fin :: "'m impl_fin_state => 'm packet list"
- "srch_fin == fst o snd o snd"
+definition
+ srch_fin :: "'m impl_fin_state => 'm packet list" where
+ "srch_fin = fst o snd o snd"
- rsch_fin :: "'m impl_fin_state => bool list"
- "rsch_fin == snd o snd o snd"
+definition
+ rsch_fin :: "'m impl_fin_state => bool list" where
+ "rsch_fin = snd o snd o snd"
end
--- a/src/HOLCF/IOA/ABP/Packet.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Packet.thy Sun Oct 21 14:21:48 2007 +0200
@@ -12,11 +12,12 @@
types
'msg packet = "bool * 'msg"
-constdefs
- hdr :: "'msg packet => bool"
- "hdr == fst"
+definition
+ hdr :: "'msg packet => bool" where
+ "hdr = fst"
- msg :: "'msg packet => 'msg"
- "msg == snd"
+definition
+ msg :: "'msg packet => 'msg" where
+ "msg = snd"
end
--- a/src/HOLCF/IOA/ABP/Receiver.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Receiver.thy Sun Oct 21 14:21:48 2007 +0200
@@ -12,43 +12,47 @@
types
'm receiver_state = "'m list * bool" -- {* messages, mode *}
-constdefs
- rq :: "'m receiver_state => 'm list"
- "rq == fst"
+definition
+ rq :: "'m receiver_state => 'm list" where
+ "rq = fst"
- rbit :: "'m receiver_state => bool"
- "rbit == snd"
+definition
+ rbit :: "'m receiver_state => bool" where
+ "rbit = snd"
-receiver_asig :: "'m action signature"
-"receiver_asig ==
- (UN pkt. {R_pkt(pkt)},
- (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
- {})"
+definition
+ receiver_asig :: "'m action signature" where
+ "receiver_asig =
+ (UN pkt. {R_pkt(pkt)},
+ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
+ {})"
-receiver_trans :: "('m action, 'm receiver_state)transition set"
-"receiver_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of
- Next => False |
- S_msg(m) => False |
- R_msg(m) => (rq(s) ~= []) &
- m = hd(rq(s)) &
- rq(t) = tl(rq(s)) &
- rbit(t)=rbit(s) |
- S_pkt(pkt) => False |
- R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
- rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
- rq(t) =rq(s) & rbit(t)=rbit(s) |
- S_ack(b) => b = rbit(s) &
- rq(t) = rq(s) &
- rbit(t)=rbit(s) |
- R_ack(b) => False}"
+definition
+ receiver_trans :: "('m action, 'm receiver_state)transition set" where
+ "receiver_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ Next => False |
+ S_msg(m) => False |
+ R_msg(m) => (rq(s) ~= []) &
+ m = hd(rq(s)) &
+ rq(t) = tl(rq(s)) &
+ rbit(t)=rbit(s) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
+ rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
+ rq(t) =rq(s) & rbit(t)=rbit(s) |
+ S_ack(b) => b = rbit(s) &
+ rq(t) = rq(s) &
+ rbit(t)=rbit(s) |
+ R_ack(b) => False}"
-receiver_ioa :: "('m action, 'm receiver_state)ioa"
-"receiver_ioa ==
- (receiver_asig, {([],False)}, receiver_trans,{},{})"
+definition
+ receiver_ioa :: "('m action, 'm receiver_state)ioa" where
+ "receiver_ioa =
+ (receiver_asig, {([],False)}, receiver_trans,{},{})"
end
--- a/src/HOLCF/IOA/ABP/Sender.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Sender.thy Sun Oct 21 14:21:48 2007 +0200
@@ -12,41 +12,45 @@
types
'm sender_state = "'m list * bool" -- {* messages, Alternating Bit *}
-constdefs
-sq :: "'m sender_state => 'm list"
-"sq == fst"
+definition
+ sq :: "'m sender_state => 'm list" where
+ "sq = fst"
-sbit :: "'m sender_state => bool"
-"sbit == snd"
+definition
+ sbit :: "'m sender_state => bool" where
+ "sbit = snd"
-sender_asig :: "'m action signature"
-"sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
- UN pkt. {S_pkt(pkt)},
- {})"
+definition
+ sender_asig :: "'m action signature" where
+ "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
+ UN pkt. {S_pkt(pkt)},
+ {})"
-sender_trans :: "('m action, 'm sender_state)transition set"
-"sender_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- Next => if sq(s)=[] then t=s else False |
- S_msg(m) => sq(t)=sq(s)@[m] &
- sbit(t)=sbit(s) |
- R_msg(m) => False |
- S_pkt(pkt) => sq(s) ~= [] &
- hdr(pkt) = sbit(s) &
- msg(pkt) = hd(sq(s)) &
- sq(t) = sq(s) &
- sbit(t) = sbit(s) |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => if b = sbit(s) then
- sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
- sq(t)=sq(s) & sbit(t)=sbit(s)}"
-
-sender_ioa :: "('m action, 'm sender_state)ioa"
-"sender_ioa ==
- (sender_asig, {([],True)}, sender_trans,{},{})"
+definition
+ sender_trans :: "('m action, 'm sender_state)transition set" where
+ "sender_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ Next => if sq(s)=[] then t=s else False |
+ S_msg(m) => sq(t)=sq(s)@[m] &
+ sbit(t)=sbit(s) |
+ R_msg(m) => False |
+ S_pkt(pkt) => sq(s) ~= [] &
+ hdr(pkt) = sbit(s) &
+ msg(pkt) = hd(sq(s)) &
+ sq(t) = sq(s) &
+ sbit(t) = sbit(s) |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => if b = sbit(s) then
+ sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
+ sq(t)=sq(s) & sbit(t)=sbit(s)}"
+
+definition
+ sender_ioa :: "('m action, 'm sender_state)ioa" where
+ "sender_ioa =
+ (sender_asig, {([],True)}, sender_trans,{},{})"
end
--- a/src/HOLCF/IOA/Modelcheck/Ring3.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy Sun Oct 21 14:21:48 2007 +0200
@@ -11,9 +11,9 @@
Zero_One token | One_Two token | Two_Zero token |
Leader_Zero | Leader_One | Leader_Two
-constdefs
- Greater :: "[token, token] => bool"
- "Greater x y ==
+definition
+ Greater :: "[token, token] => bool" where
+ "Greater x y =
(x~=Leader & x~=id0 & y=id0) | (x=id4 & y~=id4 & y~=Leader) |
(x=id2 & y=id1) | (x=id3 & y=id1) | (x=id3 & y=id2)"
--- a/src/HOLCF/IOA/NTP/Correctness.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.thy Sun Oct 21 14:21:48 2007 +0200
@@ -9,10 +9,10 @@
imports Impl Spec
begin
-constdefs
- hom :: "'m impl_state => 'm list"
- "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
- else tl(sq(sen s)))"
+definition
+ hom :: "'m impl_state => 'm list" where
+ "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
+ else tl(sq(sen s)))"
ML_setup {*
(* repeated from Traces.ML *)
--- a/src/HOLCF/IOA/NTP/Packet.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Packet.thy Sun Oct 21 14:21:48 2007 +0200
@@ -10,12 +10,12 @@
types
'msg packet = "bool * 'msg"
-constdefs
-
- hdr :: "'msg packet => bool"
+definition
+ hdr :: "'msg packet => bool" where
"hdr == fst"
- msg :: "'msg packet => 'msg"
+definition
+ msg :: "'msg packet => 'msg" where
"msg == snd"
--- a/src/HOLCF/IOA/Storage/Correctness.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.thy Sun Oct 21 14:21:48 2007 +0200
@@ -11,13 +11,13 @@
defaultsort type
-constdefs
- sim_relation :: "((nat * bool) * (nat set * bool)) set"
- "sim_relation == {qua. let c = fst qua; a = snd qua ;
- k = fst c; b = snd c;
- used = fst a; c = snd a
- in
- (! l:used. l < k) & b=c }"
+definition
+ sim_relation :: "((nat * bool) * (nat set * bool)) set" where
+ "sim_relation = {qua. let c = fst qua; a = snd qua ;
+ k = fst c; b = snd c;
+ used = fst a; c = snd a
+ in
+ (! l:used. l < k) & b=c}"
declare split_paired_All [simp]
declare split_paired_Ex [simp del]
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Sun Oct 21 14:21:48 2007 +0200
@@ -68,23 +68,6 @@
rename_set :: "'a set => ('c => 'a option) => 'c set"
rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
-
-syntax
-
- "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" ("_ -_--_-> _" [81,81,81,81] 100)
- "act" :: "('a,'s)ioa => 'a set"
- "ext" :: "('a,'s)ioa => 'a set"
- "int" :: "('a,'s)ioa => 'a set"
- "inp" :: "('a,'s)ioa => 'a set"
- "out" :: "('a,'s)ioa => 'a set"
- "local" :: "('a,'s)ioa => 'a set"
-
-
-syntax (xsymbols)
-
- "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool"
- ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
-
notation (xsymbols)
par (infixr "\<parallel>" 10)
@@ -96,15 +79,19 @@
reachable_0: "s : starts_of C ==> reachable C s"
| reachable_n: "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t"
+abbreviation
+ trans_of_syn ("_ -_--_-> _" [81,81,81,81] 100) where
+ "s -a--A-> t == (s,a,t):trans_of A"
-translations
- "s -a--A-> t" == "(s,a,t):trans_of A"
- "act A" == "actions (asig_of A)"
- "ext A" == "externals (asig_of A)"
- "int A" == "internals (asig_of A)"
- "inp A" == "inputs (asig_of A)"
- "out A" == "outputs (asig_of A)"
- "local A" == "locals (asig_of A)"
+notation (xsymbols)
+ trans_of_syn ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
+
+abbreviation "act A == actions (asig_of A)"
+abbreviation "ext A == externals (asig_of A)"
+abbreviation int where "int A == internals (asig_of A)"
+abbreviation "inp A == inputs (asig_of A)"
+abbreviation "out A == outputs (asig_of A)"
+abbreviation "local A == locals (asig_of A)"
defs
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sun Oct 21 14:21:48 2007 +0200
@@ -27,24 +27,23 @@
Filter2 ::"('a => bool) => 'a Seq -> 'a Seq"
-syntax
+abbreviation
+ Consq_syn ("(_/>>_)" [66,65] 65) where
+ "a>>s == Consq a$s"
- "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_/>>_)" [66,65] 65)
- (* list Enumeration *)
- "_totlist" :: "args => 'a Seq" ("[(_)!]")
- "_partlist" :: "args => 'a Seq" ("[(_)?]")
+notation (xsymbols)
+ Consq_syn ("(_\<leadsto>_)" [66,65] 65)
-syntax (xsymbols)
- "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_\<leadsto>_)" [66,65] 65)
-
-
+(* list Enumeration *)
+syntax
+ "_totlist" :: "args => 'a Seq" ("[(_)!]")
+ "_partlist" :: "args => 'a Seq" ("[(_)?]")
translations
- "a>>s" == "Consq a$s"
"[x, xs!]" == "x>>[xs!]"
- "[x!]" == "x>>nil"
+ "[x!]" == "x>>CONST nil"
"[x, xs?]" == "x>>[xs?]"
- "[x?]" == "x>>UU"
+ "[x?]" == "x>>CONST UU"
defs
--- a/src/HOLCF/IOA/meta_theory/TL.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Sun Oct 21 14:21:48 2007 +0200
@@ -30,10 +30,10 @@
Next ::"'a temporal => 'a temporal"
Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22)
-syntax (xsymbols)
- "Box" ::"'a temporal => 'a temporal" ("\<box> (_)" [80] 80)
- "Diamond" ::"'a temporal => 'a temporal" ("\<diamond> (_)" [80] 80)
- "Leadsto" ::"'a temporal => 'a temporal => 'a temporal" (infixr "\<leadsto>" 22)
+notation (xsymbols)
+ Box ("\<box> (_)" [80] 80) and
+ Diamond ("\<diamond> (_)" [80] 80) and
+ Leadsto (infixr "\<leadsto>" 22)
defs
--- a/src/HOLCF/Lift.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Lift.thy Sun Oct 21 14:21:48 2007 +0200
@@ -16,9 +16,9 @@
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
-constdefs
- Def :: "'a \<Rightarrow> 'a lift"
- "Def x \<equiv> Abs_lift (up\<cdot>(Discr x))"
+definition
+ Def :: "'a \<Rightarrow> 'a lift" where
+ "Def x = Abs_lift (up\<cdot>(Discr x))"
subsection {* Lift as a datatype *}
@@ -110,15 +110,17 @@
subsection {* Further operations *}
-constdefs
- flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10)
- "flift1 \<equiv> \<lambda>f. (\<Lambda> x. lift_case \<bottom> f x)"
+definition
+ flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where
+ "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
- flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)"
- "flift2 f \<equiv> FLIFT x. Def (f x)"
+definition
+ flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where
+ "flift2 f = (FLIFT x. Def (f x))"
- liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift"
- "liftpair x \<equiv> csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
+definition
+ liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" where
+ "liftpair x = csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x"
subsection {* Continuity Proofs for flift1, flift2 *}
--- a/src/HOLCF/One.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/One.thy Sun Oct 21 14:21:48 2007 +0200
@@ -12,13 +12,12 @@
begin
types one = "unit lift"
+translations
+ "one" <= (type) "unit lift"
constdefs
ONE :: "one"
- "ONE \<equiv> Def ()"
-
-translations
- "one" <= (type) "unit lift"
+ "ONE == Def ()"
text {* Exhaustion and Elimination for type @{typ one} *}
@@ -50,13 +49,13 @@
text {* Case analysis function for type @{typ one} *}
-constdefs
- one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a"
- "one_when \<equiv> \<Lambda> a. strictify\<cdot>(\<Lambda> _. a)"
+definition
+ one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
+ "one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))"
translations
- "case x of ONE \<Rightarrow> t" == "one_when\<cdot>t\<cdot>x"
- "\<Lambda> ONE. t" == "one_when\<cdot>t"
+ "case x of CONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
+ "\<Lambda> (CONST ONE). t" == "CONST one_when\<cdot>t"
lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
by (simp add: one_when_def)
--- a/src/HOLCF/Pcpo.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Pcpo.thy Sun Oct 21 14:21:48 2007 +0200
@@ -171,12 +171,12 @@
axclass pcpo < cpo
least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
-constdefs
- UU :: "'a::pcpo"
- "UU \<equiv> THE x. \<forall>y. x \<sqsubseteq> y"
+definition
+ UU :: "'a::pcpo" where
+ "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
-syntax (xsymbols)
- UU :: "'a::pcpo" ("\<bottom>")
+notation (xsymbols)
+ UU ("\<bottom>")
text {* derive the old rule minimal *}
--- a/src/HOLCF/Porder.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Porder.thy Sun Oct 21 14:21:48 2007 +0200
@@ -22,7 +22,7 @@
axclass po < sq_ord
refl_less [iff]: "x \<sqsubseteq> x"
- antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
+ antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
text {* minimal fixes least element *}
@@ -58,32 +58,38 @@
subsection {* Chains and least upper bounds *}
-constdefs
+text {* class definitions *}
- -- {* class definitions *}
- is_ub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<|" 55)
- "S <| x \<equiv> \<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x"
+definition
+ is_ub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<|" 55) where
+ "(S <| x) = (\<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x)"
- is_lub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<<|" 55)
- "S <<| x \<equiv> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
+definition
+ is_lub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<<|" 55) where
+ "(S <<| x) = (S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u))"
+definition
-- {* Arbitrary chains are total orders *}
- tord :: "'a::po set \<Rightarrow> bool"
- "tord S \<equiv> \<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
+ tord :: "'a::po set \<Rightarrow> bool" where
+ "tord S = (\<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x))"
+definition
-- {* Here we use countable chains and I prefer to code them as functions! *}
- chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
- "chain F \<equiv> \<forall>i. F i \<sqsubseteq> F (Suc i)"
+ chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
+ "chain F = (\<forall>i. F i \<sqsubseteq> F (Suc i))"
+definition
-- {* finite chains, needed for monotony of continuous functions *}
- max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool"
- "max_in_chain i C \<equiv> \<forall>j. i \<le> j \<longrightarrow> C i = C j"
+ max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool" where
+ "max_in_chain i C = (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
- finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
- "finite_chain C \<equiv> chain(C) \<and> (\<exists>i. max_in_chain i C)"
+definition
+ finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
+ "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
- lub :: "'a set \<Rightarrow> 'a::po"
- "lub S \<equiv> THE x. S <<| x"
+definition
+ lub :: "'a set \<Rightarrow> 'a::po" where
+ "lub S = (THE x. S <<| x)"
abbreviation
Lub (binder "LUB " 10) where
@@ -124,8 +130,6 @@
text {* technical lemmas about @{term lub} and @{term is_lub} *}
-lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard]
-
lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
apply (unfold lub_def)
apply (rule theI)
@@ -201,7 +205,7 @@
apply (erule ub_rangeD)
done
-lemma lub_finch2:
+lemma lub_finch2:
"finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
apply (unfold finite_chain_def)
apply (erule conjE)
--- a/src/HOLCF/Sprod.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Sprod.thy Sun Oct 21 14:21:48 2007 +0200
@@ -48,10 +48,10 @@
translations
"(:x, y, z:)" == "(:x, (:y, z:):)"
- "(:x, y:)" == "spair\<cdot>x\<cdot>y"
+ "(:x, y:)" == "CONST spair\<cdot>x\<cdot>y"
translations
- "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)"
+ "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
subsection {* Case analysis *}
--- a/src/HOLCF/Ssum.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Ssum.thy Sun Oct 21 14:21:48 2007 +0200
@@ -27,12 +27,13 @@
subsection {* Definitions of constructors *}
-constdefs
- sinl :: "'a \<rightarrow> ('a ++ 'b)"
- "sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>"
+definition
+ sinl :: "'a \<rightarrow> ('a ++ 'b)" where
+ "sinl = (\<Lambda> a. Abs_Ssum <a, \<bottom>>)"
- sinr :: "'b \<rightarrow> ('a ++ 'b)"
- "sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>"
+definition
+ sinr :: "'b \<rightarrow> ('a ++ 'b)" where
+ "sinr = (\<Lambda> b. Abs_Ssum <\<bottom>, b>)"
subsection {* Properties of @{term sinl} and @{term sinr} *}
@@ -169,11 +170,11 @@
subsection {* Definitions of constants *}
-constdefs
- Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c"
- "Iwhen \<equiv> \<lambda>f g s.
+definition
+ Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c" where
+ "Iwhen = (\<lambda>f g s.
if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else
- if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>"
+ if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>)"
text {* rewrites for @{term Iwhen} *}
@@ -213,16 +214,16 @@
subsection {* Continuous versions of constants *}
-constdefs
- sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
- "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
+definition
+ sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
+ "sscase = (\<Lambda> f g s. Iwhen f g s)"
translations
- "case s of sinl\<cdot>x \<Rightarrow> t1 | sinr\<cdot>y \<Rightarrow> t2" == "sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+ "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"
translations
- "\<Lambda>(sinl\<cdot>x). t" == "sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
- "\<Lambda>(sinr\<cdot>y). t" == "sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
+ "\<Lambda>(CONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
+ "\<Lambda>(CONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
text {* continuous versions of lemmas for @{term sscase} *}
--- a/src/HOLCF/Tr.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Tr.thy Sun Oct 21 14:21:48 2007 +0200
@@ -28,17 +28,19 @@
neg :: "tr \<rightarrow> tr"
If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c"
-syntax
- "@cifte" :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60)
- "@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35)
- "@orelse" :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30)
+abbreviation
+ cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) where
+ "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
+
+abbreviation
+ andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where
+ "x andalso y == trand\<cdot>x\<cdot>y"
+
+abbreviation
+ orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where
+ "x orelse y == tror\<cdot>x\<cdot>y"
translations
- "x andalso y" == "trand\<cdot>x\<cdot>y"
- "x orelse y" == "tror\<cdot>x\<cdot>y"
- "If b then e1 else e2 fi" == "trifte\<cdot>e1\<cdot>e2\<cdot>b"
-
-translations
"\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>"
"\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t"
--- a/src/HOLCF/Up.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/Up.thy Sun Oct 21 14:21:48 2007 +0200
@@ -115,7 +115,7 @@
by (rule ext, rule up_lemma3 [symmetric])
lemma up_lemma6:
- "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
+ "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
\<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
apply assumption
@@ -197,16 +197,17 @@
subsection {* Continuous versions of constants *}
-constdefs
- up :: "'a \<rightarrow> 'a u"
- "up \<equiv> \<Lambda> x. Iup x"
+definition
+ up :: "'a \<rightarrow> 'a u" where
+ "up = (\<Lambda> x. Iup x)"
- fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
- "fup \<equiv> \<Lambda> f p. Ifup f p"
+definition
+ fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
+ "fup = (\<Lambda> f p. Ifup f p)"
translations
- "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
- "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
+ "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+ "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
text {* continuous versions of lemmas for @{typ "('a)u"} *}