38 by (simp add: csplit_def) |
38 by (simp add: csplit_def) |
39 |
39 |
40 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y" |
40 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y" |
41 by (simp add: csplit_def) |
41 by (simp add: csplit_def) |
42 |
42 |
|
43 subsection {* Cartesian product is an SFP domain *} |
|
44 |
|
45 definition |
|
46 prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom" |
|
47 where |
|
48 "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
|
49 |
|
50 lemma prod_approx: "approx_chain prod_approx" |
|
51 proof (rule approx_chain.intro) |
|
52 show "chain (\<lambda>i. prod_approx i)" |
|
53 unfolding prod_approx_def by simp |
|
54 show "(\<Squnion>i. prod_approx i) = ID" |
|
55 unfolding prod_approx_def |
|
56 by (simp add: lub_distribs cprod_map_ID) |
|
57 show "\<And>i. finite_deflation (prod_approx i)" |
|
58 unfolding prod_approx_def |
|
59 by (intro finite_deflation_cprod_map finite_deflation_udom_approx) |
|
60 qed |
|
61 |
|
62 definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp" |
|
63 where "prod_sfp = sfp_fun2 prod_approx cprod_map" |
|
64 |
|
65 lemma cast_prod_sfp: |
|
66 "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo |
|
67 cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx" |
|
68 unfolding prod_sfp_def |
|
69 apply (rule cast_sfp_fun2 [OF prod_approx]) |
|
70 apply (erule (1) finite_deflation_cprod_map) |
|
71 done |
|
72 |
|
73 instantiation prod :: (sfp, sfp) sfp |
|
74 begin |
|
75 |
|
76 definition |
|
77 "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb" |
|
78 |
|
79 definition |
|
80 "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx" |
|
81 |
|
82 definition |
|
83 "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
|
84 |
|
85 instance proof |
|
86 show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)" |
|
87 unfolding emb_prod_def prj_prod_def |
|
88 using ep_pair_udom [OF prod_approx] |
|
89 by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj) |
|
90 next |
|
91 show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)" |
|
92 unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp |
|
93 by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map) |
|
94 qed |
|
95 |
43 end |
96 end |
|
97 |
|
98 lemma SFP_prod: "SFP('a::sfp \<times> 'b::sfp) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)" |
|
99 by (rule sfp_prod_def) |
|
100 |
|
101 end |