# HG changeset patch # User huffman # Date 1274728224 25200 # Node ID 7ffdbc24b27ff8e22f9eb6da992a467c26edb17d # Parent e67760c1b851c3911c2e9fd8b01f04593f15c1f2 move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Mon May 24 11:29:49 2010 -0700 +++ b/src/HOLCF/FOCUS/Fstream.thy Mon May 24 12:10:24 2010 -0700 @@ -9,7 +9,7 @@ header {* FOCUS flat streams *} theory Fstream -imports "../ex/Stream" +imports Stream begin default_sort type diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/FOCUS/Fstreams.thy --- a/src/HOLCF/FOCUS/Fstreams.thy Mon May 24 11:29:49 2010 -0700 +++ b/src/HOLCF/FOCUS/Fstreams.thy Mon May 24 12:10:24 2010 -0700 @@ -6,7 +6,9 @@ TODO: integrate this with Fstream. *) -theory Fstreams imports "../ex/Stream" begin +theory Fstreams +imports Stream +begin default_sort type diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOLCF/FOCUS/Stream_adm.thy Mon May 24 11:29:49 2010 -0700 +++ b/src/HOLCF/FOCUS/Stream_adm.thy Mon May 24 12:10:24 2010 -0700 @@ -5,7 +5,7 @@ header {* Admissibility for streams *} theory Stream_adm -imports "../ex/Stream" Continuity +imports Stream Continuity begin definition diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/HOLCF.thy --- a/src/HOLCF/HOLCF.thy Mon May 24 11:29:49 2010 -0700 +++ b/src/HOLCF/HOLCF.thy Mon May 24 12:10:24 2010 -0700 @@ -14,6 +14,8 @@ default_sort pcpo +ML {* path_add "~~/src/HOLCF/Library" *} + text {* Legacy theorem names *} lemmas sq_ord_less_eq_trans = below_eq_trans diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Mon May 24 11:29:49 2010 -0700 +++ b/src/HOLCF/IsaMakefile Mon May 24 12:10:24 2010 -0700 @@ -7,6 +7,7 @@ default: HOLCF images: HOLCF IOA test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \ + HOLCF-Library \ HOLCF-Tutorial \ IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex all: images test @@ -92,6 +93,18 @@ @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial +## HOLCF-Library + +HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz + +$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ + Library/Stream.thy \ + Library/Strict_Fun.thy \ + Library/HOLCF_Library.thy \ + Library/ROOT.ML + @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library + + ## HOLCF-IMP HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz @@ -117,8 +130,6 @@ ex/Loop.thy \ ex/Pattern_Match.thy \ ex/Powerdomain_ex.thy \ - ex/Stream.thy \ - ex/Strict_Fun.thy \ ex/ROOT.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex @@ -128,7 +139,7 @@ HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \ - ex/Stream.thy \ + Library/Stream.thy \ FOCUS/Fstreams.thy \ FOCUS/Fstream.thy FOCUS/FOCUS.thy \ FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ @@ -213,4 +224,5 @@ $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz \ + $(LOG)/HOLCF-Library.gz \ $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/Library/HOLCF_Library.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Library/HOLCF_Library.thy Mon May 24 12:10:24 2010 -0700 @@ -0,0 +1,7 @@ +theory HOLCF_Library +imports + Stream + Strict_Fun +begin + +end diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/Library/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Library/ROOT.ML Mon May 24 12:10:24 2010 -0700 @@ -0,0 +1,1 @@ +use_thys ["HOLCF_Library"]; diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/Library/Stream.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Library/Stream.thy Mon May 24 12:10:24 2010 -0700 @@ -0,0 +1,965 @@ +(* Title: HOLCF/ex/Stream.thy + Author: Franz Regensburger, David von Oheimb, Borislav Gajanovic +*) + +header {* General Stream domain *} + +theory Stream +imports HOLCF Nat_Infinity +begin + +domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65) + +definition + smap :: "('a \ 'b) \ 'a stream \ 'b stream" where + "smap = fix\(\ h f s. case s of x && xs \ f\x && h\f\xs)" + +definition + sfilter :: "('a \ tr) \ 'a stream \ 'a stream" where + "sfilter = fix\(\ h p s. case s of x && xs \ + If p\x then x && h\p\xs else h\p\xs fi)" + +definition + slen :: "'a stream \ inat" ("#_" [1000] 1000) where + "#s = (if stream_finite s then Fin (LEAST n. stream_take n\s = s) else \)" + + +(* concatenation *) + +definition + i_rt :: "nat => 'a stream => 'a stream" where (* chops the first i elements *) + "i_rt = (%i s. iterate i$rt$s)" + +definition + i_th :: "nat => 'a stream => 'a" where (* the i-th element *) + "i_th = (%i s. ft$(i_rt i s))" + +definition + sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where + "s1 ooo s2 = (case #s1 of + Fin n \ (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) + | \ \ s1)" + +primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" +where + 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" where (* constructive *) + "constr_sconc s1 s2 = (case #s1 of + Fin n \ constr_sconc' n s1 s2 + | \ \ s1)" + + +(* ----------------------------------------------------------------------- *) +(* theorems about scons *) +(* ----------------------------------------------------------------------- *) + + +section "scons" + +lemma scons_eq_UU: "(a && s = UU) = (a = UU)" +by simp + +lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R" +by simp + +lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)" +by (cases x, auto) + +lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU" +by (simp add: stream_exhaust_eq,auto) + +lemma stream_prefix: + "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt" +by (cases t, auto) + +lemma stream_prefix': + "b ~= UU ==> x << b && z = + (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))" +by (cases x, auto) + + +(* +lemma stream_prefix1: "[| x< x&&xs << y&&ys" +by (insert stream_prefix' [of y "x&&xs" ys],force) +*) + +lemma stream_flat_prefix: + "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" +apply (case_tac "y=UU",auto) +by (drule ax_flat,simp) + + + + +(* ----------------------------------------------------------------------- *) +(* theorems about stream_when *) +(* ----------------------------------------------------------------------- *) + +section "stream_when" + + +lemma stream_when_strictf: "stream_when$UU$s=UU" +by (cases s, auto) + + + +(* ----------------------------------------------------------------------- *) +(* theorems about ft and rt *) +(* ----------------------------------------------------------------------- *) + + +section "ft & rt" + + +lemma ft_defin: "s~=UU ==> ft$s~=UU" +by simp + +lemma rt_strict_rev: "rt$s~=UU ==> s~=UU" +by auto + +lemma surjectiv_scons: "(ft$s)&&(rt$s)=s" +by (cases s, auto) + +lemma monofun_rt_mult: "x << s ==> iterate i$rt$x << iterate i$rt$s" +by (rule monofun_cfun_arg) + + + +(* ----------------------------------------------------------------------- *) +(* theorems about stream_take *) +(* ----------------------------------------------------------------------- *) + + +section "stream_take" + + +lemma stream_reach2: "(LUB i. stream_take i$s) = s" +by (rule stream.reach) + +lemma chain_stream_take: "chain (%i. stream_take i$s)" +by simp + +lemma stream_take_prefix [simp]: "stream_take n$s << s" +apply (insert stream_reach2 [of s]) +apply (erule subst) back +apply (rule is_ub_thelub) +by (simp only: chain_stream_take) + +lemma stream_take_more [rule_format]: + "ALL x. stream_take n$x = x --> stream_take (Suc n)$x = x" +apply (induct_tac n,auto) +apply (case_tac "x=UU",auto) +by (drule stream_exhaust_eq [THEN iffD1],auto) + +lemma stream_take_lemma3 [rule_format]: + "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs" +apply (induct_tac n,clarsimp) +(*apply (drule sym, erule scons_not_empty, simp)*) +apply (clarify, rule stream_take_more) +apply (erule_tac x="x" in allE) +by (erule_tac x="xs" in allE,simp) + +lemma stream_take_lemma4: + "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs" +by auto + +lemma stream_take_idempotent [rule_format, simp]: + "ALL s. stream_take n$(stream_take n$s) = stream_take n$s" +apply (induct_tac n, auto) +apply (case_tac "s=UU", auto) +by (drule stream_exhaust_eq [THEN iffD1], auto) + +lemma stream_take_take_Suc [rule_format, simp]: + "ALL s. stream_take n$(stream_take (Suc n)$s) = + stream_take n$s" +apply (induct_tac n, auto) +apply (case_tac "s=UU", auto) +by (drule stream_exhaust_eq [THEN iffD1], auto) + +lemma mono_stream_take_pred: + "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> + stream_take n$s1 << stream_take n$s2" +by (insert monofun_cfun_arg [of "stream_take (Suc n)$s1" + "stream_take (Suc n)$s2" "stream_take n"], auto) +(* +lemma mono_stream_take_pred: + "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> + stream_take n$s1 << stream_take n$s2" +by (drule mono_stream_take [of _ _ n],simp) +*) + +lemma stream_take_lemma10 [rule_format]: + "ALL k<=n. stream_take n$s1 << stream_take n$s2 + --> stream_take k$s1 << stream_take k$s2" +apply (induct_tac n,simp,clarsimp) +apply (case_tac "k=Suc n",blast) +apply (erule_tac x="k" in allE) +by (drule mono_stream_take_pred,simp) + +lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1" +apply (insert chain_stream_take [of s1]) +by (drule chain_mono,auto) + +lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2" +by (simp add: monofun_cfun_arg) + +(* +lemma stream_take_prefix [simp]: "stream_take n$s << s" +apply (subgoal_tac "s=(LUB n. stream_take n$s)") + apply (erule ssubst, rule is_ub_thelub) + apply (simp only: chain_stream_take) +by (simp only: stream_reach2) +*) + +lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s" +by (rule monofun_cfun_arg,auto) + + +(* ------------------------------------------------------------------------- *) +(* special induction rules *) +(* ------------------------------------------------------------------------- *) + + +section "induction" + +lemma stream_finite_ind: + "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x" +apply (simp add: stream.finite_def,auto) +apply (erule subst) +by (drule stream.finite_induct [of P _ x], auto) + +lemma stream_finite_ind2: +"[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==> + !s. P (stream_take n$s)" +apply (rule nat_less_induct [of _ n],auto) +apply (case_tac n, auto) +apply (case_tac nat, auto) +apply (case_tac "s=UU",clarsimp) +apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) +apply (case_tac "s=UU",clarsimp) +apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) +apply (case_tac "y=UU",clarsimp) +by (drule stream_exhaust_eq [THEN iffD1],clarsimp) + +lemma stream_ind2: +"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x" +apply (insert stream.reach [of x],erule subst) +apply (erule admD, rule chain_stream_take) +apply (insert stream_finite_ind2 [of P]) +by simp + + + +(* ----------------------------------------------------------------------- *) +(* simplify use of coinduction *) +(* ----------------------------------------------------------------------- *) + + +section "coinduction" + +lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R" + apply (simp add: stream.bisim_def,clarsimp) + apply (drule spec, drule spec, drule (1) mp) + apply (case_tac "x", simp) + apply (case_tac "x'", simp) +by auto + + + +(* ----------------------------------------------------------------------- *) +(* theorems about stream_finite *) +(* ----------------------------------------------------------------------- *) + + +section "stream_finite" + +lemma stream_finite_UU [simp]: "stream_finite UU" +by (simp add: stream.finite_def) + +lemma stream_finite_UU_rev: "~ stream_finite s ==> s ~= UU" +by (auto simp add: stream.finite_def) + +lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)" +apply (simp add: stream.finite_def,auto) +apply (rule_tac x="Suc n" in exI) +by (simp add: stream_take_lemma4) + +lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" +apply (simp add: stream.finite_def, auto) +apply (rule_tac x="n" in exI) +by (erule stream_take_lemma3,simp) + +lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s" +apply (cases s, auto) +apply (rule stream_finite_lemma1, simp) +by (rule stream_finite_lemma2,simp) + +lemma stream_finite_less: "stream_finite s ==> !t. t< stream_finite t" +apply (erule stream_finite_ind [of s], auto) +apply (case_tac "t=UU", auto) +apply (drule stream_exhaust_eq [THEN iffD1],auto) +apply (erule_tac x="y" in allE, simp) +by (rule stream_finite_lemma1, simp) + +lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)" +apply (simp add: stream.finite_def) +by (rule_tac x="n" in exI,simp) + +lemma adm_not_stream_finite: "adm (%x. ~ stream_finite x)" +apply (rule adm_upward) +apply (erule contrapos_nn) +apply (erule (1) stream_finite_less [rule_format]) +done + + + +(* ----------------------------------------------------------------------- *) +(* theorems about stream length *) +(* ----------------------------------------------------------------------- *) + + +section "slen" + +lemma slen_empty [simp]: "#\ = 0" +by (simp add: slen_def stream.finite_def zero_inat_def Least_equality) + +lemma slen_scons [simp]: "x ~= \ ==> #(x&&xs) = iSuc (#xs)" +apply (case_tac "stream_finite (x && xs)") +apply (simp add: slen_def, auto) +apply (simp add: stream.finite_def, auto simp add: iSuc_Fin) +apply (rule Least_Suc2, auto) +(*apply (drule sym)*) +(*apply (drule sym scons_eq_UU [THEN iffD1],simp)*) +apply (erule stream_finite_lemma2, simp) +apply (simp add: slen_def, auto) +by (drule stream_finite_lemma1,auto) + +lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \)" +by (cases x, auto simp add: Fin_0 iSuc_Fin[THEN sym]) + +lemma slen_empty_eq: "(#x = 0) = (x = \)" +by (cases x, auto) + +lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \ & Fin n < #y)" +apply (auto, case_tac "x=UU",auto) +apply (drule stream_exhaust_eq [THEN iffD1], auto) +apply (case_tac "#y") apply simp_all +apply (case_tac "#y") apply simp_all +done + +lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y & a ~= \ & #y = n)" +by (cases x, auto) + +lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \" +by (simp add: slen_def) + +lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \ | #y < Fin (Suc n))" + apply (cases x, auto) + apply (simp add: zero_inat_def) + apply (case_tac "#stream") apply (simp_all add: iSuc_Fin) + apply (case_tac "#stream") apply (simp_all add: iSuc_Fin) +done + +lemma slen_take_lemma4 [rule_format]: + "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n" +apply (induct n, auto simp add: Fin_0) +apply (case_tac "s=UU", simp) +by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_Fin) + +(* +lemma stream_take_idempotent [simp]: + "stream_take n$(stream_take n$s) = stream_take n$s" +apply (case_tac "stream_take n$s = s") +apply (auto,insert slen_take_lemma4 [of n s]); +by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp) + +lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) = + stream_take n$s" +apply (simp add: po_eq_conv,auto) + apply (simp add: stream_take_take_less) +apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)") + apply (erule ssubst) + apply (rule_tac monofun_cfun_arg) + apply (insert chain_stream_take [of s]) +by (simp add: chain_def,simp) +*) + +lemma slen_take_eq: "ALL x. (Fin n < #x) = (stream_take n\x ~= x)" +apply (induct_tac n, auto) +apply (simp add: Fin_0, clarsimp) +apply (drule not_sym) +apply (drule slen_empty_eq [THEN iffD1], simp) +apply (case_tac "x=UU", simp) +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) +apply (erule_tac x="y" in allE, auto) +apply (simp_all add: not_less iSuc_Fin) +apply (case_tac "#y") apply simp_all +apply (case_tac "x=UU", simp) +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) +apply (erule_tac x="y" in allE, simp) +apply (case_tac "#y") by simp_all + +lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\x = x)" +by (simp add: linorder_not_less [symmetric] slen_take_eq) + +lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\x = x" +by (rule slen_take_eq_rev [THEN iffD1], auto) + +lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)" +apply (cases s1) + by (cases s2, simp+)+ + +lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n" +apply (case_tac "stream_take n$s = s") + apply (simp add: slen_take_eq_rev) +by (simp add: slen_take_lemma4) + +lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\x) = Fin i" +apply (simp add: stream.finite_def, auto) +by (simp add: slen_take_lemma4) + +lemma slen_infinite: "stream_finite x = (#x ~= Infty)" +by (simp add: slen_def) + +lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t" +apply (erule stream_finite_ind [of s], auto) +apply (case_tac "t=UU", auto) +apply (drule stream_exhaust_eq [THEN iffD1], auto) +done + +lemma slen_mono: "s << t ==> #s <= #t" +apply (case_tac "stream_finite t") +apply (frule stream_finite_less) +apply (erule_tac x="s" in allE, simp) +apply (drule slen_mono_lemma, auto) +by (simp add: slen_def) + +lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)" +by (insert iterate_Suc2 [of n F x], auto) + +lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)" +apply (induct i, auto) +apply (case_tac "x=UU", auto simp add: zero_inat_def) +apply (drule stream_exhaust_eq [THEN iffD1], auto) +apply (erule_tac x="y" in allE, auto) +apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin) +by (simp add: iterate_lemma) + +lemma slen_take_lemma3 [rule_format]: + "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\x = stream_take n\y" +apply (induct_tac n, auto) +apply (case_tac "x=UU", auto) +apply (simp add: zero_inat_def) +apply (simp add: Suc_ile_eq) +apply (case_tac "y=UU", clarsimp) +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ +apply (erule_tac x="ya" in allE, simp) +by (drule ax_flat, simp) + +lemma slen_strict_mono_lemma: + "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t" +apply (erule stream_finite_ind, auto) +apply (case_tac "sa=UU", auto) +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) +by (drule ax_flat, simp) + +lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t" +by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma) + +lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==> + stream_take n$s ~= stream_take (Suc n)$s" +apply auto +apply (subgoal_tac "stream_take n$s ~=s") + apply (insert slen_take_lemma4 [of n s],auto) +apply (cases s, simp) +by (simp add: slen_take_lemma4 iSuc_Fin) + +(* ----------------------------------------------------------------------- *) +(* theorems about smap *) +(* ----------------------------------------------------------------------- *) + + +section "smap" + +lemma smap_unfold: "smap = (\ f t. case t of x&&xs \ f$x && smap$f$xs)" +by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto) + +lemma smap_empty [simp]: "smap\f\\ = \" +by (subst smap_unfold, simp) + +lemma smap_scons [simp]: "x~=\ ==> smap\f\(x&&xs) = (f\x)&&(smap\f\xs)" +by (subst smap_unfold, force) + + + +(* ----------------------------------------------------------------------- *) +(* theorems about sfilter *) +(* ----------------------------------------------------------------------- *) + +section "sfilter" + +lemma sfilter_unfold: + "sfilter = (\ p s. case s of x && xs \ + If p\x then x && sfilter\p\xs else sfilter\p\xs fi)" +by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto) + +lemma strict_sfilter: "sfilter\\ = \" +apply (rule ext_cfun) +apply (subst sfilter_unfold, auto) +apply (case_tac "x=UU", auto) +by (drule stream_exhaust_eq [THEN iffD1], auto) + +lemma sfilter_empty [simp]: "sfilter\f\\ = \" +by (subst sfilter_unfold, force) + +lemma sfilter_scons [simp]: + "x ~= \ ==> sfilter\f\(x && xs) = + If f\x then x && sfilter\f\xs else sfilter\f\xs fi" +by (subst sfilter_unfold, force) + + +(* ----------------------------------------------------------------------- *) + section "i_rt" +(* ----------------------------------------------------------------------- *) + +lemma i_rt_UU [simp]: "i_rt n UU = UU" + by (induct n) (simp_all add: i_rt_def) + +lemma i_rt_0 [simp]: "i_rt 0 s = s" +by (simp add: i_rt_def) + +lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s" +by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc) + +lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)" +by (simp only: i_rt_def iterate_Suc2) + +lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)" +by (simp only: i_rt_def,auto) + +lemma i_rt_mono: "x << s ==> i_rt n x << i_rt n s" +by (simp add: i_rt_def monofun_rt_mult) + +lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)" +by (simp add: i_rt_def slen_rt_mult) + +lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)" +apply (induct_tac n,auto) +apply (simp add: i_rt_Suc_back) +by (drule slen_rt_mono,simp) + +lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU" +apply (induct_tac n) + apply (simp add: i_rt_Suc_back,auto) +apply (case_tac "s=UU",auto) +by (drule stream_exhaust_eq [THEN iffD1],auto) + +lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)" +apply auto + apply (insert i_rt_ij_lemma [of n "Suc 0" s]) + apply (subgoal_tac "#(i_rt n s)=0") + apply (case_tac "stream_take n$s = s",simp+) + apply (insert slen_take_eq [rule_format,of n s],simp) + apply (cases "#s") apply (simp_all add: zero_inat_def) + apply (simp add: slen_take_eq) + apply (cases "#s") + using i_rt_take_lemma1 [of n s] + apply (simp_all add: zero_inat_def) + done + +lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU" +by (simp add: i_rt_slen slen_take_lemma1) + +lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s" +apply (induct_tac n, auto) + apply (cases s, auto simp del: i_rt_Suc) +by (simp add: i_rt_Suc_back stream_finite_rt_eq)+ + +lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl & + #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j + --> Fin (j + t) = #x" +apply (induct n, auto) + apply (simp add: zero_inat_def) +apply (case_tac "x=UU",auto) + apply (simp add: zero_inat_def) +apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) +apply (subgoal_tac "EX k. Fin k = #y",clarify) + apply (erule_tac x="k" in allE) + apply (erule_tac x="y" in allE,auto) + apply (erule_tac x="THE p. Suc p = t" in allE,auto) + apply (simp add: iSuc_def split: inat.splits) + apply (simp add: iSuc_def split: inat.splits) + apply (simp only: the_equality) + apply (simp add: iSuc_def split: inat.splits) + apply force +apply (simp add: iSuc_def split: inat.splits) +done + +lemma take_i_rt_len: +"[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==> + Fin (j + t) = #x" +by (blast intro: take_i_rt_len_lemma [rule_format]) + + +(* ----------------------------------------------------------------------- *) + section "i_th" +(* ----------------------------------------------------------------------- *) + +lemma i_th_i_rt_step: +"[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==> + i_rt n s1 << i_rt n s2" +apply (simp add: i_th_def i_rt_Suc_back) +apply (cases "i_rt n s1", simp) +apply (cases "i_rt n s2", auto) +done + +lemma i_th_stream_take_Suc [rule_format]: + "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s" +apply (induct_tac n,auto) + apply (simp add: i_th_def) + apply (case_tac "s=UU",auto) + apply (drule stream_exhaust_eq [THEN iffD1],auto) +apply (case_tac "s=UU",simp add: i_th_def) +apply (drule stream_exhaust_eq [THEN iffD1],auto) +by (simp add: i_th_def i_rt_Suc_forw) + +lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)" +apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"]) +apply (rule i_th_stream_take_Suc [THEN subst]) +apply (simp add: i_th_def i_rt_Suc_back [symmetric]) +by (simp add: i_rt_take_lemma1) + +lemma i_th_last_eq: +"i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)" +apply (insert i_th_last [of n s1]) +apply (insert i_th_last [of n s2]) +by auto + +lemma i_th_prefix_lemma: +"[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==> + i_th k s1 << i_th k s2" +apply (insert i_th_stream_take_Suc [of k s1, THEN sym]) +apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto) +apply (simp add: i_th_def) +apply (rule monofun_cfun, auto) +apply (rule i_rt_mono) +by (blast intro: stream_take_lemma10) + +lemma take_i_rt_prefix_lemma1: + "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> + i_rt (Suc n) s1 << i_rt (Suc n) s2 ==> + i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2" +apply auto + apply (insert i_th_prefix_lemma [of n n s1 s2]) + apply (rule i_th_i_rt_step,auto) +by (drule mono_stream_take_pred,simp) + +lemma take_i_rt_prefix_lemma: +"[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2" +apply (case_tac "n=0",simp) +apply (auto) +apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 & + i_rt 0 s1 << i_rt 0 s2") + defer 1 + apply (rule zero_induct,blast) + apply (blast dest: take_i_rt_prefix_lemma1) +by simp + +lemma streams_prefix_lemma: "(s1 << s2) = + (stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)" +apply auto + apply (simp add: monofun_cfun_arg) + apply (simp add: i_rt_mono) +by (erule take_i_rt_prefix_lemma,simp) + +lemma streams_prefix_lemma1: + "[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2" +apply (simp add: po_eq_conv,auto) + apply (insert streams_prefix_lemma) + by blast+ + + +(* ----------------------------------------------------------------------- *) + section "sconc" +(* ----------------------------------------------------------------------- *) + +lemma UU_sconc [simp]: " UU ooo s = s " +by (simp add: sconc_def zero_inat_def) + +lemma scons_neq_UU: "a~=UU ==> a && s ~=UU" +by auto + +lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y" +apply (simp add: sconc_def zero_inat_def iSuc_def split: inat.splits, auto) +apply (rule someI2_ex,auto) + apply (rule_tac x="x && y" in exI,auto) +apply (simp add: i_rt_Suc_forw) +apply (case_tac "xa=UU",simp) +by (drule stream_exhaust_eq [THEN iffD1],auto) + +lemma ex_sconc [rule_format]: + "ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)" +apply (case_tac "#x") + apply (rule stream_finite_ind [of x],auto) + apply (simp add: stream.finite_def) + apply (drule slen_take_lemma1,blast) + apply (simp_all add: zero_inat_def iSuc_def split: inat.splits) +apply (erule_tac x="y" in allE,auto) +by (rule_tac x="a && w" in exI,auto) + +lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y" +apply (simp add: sconc_def split: inat.splits, arith?,auto) +apply (rule someI2_ex,auto) +by (drule ex_sconc,simp) + +lemma sconc_inj2: "\Fin n = #x; x ooo y = x ooo z\ \ y = z" +apply (frule_tac y=y in rt_sconc1) +by (auto elim: rt_sconc1) + +lemma sconc_UU [simp]:"s ooo UU = s" +apply (case_tac "#s") + apply (simp add: sconc_def) + apply (rule someI2_ex) + apply (rule_tac x="s" in exI) + apply auto + apply (drule slen_take_lemma1,auto) + apply (simp add: i_rt_lemma_slen) + apply (drule slen_take_lemma1,auto) + apply (simp add: i_rt_slen) +by (simp add: sconc_def) + +lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x" +apply (simp add: sconc_def) +apply (cases "#x") +apply auto +apply (rule someI2_ex, auto) +by (drule ex_sconc,simp) + +lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y" +apply (cases "#x",auto) + apply (simp add: sconc_def iSuc_Fin) + apply (rule someI2_ex) + apply (drule ex_sconc, simp) + apply (rule someI2_ex, auto) + apply (simp add: i_rt_Suc_forw) + apply (rule_tac x="a && x" in exI, auto) + apply (case_tac "xa=UU",auto) + apply (drule stream_exhaust_eq [THEN iffD1],auto) + apply (drule streams_prefix_lemma1,simp+) +by (simp add: sconc_def) + +lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x" +by (cases x, auto) + +lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z" +apply (case_tac "#x") + apply (rule stream_finite_ind [of x],auto simp del: scons_sconc) + apply (simp add: stream.finite_def del: scons_sconc) + apply (drule slen_take_lemma1,auto simp del: scons_sconc) + apply (case_tac "a = UU", auto) +by (simp add: sconc_def) + + +(* ----------------------------------------------------------------------- *) + +lemma cont_sconc_lemma1: "stream_finite x \ cont (\y. x ooo y)" +by (erule stream_finite_ind, simp_all) + +lemma cont_sconc_lemma2: "\ stream_finite x \ cont (\y. x ooo y)" +by (simp add: sconc_def slen_def) + +lemma cont_sconc: "cont (\y. x ooo y)" +apply (cases "stream_finite x") +apply (erule cont_sconc_lemma1) +apply (erule cont_sconc_lemma2) +done + +lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'" +by (rule cont_sconc [THEN cont2mono, THEN monofunE]) + +lemma sconc_mono1 [simp]: "x << x ooo y" +by (rule sconc_mono [of UU, simplified]) + +(* ----------------------------------------------------------------------- *) + +lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)" +apply (case_tac "#x",auto) + apply (insert sconc_mono1 [of x y]) + by auto + +(* ----------------------------------------------------------------------- *) + +lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x" +by (cases s, auto) + +lemma i_th_sconc_lemma [rule_format]: + "ALL x y. Fin n < #x --> i_th n (x ooo y) = i_th n x" +apply (induct_tac n, auto) +apply (simp add: Fin_0 i_th_def) +apply (simp add: slen_empty_eq ft_sconc) +apply (simp add: i_th_def) +apply (case_tac "x=UU",auto) +apply (drule stream_exhaust_eq [THEN iffD1], auto) +apply (erule_tac x="ya" in allE) +apply (case_tac "#ya") by simp_all + + + +(* ----------------------------------------------------------------------- *) + +lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s" +apply (induct_tac n,auto) +apply (case_tac "s=UU",auto) +by (drule stream_exhaust_eq [THEN iffD1],auto) + +(* ----------------------------------------------------------------------- *) + subsection "pointwise equality" +(* ----------------------------------------------------------------------- *) + +lemma ex_last_stream_take_scons: "stream_take (Suc n)$s = + stream_take n$s ooo i_rt n (stream_take (Suc n)$s)" +by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp) + +lemma i_th_stream_take_eq: +"!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2" +apply (induct_tac n,auto) +apply (subgoal_tac "stream_take (Suc na)$s1 = + stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)") + apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) = + i_rt na (stream_take (Suc na)$s2)") + apply (subgoal_tac "stream_take (Suc na)$s2 = + stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)") + apply (insert ex_last_stream_take_scons,simp) + apply blast + apply (erule_tac x="na" in allE) + apply (insert i_th_last_eq [of _ s1 s2]) +by blast+ + +lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2" +by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast) + +(* ----------------------------------------------------------------------- *) + subsection "finiteness" +(* ----------------------------------------------------------------------- *) + +lemma slen_sconc_finite1: + "[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty" +apply (case_tac "#y ~= Infty",auto) +apply (drule_tac y=y in rt_sconc1) +apply (insert stream_finite_i_rt [of n "x ooo y"]) +by (simp add: slen_infinite) + +lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty" +by (simp add: sconc_def) + +lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty" +apply (case_tac "#x") + apply (simp add: sconc_def) + apply (rule someI2_ex) + apply (drule ex_sconc,auto) + apply (erule contrapos_pp) + apply (insert stream_finite_i_rt) + apply (fastsimp simp add: slen_infinite,auto) +by (simp add: sconc_def) + +lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)" +apply auto + apply (metis not_Infty_eq slen_sconc_finite1) + apply (metis not_Infty_eq slen_sconc_infinite1) +apply (metis not_Infty_eq slen_sconc_infinite2) +done + +(* ----------------------------------------------------------------------- *) + +lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k" +apply (insert slen_mono [of "x" "x ooo y"]) +apply (cases "#x") apply simp_all +apply (cases "#(x ooo y)") apply simp_all +done + +(* ----------------------------------------------------------------------- *) + subsection "finite slen" +(* ----------------------------------------------------------------------- *) + +lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)" +apply (case_tac "#(x ooo y)") + apply (frule_tac y=y in rt_sconc1) + apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp) + apply (insert slen_sconc_mono3 [of n x _ y],simp) +by (insert sconc_finite [of x y],auto) + +(* ----------------------------------------------------------------------- *) + subsection "flat prefix" +(* ----------------------------------------------------------------------- *) + +lemma sconc_prefix: "(s1::'a::flat stream) << s2 ==> EX t. s1 ooo t = s2" +apply (case_tac "#s1") + apply (subgoal_tac "stream_take nat$s1 = stream_take nat$s2") + apply (rule_tac x="i_rt nat s2" in exI) + apply (simp add: sconc_def) + apply (rule someI2_ex) + apply (drule ex_sconc) + apply (simp,clarsimp,drule streams_prefix_lemma1) + apply (simp+,rule slen_take_lemma3 [of _ s1 s2]) + apply (simp+,rule_tac x="UU" in exI) +apply (insert slen_take_lemma3 [of _ s1 s2]) +by (rule stream.take_lemma,simp) + +(* ----------------------------------------------------------------------- *) + subsection "continuity" +(* ----------------------------------------------------------------------- *) + +lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))" +by (simp add: chain_def,auto simp add: sconc_mono) + +lemma chain_scons: "chain S ==> chain (%i. a && S i)" +apply (simp add: chain_def,auto) +by (rule monofun_cfun_arg,simp) + +lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)" +by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric]) + +lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> + (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" +apply (rule stream_finite_ind [of x]) + apply (auto) +apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)") + by (force,blast dest: contlub_scons_lemma chain_sconc) + +lemma contlub_sconc_lemma: + "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" +apply (case_tac "#x=Infty") + apply (simp add: sconc_def) +apply (drule finite_lub_sconc,auto simp add: slen_infinite) +done + +lemma monofun_sconc: "monofun (%y. x ooo y)" +by (simp add: monofun_def sconc_mono) + + +(* ----------------------------------------------------------------------- *) + section "constr_sconc" +(* ----------------------------------------------------------------------- *) + +lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s" +by (simp add: constr_sconc_def zero_inat_def) + +lemma "x ooo y = constr_sconc x y" +apply (case_tac "#x") + apply (rule stream_finite_ind [of x],auto simp del: scons_sconc) + defer 1 + apply (simp add: constr_sconc_def del: scons_sconc) + apply (case_tac "#s") + apply (simp add: iSuc_Fin) + apply (case_tac "a=UU",auto simp del: scons_sconc) + apply (simp) + apply (simp add: sconc_def) + apply (simp add: constr_sconc_def) +apply (simp add: stream.finite_def) +by (drule slen_take_lemma1,auto) + +end diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/Library/Strict_Fun.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Library/Strict_Fun.thy Mon May 24 12:10:24 2010 -0700 @@ -0,0 +1,239 @@ +(* Title: HOLCF/ex/Strict_Fun.thy + Author: Brian Huffman +*) + +header {* The Strict Function Type *} + +theory Strict_Fun +imports HOLCF +begin + +pcpodef (open) ('a, 'b) sfun (infixr "->!" 0) + = "{f :: 'a \ 'b. f\\ = \}" +by simp_all + +type_notation (xsymbols) + sfun (infixr "\!" 0) + +text {* TODO: Define nice syntax for abstraction, application. *} + +definition + sfun_abs :: "('a \ 'b) \ ('a \! 'b)" +where + "sfun_abs = (\ f. Abs_sfun (strictify\f))" + +definition + sfun_rep :: "('a \! 'b) \ 'a \ 'b" +where + "sfun_rep = (\ f. Rep_sfun f)" + +lemma sfun_rep_beta: "sfun_rep\f = Rep_sfun f" + unfolding sfun_rep_def by (simp add: cont_Rep_sfun) + +lemma sfun_rep_strict1 [simp]: "sfun_rep\\ = \" + unfolding sfun_rep_beta by (rule Rep_sfun_strict) + +lemma sfun_rep_strict2 [simp]: "sfun_rep\f\\ = \" + unfolding sfun_rep_beta by (rule Rep_sfun [simplified]) + +lemma strictify_cancel: "f\\ = \ \ strictify\f = f" + by (simp add: expand_cfun_eq strictify_conv_if) + +lemma sfun_abs_sfun_rep: "sfun_abs\(sfun_rep\f) = f" + unfolding sfun_abs_def sfun_rep_def + apply (simp add: cont_Abs_sfun cont_Rep_sfun) + apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse) + apply (simp add: expand_cfun_eq strictify_conv_if) + apply (simp add: Rep_sfun [simplified]) + done + +lemma sfun_rep_sfun_abs [simp]: "sfun_rep\(sfun_abs\f) = strictify\f" + unfolding sfun_abs_def sfun_rep_def + apply (simp add: cont_Abs_sfun cont_Rep_sfun) + apply (simp add: Abs_sfun_inverse) + done + +lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs" +apply default +apply (rule sfun_abs_sfun_rep) +apply (simp add: expand_cfun_below strictify_conv_if) +done + +interpretation sfun: ep_pair sfun_rep sfun_abs + by (rule ep_pair_sfun) + +subsection {* Map functional for strict function space *} + +definition + sfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \! 'c) \ ('b \! 'd)" +where + "sfun_map = (\ a b. sfun_abs oo cfun_map\a\b oo sfun_rep)" + +lemma sfun_map_ID: "sfun_map\ID\ID = ID" + unfolding sfun_map_def + by (simp add: cfun_map_ID expand_cfun_eq) + +lemma sfun_map_map: + assumes "f2\\ = \" and "g2\\ = \" shows + "sfun_map\f1\g1\(sfun_map\f2\g2\p) = + sfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" +unfolding sfun_map_def +by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map) + +lemma ep_pair_sfun_map: + assumes 1: "ep_pair e1 p1" + assumes 2: "ep_pair e2 p2" + shows "ep_pair (sfun_map\p1\e2) (sfun_map\e1\p2)" +proof + interpret e1p1: pcpo_ep_pair e1 p1 + unfolding pcpo_ep_pair_def by fact + interpret e2p2: pcpo_ep_pair e2 p2 + unfolding pcpo_ep_pair_def by fact + fix f show "sfun_map\e1\p2\(sfun_map\p1\e2\f) = f" + unfolding sfun_map_def + apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel) + apply (rule ep_pair.e_inverse) + apply (rule ep_pair_cfun_map [OF 1 2]) + done + fix g show "sfun_map\p1\e2\(sfun_map\e1\p2\g) \ g" + unfolding sfun_map_def + apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel) + apply (rule ep_pair.e_p_below) + apply (rule ep_pair_cfun_map [OF 1 2]) + done +qed + +lemma deflation_sfun_map: + assumes 1: "deflation d1" + assumes 2: "deflation d2" + shows "deflation (sfun_map\d1\d2)" +apply (simp add: sfun_map_def) +apply (rule deflation.intro) +apply simp +apply (subst strictify_cancel) +apply (simp add: cfun_map_def deflation_strict 1 2) +apply (simp add: cfun_map_def deflation.idem 1 2) +apply (simp add: sfun.e_below_iff [symmetric]) +apply (subst strictify_cancel) +apply (simp add: cfun_map_def deflation_strict 1 2) +apply (rule deflation.below) +apply (rule deflation_cfun_map [OF 1 2]) +done + +lemma finite_deflation_sfun_map: + assumes 1: "finite_deflation d1" + assumes 2: "finite_deflation d2" + shows "finite_deflation (sfun_map\d1\d2)" +proof (intro finite_deflation.intro finite_deflation_axioms.intro) + interpret d1: finite_deflation d1 by fact + interpret d2: finite_deflation d2 by fact + have "deflation d1" and "deflation d2" by fact+ + thus "deflation (sfun_map\d1\d2)" by (rule deflation_sfun_map) + from 1 2 have "finite_deflation (cfun_map\d1\d2)" + by (rule finite_deflation_cfun_map) + then have "finite {f. cfun_map\d1\d2\f = f}" + by (rule finite_deflation.finite_fixes) + moreover have "inj (\f. sfun_rep\f)" + by (rule inj_onI, simp) + ultimately have "finite ((\f. sfun_rep\f) -` {f. cfun_map\d1\d2\f = f})" + by (rule finite_vimageI) + then show "finite {f. sfun_map\d1\d2\f = f}" + unfolding sfun_map_def sfun.e_eq_iff [symmetric] + by (simp add: strictify_cancel + deflation_strict `deflation d1` `deflation d2`) +qed + +subsection {* Strict function space is bifinite *} + +instantiation sfun :: (bifinite, bifinite) bifinite +begin + +definition + "approx = (\i. sfun_map\(approx i)\(approx i))" + +instance proof + show "chain (approx :: nat \ ('a \! 'b) \ ('a \! 'b))" + unfolding approx_sfun_def by simp +next + fix x :: "'a \! 'b" + show "(\i. approx i\x) = x" + unfolding approx_sfun_def + by (simp add: lub_distribs sfun_map_ID [unfolded ID_def]) +next + fix i :: nat and x :: "'a \! 'b" + show "approx i\(approx i\x) = approx i\x" + unfolding approx_sfun_def + by (intro deflation.idem deflation_sfun_map deflation_approx) +next + fix i :: nat + show "finite {x::'a \! 'b. approx i\x = x}" + unfolding approx_sfun_def + by (intro finite_deflation.finite_fixes + finite_deflation_sfun_map + finite_deflation_approx) +qed + +end + +subsection {* Strict function space is representable *} + +instantiation sfun :: (rep, rep) rep +begin + +definition + "emb = udom_emb oo sfun_map\prj\emb" + +definition + "prj = sfun_map\emb\prj oo udom_prj" + +instance +apply (default, unfold emb_sfun_def prj_sfun_def) +apply (rule ep_pair_comp) +apply (rule ep_pair_sfun_map) +apply (rule ep_pair_emb_prj) +apply (rule ep_pair_emb_prj) +apply (rule ep_pair_udom) +done + +end + +text {* + A deflation constructor lets us configure the domain package to work + with the strict function space type constructor. +*} + +definition + sfun_defl :: "TypeRep \ TypeRep \ TypeRep" +where + "sfun_defl = TypeRep_fun2 sfun_map" + +lemma cast_sfun_defl: + "cast\(sfun_defl\A\B) = udom_emb oo sfun_map\(cast\A)\(cast\B) oo udom_prj" +unfolding sfun_defl_def +apply (rule cast_TypeRep_fun2) +apply (erule (1) finite_deflation_sfun_map) +done + +lemma REP_sfun: "REP('a::rep \! 'b::rep) = sfun_defl\REP('a)\REP('b)" +apply (rule cast_eq_imp_eq, rule ext_cfun) +apply (simp add: cast_REP cast_sfun_defl) +apply (simp only: prj_sfun_def emb_sfun_def) +apply (simp add: sfun_map_def cfun_map_def strictify_cancel) +done + +lemma isodefl_sfun: + "isodefl d1 t1 \ isodefl d2 t2 \ + isodefl (sfun_map\d1\d2) (sfun_defl\t1\t2)" +apply (rule isodeflI) +apply (simp add: cast_sfun_defl cast_isodefl) +apply (simp add: emb_sfun_def prj_sfun_def) +apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation]) +done + +setup {* + Domain_Isomorphism.add_type_constructor + (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm REP_sfun}, + @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map}) +*} + +end diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/ex/ROOT.ML --- a/src/HOLCF/ex/ROOT.ML Mon May 24 11:29:49 2010 -0700 +++ b/src/HOLCF/ex/ROOT.ML Mon May 24 12:10:24 2010 -0700 @@ -3,8 +3,7 @@ Misc HOLCF examples. *) -use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare", +use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare", "Loop", "Powerdomain_ex", "Domain_Proofs", "Letrec", - "Pattern_Match", - "Strict_Fun"]; + "Pattern_Match"]; diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Mon May 24 11:29:49 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,965 +0,0 @@ -(* Title: HOLCF/ex/Stream.thy - Author: Franz Regensburger, David von Oheimb, Borislav Gajanovic -*) - -header {* General Stream domain *} - -theory Stream -imports HOLCF Nat_Infinity -begin - -domain 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65) - -definition - smap :: "('a \ 'b) \ 'a stream \ 'b stream" where - "smap = fix\(\ h f s. case s of x && xs \ f\x && h\f\xs)" - -definition - sfilter :: "('a \ tr) \ 'a stream \ 'a stream" where - "sfilter = fix\(\ h p s. case s of x && xs \ - If p\x then x && h\p\xs else h\p\xs fi)" - -definition - slen :: "'a stream \ inat" ("#_" [1000] 1000) where - "#s = (if stream_finite s then Fin (LEAST n. stream_take n\s = s) else \)" - - -(* concatenation *) - -definition - i_rt :: "nat => 'a stream => 'a stream" where (* chops the first i elements *) - "i_rt = (%i s. iterate i$rt$s)" - -definition - i_th :: "nat => 'a stream => 'a" where (* the i-th element *) - "i_th = (%i s. ft$(i_rt i s))" - -definition - sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where - "s1 ooo s2 = (case #s1 of - Fin n \ (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) - | \ \ s1)" - -primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" -where - 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" where (* constructive *) - "constr_sconc s1 s2 = (case #s1 of - Fin n \ constr_sconc' n s1 s2 - | \ \ s1)" - - -(* ----------------------------------------------------------------------- *) -(* theorems about scons *) -(* ----------------------------------------------------------------------- *) - - -section "scons" - -lemma scons_eq_UU: "(a && s = UU) = (a = UU)" -by simp - -lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R" -by simp - -lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)" -by (cases x, auto) - -lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU" -by (simp add: stream_exhaust_eq,auto) - -lemma stream_prefix: - "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt" -by (cases t, auto) - -lemma stream_prefix': - "b ~= UU ==> x << b && z = - (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))" -by (cases x, auto) - - -(* -lemma stream_prefix1: "[| x< x&&xs << y&&ys" -by (insert stream_prefix' [of y "x&&xs" ys],force) -*) - -lemma stream_flat_prefix: - "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" -apply (case_tac "y=UU",auto) -by (drule ax_flat,simp) - - - - -(* ----------------------------------------------------------------------- *) -(* theorems about stream_when *) -(* ----------------------------------------------------------------------- *) - -section "stream_when" - - -lemma stream_when_strictf: "stream_when$UU$s=UU" -by (cases s, auto) - - - -(* ----------------------------------------------------------------------- *) -(* theorems about ft and rt *) -(* ----------------------------------------------------------------------- *) - - -section "ft & rt" - - -lemma ft_defin: "s~=UU ==> ft$s~=UU" -by simp - -lemma rt_strict_rev: "rt$s~=UU ==> s~=UU" -by auto - -lemma surjectiv_scons: "(ft$s)&&(rt$s)=s" -by (cases s, auto) - -lemma monofun_rt_mult: "x << s ==> iterate i$rt$x << iterate i$rt$s" -by (rule monofun_cfun_arg) - - - -(* ----------------------------------------------------------------------- *) -(* theorems about stream_take *) -(* ----------------------------------------------------------------------- *) - - -section "stream_take" - - -lemma stream_reach2: "(LUB i. stream_take i$s) = s" -by (rule stream.reach) - -lemma chain_stream_take: "chain (%i. stream_take i$s)" -by simp - -lemma stream_take_prefix [simp]: "stream_take n$s << s" -apply (insert stream_reach2 [of s]) -apply (erule subst) back -apply (rule is_ub_thelub) -by (simp only: chain_stream_take) - -lemma stream_take_more [rule_format]: - "ALL x. stream_take n$x = x --> stream_take (Suc n)$x = x" -apply (induct_tac n,auto) -apply (case_tac "x=UU",auto) -by (drule stream_exhaust_eq [THEN iffD1],auto) - -lemma stream_take_lemma3 [rule_format]: - "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs" -apply (induct_tac n,clarsimp) -(*apply (drule sym, erule scons_not_empty, simp)*) -apply (clarify, rule stream_take_more) -apply (erule_tac x="x" in allE) -by (erule_tac x="xs" in allE,simp) - -lemma stream_take_lemma4: - "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs" -by auto - -lemma stream_take_idempotent [rule_format, simp]: - "ALL s. stream_take n$(stream_take n$s) = stream_take n$s" -apply (induct_tac n, auto) -apply (case_tac "s=UU", auto) -by (drule stream_exhaust_eq [THEN iffD1], auto) - -lemma stream_take_take_Suc [rule_format, simp]: - "ALL s. stream_take n$(stream_take (Suc n)$s) = - stream_take n$s" -apply (induct_tac n, auto) -apply (case_tac "s=UU", auto) -by (drule stream_exhaust_eq [THEN iffD1], auto) - -lemma mono_stream_take_pred: - "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> - stream_take n$s1 << stream_take n$s2" -by (insert monofun_cfun_arg [of "stream_take (Suc n)$s1" - "stream_take (Suc n)$s2" "stream_take n"], auto) -(* -lemma mono_stream_take_pred: - "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> - stream_take n$s1 << stream_take n$s2" -by (drule mono_stream_take [of _ _ n],simp) -*) - -lemma stream_take_lemma10 [rule_format]: - "ALL k<=n. stream_take n$s1 << stream_take n$s2 - --> stream_take k$s1 << stream_take k$s2" -apply (induct_tac n,simp,clarsimp) -apply (case_tac "k=Suc n",blast) -apply (erule_tac x="k" in allE) -by (drule mono_stream_take_pred,simp) - -lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1" -apply (insert chain_stream_take [of s1]) -by (drule chain_mono,auto) - -lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2" -by (simp add: monofun_cfun_arg) - -(* -lemma stream_take_prefix [simp]: "stream_take n$s << s" -apply (subgoal_tac "s=(LUB n. stream_take n$s)") - apply (erule ssubst, rule is_ub_thelub) - apply (simp only: chain_stream_take) -by (simp only: stream_reach2) -*) - -lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s" -by (rule monofun_cfun_arg,auto) - - -(* ------------------------------------------------------------------------- *) -(* special induction rules *) -(* ------------------------------------------------------------------------- *) - - -section "induction" - -lemma stream_finite_ind: - "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x" -apply (simp add: stream.finite_def,auto) -apply (erule subst) -by (drule stream.finite_induct [of P _ x], auto) - -lemma stream_finite_ind2: -"[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==> - !s. P (stream_take n$s)" -apply (rule nat_less_induct [of _ n],auto) -apply (case_tac n, auto) -apply (case_tac nat, auto) -apply (case_tac "s=UU",clarsimp) -apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) -apply (case_tac "s=UU",clarsimp) -apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) -apply (case_tac "y=UU",clarsimp) -by (drule stream_exhaust_eq [THEN iffD1],clarsimp) - -lemma stream_ind2: -"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x" -apply (insert stream.reach [of x],erule subst) -apply (erule admD, rule chain_stream_take) -apply (insert stream_finite_ind2 [of P]) -by simp - - - -(* ----------------------------------------------------------------------- *) -(* simplify use of coinduction *) -(* ----------------------------------------------------------------------- *) - - -section "coinduction" - -lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R" - apply (simp add: stream.bisim_def,clarsimp) - apply (drule spec, drule spec, drule (1) mp) - apply (case_tac "x", simp) - apply (case_tac "x'", simp) -by auto - - - -(* ----------------------------------------------------------------------- *) -(* theorems about stream_finite *) -(* ----------------------------------------------------------------------- *) - - -section "stream_finite" - -lemma stream_finite_UU [simp]: "stream_finite UU" -by (simp add: stream.finite_def) - -lemma stream_finite_UU_rev: "~ stream_finite s ==> s ~= UU" -by (auto simp add: stream.finite_def) - -lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)" -apply (simp add: stream.finite_def,auto) -apply (rule_tac x="Suc n" in exI) -by (simp add: stream_take_lemma4) - -lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" -apply (simp add: stream.finite_def, auto) -apply (rule_tac x="n" in exI) -by (erule stream_take_lemma3,simp) - -lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s" -apply (cases s, auto) -apply (rule stream_finite_lemma1, simp) -by (rule stream_finite_lemma2,simp) - -lemma stream_finite_less: "stream_finite s ==> !t. t< stream_finite t" -apply (erule stream_finite_ind [of s], auto) -apply (case_tac "t=UU", auto) -apply (drule stream_exhaust_eq [THEN iffD1],auto) -apply (erule_tac x="y" in allE, simp) -by (rule stream_finite_lemma1, simp) - -lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)" -apply (simp add: stream.finite_def) -by (rule_tac x="n" in exI,simp) - -lemma adm_not_stream_finite: "adm (%x. ~ stream_finite x)" -apply (rule adm_upward) -apply (erule contrapos_nn) -apply (erule (1) stream_finite_less [rule_format]) -done - - - -(* ----------------------------------------------------------------------- *) -(* theorems about stream length *) -(* ----------------------------------------------------------------------- *) - - -section "slen" - -lemma slen_empty [simp]: "#\ = 0" -by (simp add: slen_def stream.finite_def zero_inat_def Least_equality) - -lemma slen_scons [simp]: "x ~= \ ==> #(x&&xs) = iSuc (#xs)" -apply (case_tac "stream_finite (x && xs)") -apply (simp add: slen_def, auto) -apply (simp add: stream.finite_def, auto simp add: iSuc_Fin) -apply (rule Least_Suc2, auto) -(*apply (drule sym)*) -(*apply (drule sym scons_eq_UU [THEN iffD1],simp)*) -apply (erule stream_finite_lemma2, simp) -apply (simp add: slen_def, auto) -by (drule stream_finite_lemma1,auto) - -lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \)" -by (cases x, auto simp add: Fin_0 iSuc_Fin[THEN sym]) - -lemma slen_empty_eq: "(#x = 0) = (x = \)" -by (cases x, auto) - -lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \ & Fin n < #y)" -apply (auto, case_tac "x=UU",auto) -apply (drule stream_exhaust_eq [THEN iffD1], auto) -apply (case_tac "#y") apply simp_all -apply (case_tac "#y") apply simp_all -done - -lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y & a ~= \ & #y = n)" -by (cases x, auto) - -lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \" -by (simp add: slen_def) - -lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \ | #y < Fin (Suc n))" - apply (cases x, auto) - apply (simp add: zero_inat_def) - apply (case_tac "#stream") apply (simp_all add: iSuc_Fin) - apply (case_tac "#stream") apply (simp_all add: iSuc_Fin) -done - -lemma slen_take_lemma4 [rule_format]: - "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n" -apply (induct n, auto simp add: Fin_0) -apply (case_tac "s=UU", simp) -by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_Fin) - -(* -lemma stream_take_idempotent [simp]: - "stream_take n$(stream_take n$s) = stream_take n$s" -apply (case_tac "stream_take n$s = s") -apply (auto,insert slen_take_lemma4 [of n s]); -by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp) - -lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) = - stream_take n$s" -apply (simp add: po_eq_conv,auto) - apply (simp add: stream_take_take_less) -apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)") - apply (erule ssubst) - apply (rule_tac monofun_cfun_arg) - apply (insert chain_stream_take [of s]) -by (simp add: chain_def,simp) -*) - -lemma slen_take_eq: "ALL x. (Fin n < #x) = (stream_take n\x ~= x)" -apply (induct_tac n, auto) -apply (simp add: Fin_0, clarsimp) -apply (drule not_sym) -apply (drule slen_empty_eq [THEN iffD1], simp) -apply (case_tac "x=UU", simp) -apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) -apply (erule_tac x="y" in allE, auto) -apply (simp_all add: not_less iSuc_Fin) -apply (case_tac "#y") apply simp_all -apply (case_tac "x=UU", simp) -apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) -apply (erule_tac x="y" in allE, simp) -apply (case_tac "#y") by simp_all - -lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\x = x)" -by (simp add: linorder_not_less [symmetric] slen_take_eq) - -lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\x = x" -by (rule slen_take_eq_rev [THEN iffD1], auto) - -lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)" -apply (cases s1) - by (cases s2, simp+)+ - -lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n" -apply (case_tac "stream_take n$s = s") - apply (simp add: slen_take_eq_rev) -by (simp add: slen_take_lemma4) - -lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\x) = Fin i" -apply (simp add: stream.finite_def, auto) -by (simp add: slen_take_lemma4) - -lemma slen_infinite: "stream_finite x = (#x ~= Infty)" -by (simp add: slen_def) - -lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t" -apply (erule stream_finite_ind [of s], auto) -apply (case_tac "t=UU", auto) -apply (drule stream_exhaust_eq [THEN iffD1], auto) -done - -lemma slen_mono: "s << t ==> #s <= #t" -apply (case_tac "stream_finite t") -apply (frule stream_finite_less) -apply (erule_tac x="s" in allE, simp) -apply (drule slen_mono_lemma, auto) -by (simp add: slen_def) - -lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)" -by (insert iterate_Suc2 [of n F x], auto) - -lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)" -apply (induct i, auto) -apply (case_tac "x=UU", auto simp add: zero_inat_def) -apply (drule stream_exhaust_eq [THEN iffD1], auto) -apply (erule_tac x="y" in allE, auto) -apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin) -by (simp add: iterate_lemma) - -lemma slen_take_lemma3 [rule_format]: - "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\x = stream_take n\y" -apply (induct_tac n, auto) -apply (case_tac "x=UU", auto) -apply (simp add: zero_inat_def) -apply (simp add: Suc_ile_eq) -apply (case_tac "y=UU", clarsimp) -apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ -apply (erule_tac x="ya" in allE, simp) -by (drule ax_flat, simp) - -lemma slen_strict_mono_lemma: - "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t" -apply (erule stream_finite_ind, auto) -apply (case_tac "sa=UU", auto) -apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) -by (drule ax_flat, simp) - -lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t" -by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma) - -lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==> - stream_take n$s ~= stream_take (Suc n)$s" -apply auto -apply (subgoal_tac "stream_take n$s ~=s") - apply (insert slen_take_lemma4 [of n s],auto) -apply (cases s, simp) -by (simp add: slen_take_lemma4 iSuc_Fin) - -(* ----------------------------------------------------------------------- *) -(* theorems about smap *) -(* ----------------------------------------------------------------------- *) - - -section "smap" - -lemma smap_unfold: "smap = (\ f t. case t of x&&xs \ f$x && smap$f$xs)" -by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto) - -lemma smap_empty [simp]: "smap\f\\ = \" -by (subst smap_unfold, simp) - -lemma smap_scons [simp]: "x~=\ ==> smap\f\(x&&xs) = (f\x)&&(smap\f\xs)" -by (subst smap_unfold, force) - - - -(* ----------------------------------------------------------------------- *) -(* theorems about sfilter *) -(* ----------------------------------------------------------------------- *) - -section "sfilter" - -lemma sfilter_unfold: - "sfilter = (\ p s. case s of x && xs \ - If p\x then x && sfilter\p\xs else sfilter\p\xs fi)" -by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto) - -lemma strict_sfilter: "sfilter\\ = \" -apply (rule ext_cfun) -apply (subst sfilter_unfold, auto) -apply (case_tac "x=UU", auto) -by (drule stream_exhaust_eq [THEN iffD1], auto) - -lemma sfilter_empty [simp]: "sfilter\f\\ = \" -by (subst sfilter_unfold, force) - -lemma sfilter_scons [simp]: - "x ~= \ ==> sfilter\f\(x && xs) = - If f\x then x && sfilter\f\xs else sfilter\f\xs fi" -by (subst sfilter_unfold, force) - - -(* ----------------------------------------------------------------------- *) - section "i_rt" -(* ----------------------------------------------------------------------- *) - -lemma i_rt_UU [simp]: "i_rt n UU = UU" - by (induct n) (simp_all add: i_rt_def) - -lemma i_rt_0 [simp]: "i_rt 0 s = s" -by (simp add: i_rt_def) - -lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s" -by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc) - -lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)" -by (simp only: i_rt_def iterate_Suc2) - -lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)" -by (simp only: i_rt_def,auto) - -lemma i_rt_mono: "x << s ==> i_rt n x << i_rt n s" -by (simp add: i_rt_def monofun_rt_mult) - -lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)" -by (simp add: i_rt_def slen_rt_mult) - -lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)" -apply (induct_tac n,auto) -apply (simp add: i_rt_Suc_back) -by (drule slen_rt_mono,simp) - -lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU" -apply (induct_tac n) - apply (simp add: i_rt_Suc_back,auto) -apply (case_tac "s=UU",auto) -by (drule stream_exhaust_eq [THEN iffD1],auto) - -lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)" -apply auto - apply (insert i_rt_ij_lemma [of n "Suc 0" s]) - apply (subgoal_tac "#(i_rt n s)=0") - apply (case_tac "stream_take n$s = s",simp+) - apply (insert slen_take_eq [rule_format,of n s],simp) - apply (cases "#s") apply (simp_all add: zero_inat_def) - apply (simp add: slen_take_eq) - apply (cases "#s") - using i_rt_take_lemma1 [of n s] - apply (simp_all add: zero_inat_def) - done - -lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU" -by (simp add: i_rt_slen slen_take_lemma1) - -lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s" -apply (induct_tac n, auto) - apply (cases s, auto simp del: i_rt_Suc) -by (simp add: i_rt_Suc_back stream_finite_rt_eq)+ - -lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl & - #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j - --> Fin (j + t) = #x" -apply (induct n, auto) - apply (simp add: zero_inat_def) -apply (case_tac "x=UU",auto) - apply (simp add: zero_inat_def) -apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) -apply (subgoal_tac "EX k. Fin k = #y",clarify) - apply (erule_tac x="k" in allE) - apply (erule_tac x="y" in allE,auto) - apply (erule_tac x="THE p. Suc p = t" in allE,auto) - apply (simp add: iSuc_def split: inat.splits) - apply (simp add: iSuc_def split: inat.splits) - apply (simp only: the_equality) - apply (simp add: iSuc_def split: inat.splits) - apply force -apply (simp add: iSuc_def split: inat.splits) -done - -lemma take_i_rt_len: -"[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==> - Fin (j + t) = #x" -by (blast intro: take_i_rt_len_lemma [rule_format]) - - -(* ----------------------------------------------------------------------- *) - section "i_th" -(* ----------------------------------------------------------------------- *) - -lemma i_th_i_rt_step: -"[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==> - i_rt n s1 << i_rt n s2" -apply (simp add: i_th_def i_rt_Suc_back) -apply (cases "i_rt n s1", simp) -apply (cases "i_rt n s2", auto) -done - -lemma i_th_stream_take_Suc [rule_format]: - "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s" -apply (induct_tac n,auto) - apply (simp add: i_th_def) - apply (case_tac "s=UU",auto) - apply (drule stream_exhaust_eq [THEN iffD1],auto) -apply (case_tac "s=UU",simp add: i_th_def) -apply (drule stream_exhaust_eq [THEN iffD1],auto) -by (simp add: i_th_def i_rt_Suc_forw) - -lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)" -apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"]) -apply (rule i_th_stream_take_Suc [THEN subst]) -apply (simp add: i_th_def i_rt_Suc_back [symmetric]) -by (simp add: i_rt_take_lemma1) - -lemma i_th_last_eq: -"i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)" -apply (insert i_th_last [of n s1]) -apply (insert i_th_last [of n s2]) -by auto - -lemma i_th_prefix_lemma: -"[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==> - i_th k s1 << i_th k s2" -apply (insert i_th_stream_take_Suc [of k s1, THEN sym]) -apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto) -apply (simp add: i_th_def) -apply (rule monofun_cfun, auto) -apply (rule i_rt_mono) -by (blast intro: stream_take_lemma10) - -lemma take_i_rt_prefix_lemma1: - "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> - i_rt (Suc n) s1 << i_rt (Suc n) s2 ==> - i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2" -apply auto - apply (insert i_th_prefix_lemma [of n n s1 s2]) - apply (rule i_th_i_rt_step,auto) -by (drule mono_stream_take_pred,simp) - -lemma take_i_rt_prefix_lemma: -"[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2" -apply (case_tac "n=0",simp) -apply (auto) -apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 & - i_rt 0 s1 << i_rt 0 s2") - defer 1 - apply (rule zero_induct,blast) - apply (blast dest: take_i_rt_prefix_lemma1) -by simp - -lemma streams_prefix_lemma: "(s1 << s2) = - (stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)" -apply auto - apply (simp add: monofun_cfun_arg) - apply (simp add: i_rt_mono) -by (erule take_i_rt_prefix_lemma,simp) - -lemma streams_prefix_lemma1: - "[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2" -apply (simp add: po_eq_conv,auto) - apply (insert streams_prefix_lemma) - by blast+ - - -(* ----------------------------------------------------------------------- *) - section "sconc" -(* ----------------------------------------------------------------------- *) - -lemma UU_sconc [simp]: " UU ooo s = s " -by (simp add: sconc_def zero_inat_def) - -lemma scons_neq_UU: "a~=UU ==> a && s ~=UU" -by auto - -lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y" -apply (simp add: sconc_def zero_inat_def iSuc_def split: inat.splits, auto) -apply (rule someI2_ex,auto) - apply (rule_tac x="x && y" in exI,auto) -apply (simp add: i_rt_Suc_forw) -apply (case_tac "xa=UU",simp) -by (drule stream_exhaust_eq [THEN iffD1],auto) - -lemma ex_sconc [rule_format]: - "ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)" -apply (case_tac "#x") - apply (rule stream_finite_ind [of x],auto) - apply (simp add: stream.finite_def) - apply (drule slen_take_lemma1,blast) - apply (simp_all add: zero_inat_def iSuc_def split: inat.splits) -apply (erule_tac x="y" in allE,auto) -by (rule_tac x="a && w" in exI,auto) - -lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y" -apply (simp add: sconc_def split: inat.splits, arith?,auto) -apply (rule someI2_ex,auto) -by (drule ex_sconc,simp) - -lemma sconc_inj2: "\Fin n = #x; x ooo y = x ooo z\ \ y = z" -apply (frule_tac y=y in rt_sconc1) -by (auto elim: rt_sconc1) - -lemma sconc_UU [simp]:"s ooo UU = s" -apply (case_tac "#s") - apply (simp add: sconc_def) - apply (rule someI2_ex) - apply (rule_tac x="s" in exI) - apply auto - apply (drule slen_take_lemma1,auto) - apply (simp add: i_rt_lemma_slen) - apply (drule slen_take_lemma1,auto) - apply (simp add: i_rt_slen) -by (simp add: sconc_def) - -lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x" -apply (simp add: sconc_def) -apply (cases "#x") -apply auto -apply (rule someI2_ex, auto) -by (drule ex_sconc,simp) - -lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y" -apply (cases "#x",auto) - apply (simp add: sconc_def iSuc_Fin) - apply (rule someI2_ex) - apply (drule ex_sconc, simp) - apply (rule someI2_ex, auto) - apply (simp add: i_rt_Suc_forw) - apply (rule_tac x="a && x" in exI, auto) - apply (case_tac "xa=UU",auto) - apply (drule stream_exhaust_eq [THEN iffD1],auto) - apply (drule streams_prefix_lemma1,simp+) -by (simp add: sconc_def) - -lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x" -by (cases x, auto) - -lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z" -apply (case_tac "#x") - apply (rule stream_finite_ind [of x],auto simp del: scons_sconc) - apply (simp add: stream.finite_def del: scons_sconc) - apply (drule slen_take_lemma1,auto simp del: scons_sconc) - apply (case_tac "a = UU", auto) -by (simp add: sconc_def) - - -(* ----------------------------------------------------------------------- *) - -lemma cont_sconc_lemma1: "stream_finite x \ cont (\y. x ooo y)" -by (erule stream_finite_ind, simp_all) - -lemma cont_sconc_lemma2: "\ stream_finite x \ cont (\y. x ooo y)" -by (simp add: sconc_def slen_def) - -lemma cont_sconc: "cont (\y. x ooo y)" -apply (cases "stream_finite x") -apply (erule cont_sconc_lemma1) -apply (erule cont_sconc_lemma2) -done - -lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'" -by (rule cont_sconc [THEN cont2mono, THEN monofunE]) - -lemma sconc_mono1 [simp]: "x << x ooo y" -by (rule sconc_mono [of UU, simplified]) - -(* ----------------------------------------------------------------------- *) - -lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)" -apply (case_tac "#x",auto) - apply (insert sconc_mono1 [of x y]) - by auto - -(* ----------------------------------------------------------------------- *) - -lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x" -by (cases s, auto) - -lemma i_th_sconc_lemma [rule_format]: - "ALL x y. Fin n < #x --> i_th n (x ooo y) = i_th n x" -apply (induct_tac n, auto) -apply (simp add: Fin_0 i_th_def) -apply (simp add: slen_empty_eq ft_sconc) -apply (simp add: i_th_def) -apply (case_tac "x=UU",auto) -apply (drule stream_exhaust_eq [THEN iffD1], auto) -apply (erule_tac x="ya" in allE) -apply (case_tac "#ya") by simp_all - - - -(* ----------------------------------------------------------------------- *) - -lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s" -apply (induct_tac n,auto) -apply (case_tac "s=UU",auto) -by (drule stream_exhaust_eq [THEN iffD1],auto) - -(* ----------------------------------------------------------------------- *) - subsection "pointwise equality" -(* ----------------------------------------------------------------------- *) - -lemma ex_last_stream_take_scons: "stream_take (Suc n)$s = - stream_take n$s ooo i_rt n (stream_take (Suc n)$s)" -by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp) - -lemma i_th_stream_take_eq: -"!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2" -apply (induct_tac n,auto) -apply (subgoal_tac "stream_take (Suc na)$s1 = - stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)") - apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) = - i_rt na (stream_take (Suc na)$s2)") - apply (subgoal_tac "stream_take (Suc na)$s2 = - stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)") - apply (insert ex_last_stream_take_scons,simp) - apply blast - apply (erule_tac x="na" in allE) - apply (insert i_th_last_eq [of _ s1 s2]) -by blast+ - -lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2" -by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast) - -(* ----------------------------------------------------------------------- *) - subsection "finiteness" -(* ----------------------------------------------------------------------- *) - -lemma slen_sconc_finite1: - "[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty" -apply (case_tac "#y ~= Infty",auto) -apply (drule_tac y=y in rt_sconc1) -apply (insert stream_finite_i_rt [of n "x ooo y"]) -by (simp add: slen_infinite) - -lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty" -by (simp add: sconc_def) - -lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty" -apply (case_tac "#x") - apply (simp add: sconc_def) - apply (rule someI2_ex) - apply (drule ex_sconc,auto) - apply (erule contrapos_pp) - apply (insert stream_finite_i_rt) - apply (fastsimp simp add: slen_infinite,auto) -by (simp add: sconc_def) - -lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)" -apply auto - apply (metis not_Infty_eq slen_sconc_finite1) - apply (metis not_Infty_eq slen_sconc_infinite1) -apply (metis not_Infty_eq slen_sconc_infinite2) -done - -(* ----------------------------------------------------------------------- *) - -lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k" -apply (insert slen_mono [of "x" "x ooo y"]) -apply (cases "#x") apply simp_all -apply (cases "#(x ooo y)") apply simp_all -done - -(* ----------------------------------------------------------------------- *) - subsection "finite slen" -(* ----------------------------------------------------------------------- *) - -lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)" -apply (case_tac "#(x ooo y)") - apply (frule_tac y=y in rt_sconc1) - apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp) - apply (insert slen_sconc_mono3 [of n x _ y],simp) -by (insert sconc_finite [of x y],auto) - -(* ----------------------------------------------------------------------- *) - subsection "flat prefix" -(* ----------------------------------------------------------------------- *) - -lemma sconc_prefix: "(s1::'a::flat stream) << s2 ==> EX t. s1 ooo t = s2" -apply (case_tac "#s1") - apply (subgoal_tac "stream_take nat$s1 = stream_take nat$s2") - apply (rule_tac x="i_rt nat s2" in exI) - apply (simp add: sconc_def) - apply (rule someI2_ex) - apply (drule ex_sconc) - apply (simp,clarsimp,drule streams_prefix_lemma1) - apply (simp+,rule slen_take_lemma3 [of _ s1 s2]) - apply (simp+,rule_tac x="UU" in exI) -apply (insert slen_take_lemma3 [of _ s1 s2]) -by (rule stream.take_lemma,simp) - -(* ----------------------------------------------------------------------- *) - subsection "continuity" -(* ----------------------------------------------------------------------- *) - -lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))" -by (simp add: chain_def,auto simp add: sconc_mono) - -lemma chain_scons: "chain S ==> chain (%i. a && S i)" -apply (simp add: chain_def,auto) -by (rule monofun_cfun_arg,simp) - -lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)" -by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric]) - -lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> - (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" -apply (rule stream_finite_ind [of x]) - apply (auto) -apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)") - by (force,blast dest: contlub_scons_lemma chain_sconc) - -lemma contlub_sconc_lemma: - "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" -apply (case_tac "#x=Infty") - apply (simp add: sconc_def) -apply (drule finite_lub_sconc,auto simp add: slen_infinite) -done - -lemma monofun_sconc: "monofun (%y. x ooo y)" -by (simp add: monofun_def sconc_mono) - - -(* ----------------------------------------------------------------------- *) - section "constr_sconc" -(* ----------------------------------------------------------------------- *) - -lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s" -by (simp add: constr_sconc_def zero_inat_def) - -lemma "x ooo y = constr_sconc x y" -apply (case_tac "#x") - apply (rule stream_finite_ind [of x],auto simp del: scons_sconc) - defer 1 - apply (simp add: constr_sconc_def del: scons_sconc) - apply (case_tac "#s") - apply (simp add: iSuc_Fin) - apply (case_tac "a=UU",auto simp del: scons_sconc) - apply (simp) - apply (simp add: sconc_def) - apply (simp add: constr_sconc_def) -apply (simp add: stream.finite_def) -by (drule slen_take_lemma1,auto) - -end diff -r e67760c1b851 -r 7ffdbc24b27f src/HOLCF/ex/Strict_Fun.thy --- a/src/HOLCF/ex/Strict_Fun.thy Mon May 24 11:29:49 2010 -0700 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,239 +0,0 @@ -(* Title: HOLCF/ex/Strict_Fun.thy - Author: Brian Huffman -*) - -header {* The Strict Function Type *} - -theory Strict_Fun -imports HOLCF -begin - -pcpodef (open) ('a, 'b) sfun (infixr "->!" 0) - = "{f :: 'a \ 'b. f\\ = \}" -by simp_all - -type_notation (xsymbols) - sfun (infixr "\!" 0) - -text {* TODO: Define nice syntax for abstraction, application. *} - -definition - sfun_abs :: "('a \ 'b) \ ('a \! 'b)" -where - "sfun_abs = (\ f. Abs_sfun (strictify\f))" - -definition - sfun_rep :: "('a \! 'b) \ 'a \ 'b" -where - "sfun_rep = (\ f. Rep_sfun f)" - -lemma sfun_rep_beta: "sfun_rep\f = Rep_sfun f" - unfolding sfun_rep_def by (simp add: cont_Rep_sfun) - -lemma sfun_rep_strict1 [simp]: "sfun_rep\\ = \" - unfolding sfun_rep_beta by (rule Rep_sfun_strict) - -lemma sfun_rep_strict2 [simp]: "sfun_rep\f\\ = \" - unfolding sfun_rep_beta by (rule Rep_sfun [simplified]) - -lemma strictify_cancel: "f\\ = \ \ strictify\f = f" - by (simp add: expand_cfun_eq strictify_conv_if) - -lemma sfun_abs_sfun_rep: "sfun_abs\(sfun_rep\f) = f" - unfolding sfun_abs_def sfun_rep_def - apply (simp add: cont_Abs_sfun cont_Rep_sfun) - apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse) - apply (simp add: expand_cfun_eq strictify_conv_if) - apply (simp add: Rep_sfun [simplified]) - done - -lemma sfun_rep_sfun_abs [simp]: "sfun_rep\(sfun_abs\f) = strictify\f" - unfolding sfun_abs_def sfun_rep_def - apply (simp add: cont_Abs_sfun cont_Rep_sfun) - apply (simp add: Abs_sfun_inverse) - done - -lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs" -apply default -apply (rule sfun_abs_sfun_rep) -apply (simp add: expand_cfun_below strictify_conv_if) -done - -interpretation sfun: ep_pair sfun_rep sfun_abs - by (rule ep_pair_sfun) - -subsection {* Map functional for strict function space *} - -definition - sfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \! 'c) \ ('b \! 'd)" -where - "sfun_map = (\ a b. sfun_abs oo cfun_map\a\b oo sfun_rep)" - -lemma sfun_map_ID: "sfun_map\ID\ID = ID" - unfolding sfun_map_def - by (simp add: cfun_map_ID expand_cfun_eq) - -lemma sfun_map_map: - assumes "f2\\ = \" and "g2\\ = \" shows - "sfun_map\f1\g1\(sfun_map\f2\g2\p) = - sfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" -unfolding sfun_map_def -by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map) - -lemma ep_pair_sfun_map: - assumes 1: "ep_pair e1 p1" - assumes 2: "ep_pair e2 p2" - shows "ep_pair (sfun_map\p1\e2) (sfun_map\e1\p2)" -proof - interpret e1p1: pcpo_ep_pair e1 p1 - unfolding pcpo_ep_pair_def by fact - interpret e2p2: pcpo_ep_pair e2 p2 - unfolding pcpo_ep_pair_def by fact - fix f show "sfun_map\e1\p2\(sfun_map\p1\e2\f) = f" - unfolding sfun_map_def - apply (simp add: sfun.e_eq_iff [symmetric] strictify_cancel) - apply (rule ep_pair.e_inverse) - apply (rule ep_pair_cfun_map [OF 1 2]) - done - fix g show "sfun_map\p1\e2\(sfun_map\e1\p2\g) \ g" - unfolding sfun_map_def - apply (simp add: sfun.e_below_iff [symmetric] strictify_cancel) - apply (rule ep_pair.e_p_below) - apply (rule ep_pair_cfun_map [OF 1 2]) - done -qed - -lemma deflation_sfun_map: - assumes 1: "deflation d1" - assumes 2: "deflation d2" - shows "deflation (sfun_map\d1\d2)" -apply (simp add: sfun_map_def) -apply (rule deflation.intro) -apply simp -apply (subst strictify_cancel) -apply (simp add: cfun_map_def deflation_strict 1 2) -apply (simp add: cfun_map_def deflation.idem 1 2) -apply (simp add: sfun.e_below_iff [symmetric]) -apply (subst strictify_cancel) -apply (simp add: cfun_map_def deflation_strict 1 2) -apply (rule deflation.below) -apply (rule deflation_cfun_map [OF 1 2]) -done - -lemma finite_deflation_sfun_map: - assumes 1: "finite_deflation d1" - assumes 2: "finite_deflation d2" - shows "finite_deflation (sfun_map\d1\d2)" -proof (intro finite_deflation.intro finite_deflation_axioms.intro) - interpret d1: finite_deflation d1 by fact - interpret d2: finite_deflation d2 by fact - have "deflation d1" and "deflation d2" by fact+ - thus "deflation (sfun_map\d1\d2)" by (rule deflation_sfun_map) - from 1 2 have "finite_deflation (cfun_map\d1\d2)" - by (rule finite_deflation_cfun_map) - then have "finite {f. cfun_map\d1\d2\f = f}" - by (rule finite_deflation.finite_fixes) - moreover have "inj (\f. sfun_rep\f)" - by (rule inj_onI, simp) - ultimately have "finite ((\f. sfun_rep\f) -` {f. cfun_map\d1\d2\f = f})" - by (rule finite_vimageI) - then show "finite {f. sfun_map\d1\d2\f = f}" - unfolding sfun_map_def sfun.e_eq_iff [symmetric] - by (simp add: strictify_cancel - deflation_strict `deflation d1` `deflation d2`) -qed - -subsection {* Strict function space is bifinite *} - -instantiation sfun :: (bifinite, bifinite) bifinite -begin - -definition - "approx = (\i. sfun_map\(approx i)\(approx i))" - -instance proof - show "chain (approx :: nat \ ('a \! 'b) \ ('a \! 'b))" - unfolding approx_sfun_def by simp -next - fix x :: "'a \! 'b" - show "(\i. approx i\x) = x" - unfolding approx_sfun_def - by (simp add: lub_distribs sfun_map_ID [unfolded ID_def]) -next - fix i :: nat and x :: "'a \! 'b" - show "approx i\(approx i\x) = approx i\x" - unfolding approx_sfun_def - by (intro deflation.idem deflation_sfun_map deflation_approx) -next - fix i :: nat - show "finite {x::'a \! 'b. approx i\x = x}" - unfolding approx_sfun_def - by (intro finite_deflation.finite_fixes - finite_deflation_sfun_map - finite_deflation_approx) -qed - -end - -subsection {* Strict function space is representable *} - -instantiation sfun :: (rep, rep) rep -begin - -definition - "emb = udom_emb oo sfun_map\prj\emb" - -definition - "prj = sfun_map\emb\prj oo udom_prj" - -instance -apply (default, unfold emb_sfun_def prj_sfun_def) -apply (rule ep_pair_comp) -apply (rule ep_pair_sfun_map) -apply (rule ep_pair_emb_prj) -apply (rule ep_pair_emb_prj) -apply (rule ep_pair_udom) -done - -end - -text {* - A deflation constructor lets us configure the domain package to work - with the strict function space type constructor. -*} - -definition - sfun_defl :: "TypeRep \ TypeRep \ TypeRep" -where - "sfun_defl = TypeRep_fun2 sfun_map" - -lemma cast_sfun_defl: - "cast\(sfun_defl\A\B) = udom_emb oo sfun_map\(cast\A)\(cast\B) oo udom_prj" -unfolding sfun_defl_def -apply (rule cast_TypeRep_fun2) -apply (erule (1) finite_deflation_sfun_map) -done - -lemma REP_sfun: "REP('a::rep \! 'b::rep) = sfun_defl\REP('a)\REP('b)" -apply (rule cast_eq_imp_eq, rule ext_cfun) -apply (simp add: cast_REP cast_sfun_defl) -apply (simp only: prj_sfun_def emb_sfun_def) -apply (simp add: sfun_map_def cfun_map_def strictify_cancel) -done - -lemma isodefl_sfun: - "isodefl d1 t1 \ isodefl d2 t2 \ - isodefl (sfun_map\d1\d2) (sfun_defl\t1\t2)" -apply (rule isodeflI) -apply (simp add: cast_sfun_defl cast_isodefl) -apply (simp add: emb_sfun_def prj_sfun_def) -apply (simp add: sfun_map_map deflation_strict [OF isodefl_imp_deflation]) -done - -setup {* - Domain_Isomorphism.add_type_constructor - (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm REP_sfun}, - @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map}) -*} - -end