--- a/src/HOLCF/FOCUS/Buffer.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy Fri Jun 02 19:41:37 2006 +0200
@@ -41,48 +41,50 @@
SPSF11 = "State \<Rightarrow> SPF11"
SPECS11 = "SPSF11 set"
-consts
+definition
BufEq_F :: "SPEC11 \<Rightarrow> SPEC11"
+ "BufEq_F B = {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and>
+ (\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}"
+
BufEq :: "SPEC11"
+ "BufEq = gfp BufEq_F"
+
BufEq_alt :: "SPEC11"
+ "BufEq_alt = gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and>
+ (\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})"
BufAC_Asm_F :: " (M fstream set) \<Rightarrow> (M fstream set)"
+ "BufAC_Asm_F A = {s. s = <> \<or>
+ (\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}"
+
BufAC_Asm :: " (M fstream set)"
+ "BufAC_Asm = gfp BufAC_Asm_F"
+
BufAC_Cmt_F :: "((M fstream * D fstream) set) \<Rightarrow>
((M fstream * D fstream) set)"
- BufAC_Cmt :: "((M fstream * D fstream) set)"
- BufAC :: "SPEC11"
-
- BufSt_F :: "SPECS11 \<Rightarrow> SPECS11"
- BufSt_P :: "SPECS11"
- BufSt :: "SPEC11"
-
-defs
-
- BufEq_F_def: "BufEq_F B \<equiv> {f. \<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and>
- (\<forall>x. \<exists>ff\<in>B. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x)}"
- BufEq_def: "BufEq \<equiv> gfp BufEq_F"
- BufEq_alt_def: "BufEq_alt \<equiv> gfp (\<lambda>B. {f. \<forall>d. f\<cdot>(Md d\<leadsto><> ) = <> \<and>
- (\<exists>ff\<in>B. (\<forall>x. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x))})"
- BufAC_Asm_F_def: "BufAC_Asm_F A \<equiv> {s. s = <> \<or>
- (\<exists>d x. s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>A)))}"
- BufAC_Asm_def: "BufAC_Asm \<equiv> gfp BufAC_Asm_F"
-
- BufAC_Cmt_F_def: "BufAC_Cmt_F C \<equiv> {(s,t). \<forall>d x.
+ "BufAC_Cmt_F C = {(s,t). \<forall>d x.
(s = <> \<longrightarrow> t = <> ) \<and>
(s = Md d\<leadsto><> \<longrightarrow> t = <> ) \<and>
(s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> (ft\<cdot>t = Def d \<and> (x,rt\<cdot>t)\<in>C))}"
- BufAC_Cmt_def: "BufAC_Cmt \<equiv> gfp BufAC_Cmt_F"
- BufAC_def: "BufAC \<equiv> {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}"
+
+ BufAC_Cmt :: "((M fstream * D fstream) set)"
+ "BufAC_Cmt = gfp BufAC_Cmt_F"
- BufSt_F_def: "BufSt_F H \<equiv> {h. \<forall>s . h s \<cdot><> = <> \<and>
+ BufAC :: "SPEC11"
+ "BufAC = {f. \<forall>x. x\<in>BufAC_Asm \<longrightarrow> (x,f\<cdot>x)\<in>BufAC_Cmt}"
+
+ BufSt_F :: "SPECS11 \<Rightarrow> SPECS11"
+ "BufSt_F H = {h. \<forall>s . h s \<cdot><> = <> \<and>
(\<forall>d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and>
(\<exists>hh\<in>H. h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency>\<cdot>x)))}"
- BufSt_P_def: "BufSt_P \<equiv> gfp BufSt_F"
- BufSt_def: "BufSt \<equiv> {f. \<exists>h\<in>BufSt_P. f = h \<currency>}"
+
+ BufSt_P :: "SPECS11"
+ "BufSt_P = gfp BufSt_F"
-ML {* use_legacy_bindings (the_context ()) *}
+ BufSt :: "SPEC11"
+ "BufSt = {f. \<exists>h\<in>BufSt_P. f = h \<currency>}"
+
lemma set_cong: "!!X. A = B ==> (x:A) = (x:B)"
by (erule subst, rule refl)
@@ -100,7 +102,7 @@
lemma mono_BufEq_F: "mono BufEq_F"
by (unfold mono_def BufEq_F_def, fast)
-lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN def_gfp_unfold]];
+lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN eq_reflection, THEN def_gfp_unfold]]
lemma BufEq_unfold: "(f:BufEq) = (!d. f\<cdot>(Md d\<leadsto><>) = <> &
(!x. ? ff:BufEq. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>(ff\<cdot>x)))"
@@ -125,7 +127,8 @@
lemma mono_BufAC_Asm_F: "mono BufAC_Asm_F"
by (unfold mono_def BufAC_Asm_F_def, fast)
-lemmas BufAC_Asm_fix = mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN def_gfp_unfold]]
+lemmas BufAC_Asm_fix =
+ mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN eq_reflection, THEN def_gfp_unfold]]
lemma BufAC_Asm_unfold: "(s:BufAC_Asm) = (s = <> | (? d x.
s = Md d\<leadsto>x & (x = <> | (ft\<cdot>x = Def \<bullet> & (rt\<cdot>x):BufAC_Asm))))"
@@ -150,7 +153,8 @@
lemma mono_BufAC_Cmt_F: "mono BufAC_Cmt_F"
by (unfold mono_def BufAC_Cmt_F_def, fast)
-lemmas BufAC_Cmt_fix = mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN def_gfp_unfold]]
+lemmas BufAC_Cmt_fix =
+ mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN eq_reflection, THEN def_gfp_unfold]]
lemma BufAC_Cmt_unfold: "((s,t):BufAC_Cmt) = (!d x.
(s = <> --> t = <>) &
@@ -225,7 +229,8 @@
lemma mono_BufSt_F: "mono BufSt_F"
by (unfold mono_def BufSt_F_def, fast)
-lemmas BufSt_P_fix = mono_BufSt_F [THEN BufSt_P_def [THEN def_gfp_unfold]]
+lemmas BufSt_P_fix =
+ mono_BufSt_F [THEN BufSt_P_def [THEN eq_reflection, THEN def_gfp_unfold]]
lemma BufSt_P_unfold: "(h:BufSt_P) = (!s. h s\<cdot><> = <> &
(!d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x &
--- a/src/HOLCF/FOCUS/Buffer_adm.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy Fri Jun 02 19:41:37 2006 +0200
@@ -235,7 +235,7 @@
lemma adm_BufAC_Asm: "adm (\<lambda>x. x\<in>BufAC_Asm)"
apply (rule def_gfp_admI)
-apply (rule BufAC_Asm_def)
+apply (rule BufAC_Asm_def [THEN eq_reflection])
apply (safe)
apply (unfold BufAC_Asm_F_def)
apply (safe)
@@ -269,7 +269,7 @@
lemma adm_non_BufAC_Asm': "adm (\<lambda>u. u \<notin> BufAC_Asm)" (* uses antitonP *)
apply (rule def_gfp_adm_nonP)
-apply (rule BufAC_Asm_def)
+apply (rule BufAC_Asm_def [THEN eq_reflection])
apply (unfold BufAC_Asm_F_def)
apply (safe)
apply (erule contrapos_np)
--- a/src/HOLCF/FOCUS/Fstream.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Fri Jun 02 19:41:37 2006 +0200
@@ -16,35 +16,27 @@
types 'a fstream = "'a lift stream"
-consts
-
+definition
fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
- fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+ "fscons a = (\<Lambda> s. Def a && s)"
-syntax
+ fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+ "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))"
- "@emptystream":: "'a fstream" ("<>")
- "@fscons" :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65)
- "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
-
-syntax (xsymbols)
+abbreviation
+ emptystream :: "'a fstream" ("<>")
+ "<> == \<bottom>"
- "@fscons" :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<leadsto>_)"
- [66,65] 65)
- "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)"
- [64,63] 63)
-translations
+ fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_~>_)" [66,65] 65)
+ "a~>s == fscons a\<cdot>s"
- "<>" => "\<bottom>"
- "a~>s" == "fscons a\<cdot>s"
- "A(C)s" == "fsfilter A\<cdot>s"
+ fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
+ "A(C)s == fsfilter A\<cdot>s"
-defs
+const_syntax (xsymbols)
+ fscons' ("(_\<leadsto>_)" [66,65] 65)
+ fsfilter' ("(_\<copyright>_)" [64,63] 63)
- fscons_def: "fscons a \<equiv> \<Lambda> s. Def a && s"
- fsfilter_def: "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
-
-ML {* use_legacy_bindings (the_context ()) *}
lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
apply (rule flat_eq [THEN iffD1, symmetric])
--- a/src/HOLCF/FOCUS/Fstreams.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy Fri Jun 02 19:41:37 2006 +0200
@@ -12,44 +12,35 @@
types 'a fstream = "('a lift) stream"
-consts
-
+definition
fsingleton :: "'a => 'a fstream" ("<_>" [1000] 999)
+ fsingleton_def2: "fsingleton = (%a. Def a && UU)"
+
fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
+ "fsfilter A = sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
+
fsmap :: "('a => 'b) => 'a fstream -> 'b fstream"
+ "fsmap f = smap$(flift2 f)"
jth :: "nat => 'a fstream => 'a"
+ "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary)"
first :: "'a fstream => 'a"
+ "first = (%s. jth 0 s)"
+
last :: "'a fstream => 'a"
+ "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
+ | Infty => arbitrary)"
-syntax
-
- "@emptystream":: "'a fstream" ("<>")
- "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
-
-syntax (xsymbols)
-
- "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)"
- [64,63] 63)
-translations
+abbreviation
+ emptystream :: "'a fstream" ("<>")
+ "<> == \<bottom>"
+ fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63)
+ "A(C)s == fsfilter A\<cdot>s"
- "<>" => "\<bottom>"
- "A(C)s" == "fsfilter A\<cdot>s"
-
-defs
-
- fsingleton_def2: "fsingleton == %a. Def a && UU"
-
- jth_def: "jth == %n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary"
-
- first_def: "first == %s. jth 0 s"
- last_def: "last == %s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
- | Infty => arbitrary"
-
- fsfilter_def: "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
- fsmap_def: "fsmap f == smap$(flift2 f)"
+const_syntax (xsymbols)
+ fsfilter' ("(_\<copyright>_)" [64,63] 63)
lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
--- a/src/HOLCF/FOCUS/Stream_adm.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Fri Jun 02 19:41:37 2006 +0200
@@ -9,22 +9,21 @@
imports Stream Continuity
begin
-constdefs
+definition
stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
- "stream_monoP F \<equiv> \<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
- (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P)"
+ "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
+ (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))"
stream_antiP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
- "stream_antiP F \<equiv> \<forall>P x. \<exists>Q i.
+ "stream_antiP F = (\<forall>P x. \<exists>Q i.
(#x < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
(Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
- (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P)))"
+ (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))"
antitonP :: "'a set => bool"
- "antitonP P \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P"
+ "antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)"
-ML {* use_legacy_bindings (the_context ()) *}
(* ----------------------------------------------------------------------- *)
--- a/src/HOLCF/ex/Dagstuhl.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Dagstuhl.thy Fri Jun 02 19:41:37 2006 +0200
@@ -7,16 +7,16 @@
consts
y :: "'a"
-constdefs
+definition
YS :: "'a stream"
- "YS == fix$(LAM x. y && x)"
+ "YS = fix$(LAM x. y && x)"
YYS :: "'a stream"
- "YYS == fix$(LAM z. y && y && z)"
+ "YYS = fix$(LAM z. y && y && z)"
lemma YS_def2: "YS = y && YS"
apply (rule trans)
apply (rule fix_eq2)
- apply (rule YS_def)
+ apply (rule YS_def [THEN eq_reflection])
apply (rule beta_cfun)
apply simp
done
@@ -24,14 +24,14 @@
lemma YYS_def2: "YYS = y && y && YYS"
apply (rule trans)
apply (rule fix_eq2)
- apply (rule YYS_def)
+ apply (rule YYS_def [THEN eq_reflection])
apply (rule beta_cfun)
apply simp
done
lemma lemma3: "YYS << y && YYS"
- apply (rule YYS_def [THEN def_fix_ind])
+ apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind])
apply simp_all
apply (rule monofun_cfun_arg)
apply (rule monofun_cfun_arg)
@@ -77,7 +77,7 @@
done
lemma lemma7: "YS << YYS"
- apply (rule YS_def [THEN def_fix_ind])
+ apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind])
apply simp_all
apply (subst lemma5 [symmetric])
apply (erule monofun_cfun_arg)
--- a/src/HOLCF/ex/Dnat.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Dnat.thy Fri Jun 02 19:41:37 2006 +0200
@@ -9,9 +9,9 @@
domain dnat = dzero | dsucc (dpred :: dnat)
-constdefs
+definition
iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
- "iterator == fix $ (LAM h n f x.
+ "iterator = fix $ (LAM h n f x.
case n of dzero => x
| dsucc $ m => f $ (h $ m $ f $ x))"
@@ -20,7 +20,7 @@
*}
ML_setup {*
-bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def")
+bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def" RS eq_reflection)
"iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))");
*}
--- a/src/HOLCF/ex/Focus_ex.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy Fri Jun 02 19:41:37 2006 +0200
@@ -108,33 +108,23 @@
arities tc:: (pcpo, pcpo) pcpo
consts
+ Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
-is_f ::
- "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
-is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
- 'b stream => 'c stream => bool"
-is_g :: "('b stream -> 'c stream) => bool"
-def_g :: "('b stream -> 'c stream) => bool"
-Rf ::
-"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
+definition
+ is_f :: "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
+ "is_f f = (!i1 i2 o1 o2. f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
-defs
-
-is_f: "is_f f == (!i1 i2 o1 o2.
- f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
-
-is_net_g: "is_net_g f x y == (? z.
+ is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
+ 'b stream => 'c stream => bool"
+ "is_net_g f x y == (? z.
<y,z> = f$<x,z> &
(!oy hz. <oy,hz> = f$<x,hz> --> z << hz))"
-is_g: "is_g g == (? f.
- is_f f &
- (!x y. g$x = y --> is_net_g f x y))"
+ is_g :: "('b stream -> 'c stream) => bool"
+ "is_g g == (? f. is_f f & (!x y. g$x = y --> is_net_g f x y))"
-
-def_g: "def_g g == (? f.
- is_f f &
- g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))"
+ def_g :: "('b stream -> 'c stream) => bool"
+ "def_g g == (? f. is_f f & g = (LAM x. cfst$(f$<x,fix$(LAM k. csnd$(f$<x,k>))>)))"
(* first some logical trading *)
@@ -143,7 +133,7 @@
"is_g(g) =
(? f. is_f(f) & (!x.(? z. <g$x,z> = f$<x,z> &
(! w y. <y,w> = f$<x,w> --> z << w))))"
-apply (simp add: is_g is_net_g)
+apply (simp add: is_g_def is_net_g_def)
apply fast
done
@@ -191,7 +181,7 @@
done
lemma lemma3: "def_g(g) --> is_g(g)"
-apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g", thm "lemma1", thm "lemma2"]) 1 *})
+apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *})
apply (rule impI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
@@ -218,7 +208,7 @@
lemma lemma4: "is_g(g) --> def_g(g)"
apply (tactic {* simp_tac (HOL_ss delsimps (thms "ex_simps" @ thms "all_simps")
- addsimps [thm "lemma1", thm "lemma2", thm "def_g"]) 1 *})
+ addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
apply (rule impI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
@@ -262,7 +252,7 @@
is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))
-->
(? g. def_g(g::'b stream -> 'c stream ))"
-apply (simp add: def_g)
+apply (simp add: def_g_def)
done
theorem conservative_loopback:
--- a/src/HOLCF/ex/Hoare.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Hoare.thy Fri Jun 02 19:41:37 2006 +0200
@@ -28,15 +28,13 @@
b1 :: "'a -> tr"
b2 :: "'a -> tr"
g :: "'a -> 'a"
- p :: "'a -> 'a"
- q :: "'a -> 'a"
-defs
- p_def: "p == fix$(LAM f. LAM x.
- If b1$x then f$(g$x) else x fi)"
+definition
+ p :: "'a -> 'a"
+ "p = fix$(LAM f. LAM x. If b1$x then f$(g$x) else x fi)"
- q_def: "q == fix$(LAM f. LAM x.
- If b1$x orelse b2$x then f$(g$x) else x fi)"
+ q :: "'a -> 'a"
+ "q = fix$(LAM f. LAM x. If b1$x orelse b2$x then f$(g$x) else x fi)"
(* --------- pure HOLCF logic, some little lemmas ------ *)
@@ -106,13 +104,13 @@
lemma p_def3: "p$x = If b1$x then p$(g$x) else x fi"
apply (rule trans)
-apply (rule p_def [THEN fix_eq3])
+apply (rule p_def [THEN eq_reflection, THEN fix_eq3])
apply simp
done
lemma q_def3: "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"
apply (rule trans)
-apply (rule q_def [THEN fix_eq3])
+apply (rule q_def [THEN eq_reflection, THEN fix_eq3])
apply simp
done
@@ -233,7 +231,7 @@
(* -------- results about p for case (ALL k. b1$(iterate k$g$x)=TT) ------- *)
lemma fernpass_lemma: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. p$(iterate k$g$x) = UU"
-apply (rule p_def [THEN def_fix_ind])
+apply (rule p_def [THEN eq_reflection, THEN def_fix_ind])
apply (rule adm_all)
apply (rule allI)
apply (rule adm_eq)
@@ -258,7 +256,7 @@
(* -------- results about q for case (ALL k. b1$(iterate k$g$x)=TT) ------- *)
lemma hoare_lemma17: "(ALL k. b1$(iterate k$g$x)=TT) ==> ALL k. q$(iterate k$g$x) = UU"
-apply (rule q_def [THEN def_fix_ind])
+apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
apply (rule adm_all)
apply (rule allI)
apply (rule adm_eq)
@@ -288,7 +286,7 @@
done
lemma hoare_lemma20: "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k$g$(x::'a)) = UU"
-apply (rule q_def [THEN def_fix_ind])
+apply (rule q_def [THEN eq_reflection, THEN def_fix_ind])
apply (rule adm_all)
apply (rule allI)
apply (rule adm_eq)
--- a/src/HOLCF/ex/Loop.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Loop.thy Fri Jun 02 19:41:37 2006 +0200
@@ -9,13 +9,12 @@
imports HOLCF
begin
-constdefs
+definition
step :: "('a -> tr)->('a -> 'a)->'a->'a"
- "step == (LAM b g x. If b$x then g$x else x fi)"
+ "step = (LAM b g x. If b$x then g$x else x fi)"
while :: "('a -> tr)->('a -> 'a)->'a->'a"
- "while == (LAM b g. fix$(LAM f x.
- If b$x then f$(g$x) else x fi))"
+ "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
(* ------------------------------------------------------------------------- *)
(* access to definitions *)
--- a/src/HOLCF/ex/Stream.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Stream.thy Fri Jun 02 19:41:37 2006 +0200
@@ -11,47 +11,45 @@
domain 'a stream = "&&" (ft::'a) (lazy rt::"'a stream") (infixr 65)
-consts
-
+definition
smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream"
- sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream"
- slen :: "'a stream \<Rightarrow> inat" ("#_" [1000] 1000)
+ "smap = fix\<cdot>(\<Lambda> h f s. case s of x && xs \<Rightarrow> f\<cdot>x && h\<cdot>f\<cdot>xs)"
-defs
+ sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream"
+ "sfilter = fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
+ If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
- smap_def: "smap \<equiv> fix\<cdot>(\<Lambda> h f s. case s of x && xs \<Rightarrow> f\<cdot>x && h\<cdot>f\<cdot>xs)"
- sfilter_def: "sfilter \<equiv> fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
- If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
- slen_def: "#s \<equiv> if stream_finite s
- then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>"
+ slen :: "'a stream \<Rightarrow> inat" ("#_" [1000] 1000)
+ "#s = (if stream_finite s then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
+
(* concatenation *)
-consts
+definition
+ i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *)
+ "i_rt = (%i s. iterate i$rt$s)"
- i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *)
i_th :: "nat => 'a stream => 'a" (* the i-th element *)
+ "i_th = (%i s. ft$(i_rt i s))"
sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65)
- constr_sconc :: "'a stream => 'a stream => 'a stream" (* constructive *)
- constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
-
-defs
- i_rt_def: "i_rt == %i s. iterate i$rt$s"
- i_th_def: "i_th == %i s. ft$(i_rt i s)"
+ "s1 ooo s2 = (case #s1 of
+ Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
+ | \<infinity> \<Rightarrow> s1)"
- sconc_def: "s1 ooo s2 == case #s1 of
- Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
- | \<infinity> \<Rightarrow> s1"
-
- constr_sconc_def: "constr_sconc s1 s2 == case #s1 of
- Fin n \<Rightarrow> constr_sconc' n s1 s2
- | \<infinity> \<Rightarrow> s1"
+consts
+ constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream"
primrec
constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2"
constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 &&
constr_sconc' n (rt$s1) s2"
+definition
+ constr_sconc :: "'a stream => 'a stream => 'a stream" (* constructive *)
+ "constr_sconc s1 s2 = (case #s1 of
+ Fin n \<Rightarrow> constr_sconc' n s1 s2
+ | \<infinity> \<Rightarrow> s1)"
+
declare stream.rews [simp add]
@@ -519,7 +517,7 @@
section "smap"
lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
-by (insert smap_def [THEN fix_eq2], auto)
+by (insert smap_def [THEN eq_reflection, THEN fix_eq2], auto)
lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
by (subst smap_unfold, simp)
@@ -538,7 +536,7 @@
lemma sfilter_unfold:
"sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
-by (insert sfilter_def [THEN fix_eq2], auto)
+by (insert sfilter_def [THEN eq_reflection, THEN fix_eq2], auto)
lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
apply (rule ext_cfun)