author | huffman |
Thu, 21 Oct 2010 15:21:39 -0700 | |
changeset 40086 | c339c0e8fdfb |
parent 40012 | f13341a45407 |
child 40484 | 768f7e264e2b |
permissions | -rw-r--r-- |
25903 | 1 |
(* Title: HOLCF/Bifinite.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
5 |
header {* Bifinite domains *} |
25903 | 6 |
|
7 |
theory Bifinite |
|
40086 | 8 |
imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable |
25903 | 9 |
begin |
10 |
||
39986 | 11 |
subsection {* Class of bifinite domains *} |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
12 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
13 |
text {* |
39986 | 14 |
We define a bifinite domain as a pcpo that is isomorphic to some |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
15 |
algebraic deflation over the universal domain. |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
16 |
*} |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
17 |
|
39986 | 18 |
class bifinite = pcpo + |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
19 |
fixes emb :: "'a::pcpo \<rightarrow> udom" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
20 |
fixes prj :: "udom \<rightarrow> 'a::pcpo" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
21 |
fixes defl :: "'a itself \<Rightarrow> defl" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
22 |
assumes ep_pair_emb_prj: "ep_pair emb prj" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
23 |
assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj" |
31113
15cf300a742f
move bifinite instance for product type from Cprod.thy to Bifinite.thy
huffman
parents:
31076
diff
changeset
|
24 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
25 |
syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))") |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
26 |
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
27 |
|
39986 | 28 |
interpretation bifinite: |
29 |
pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite" |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
30 |
unfolding pcpo_ep_pair_def |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
31 |
by (rule ep_pair_emb_prj) |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
32 |
|
39986 | 33 |
lemmas emb_inverse = bifinite.e_inverse |
34 |
lemmas emb_prj_below = bifinite.e_p_below |
|
35 |
lemmas emb_eq_iff = bifinite.e_eq_iff |
|
36 |
lemmas emb_strict = bifinite.e_strict |
|
37 |
lemmas prj_strict = bifinite.p_strict |
|
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
38 |
|
39986 | 39 |
subsection {* Bifinite domains have a countable compact basis *} |
33808 | 40 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
41 |
text {* |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
42 |
Eventually it should be possible to generalize this to an unpointed |
39986 | 43 |
variant of the bifinite class. |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
44 |
*} |
33587 | 45 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
46 |
interpretation compact_basis: |
39986 | 47 |
ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
48 |
proof - |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
49 |
obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
50 |
and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
51 |
by (rule defl.obtain_principal_chain) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
52 |
def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
53 |
interpret defl_approx: approx_chain approx |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
54 |
proof (rule approx_chain.intro) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
55 |
show "chain (\<lambda>i. approx i)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
56 |
unfolding approx_def by (simp add: Y) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
57 |
show "(\<Squnion>i. approx i) = ID" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
58 |
unfolding approx_def |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
59 |
by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
60 |
show "\<And>i. finite_deflation (approx i)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
61 |
unfolding approx_def |
39986 | 62 |
apply (rule bifinite.finite_deflation_p_d_e) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
63 |
apply (rule finite_deflation_cast) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
64 |
apply (rule defl.compact_principal) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
65 |
apply (rule below_trans [OF monofun_cfun_fun]) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
66 |
apply (rule is_ub_thelub, simp add: Y) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
67 |
apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
68 |
done |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
69 |
qed |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
70 |
(* FIXME: why does show ?thesis fail here? *) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
71 |
show "ideal_completion below Rep_compact_basis (approximants::'a \<Rightarrow> _)" .. |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
72 |
qed |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
73 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
74 |
subsection {* Type combinators *} |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
75 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
76 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
77 |
defl_fun1 :: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
78 |
"(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) \<Rightarrow> (defl \<rightarrow> defl)" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
79 |
where |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
80 |
"defl_fun1 approx f = |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
81 |
defl.basis_fun (\<lambda>a. |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
82 |
defl_principal (Abs_fin_defl |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
83 |
(udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)))" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
84 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
85 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
86 |
defl_fun2 :: |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
87 |
"(nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ((udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom) \<rightarrow> ('a \<rightarrow> 'a)) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
88 |
\<Rightarrow> (defl \<rightarrow> defl \<rightarrow> defl)" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
89 |
where |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
90 |
"defl_fun2 approx f = |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
91 |
defl.basis_fun (\<lambda>a. |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
92 |
defl.basis_fun (\<lambda>b. |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
93 |
defl_principal (Abs_fin_defl |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
94 |
(udom_emb approx oo |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
95 |
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx))))" |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
96 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
97 |
lemma cast_defl_fun1: |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
98 |
assumes approx: "approx_chain approx" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
99 |
assumes f: "\<And>a. finite_deflation a \<Longrightarrow> finite_deflation (f\<cdot>a)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
100 |
shows "cast\<cdot>(defl_fun1 approx f\<cdot>A) = udom_emb approx oo f\<cdot>(cast\<cdot>A) oo udom_prj approx" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
101 |
proof - |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
102 |
have 1: "\<And>a. finite_deflation |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
103 |
(udom_emb approx oo f\<cdot>(Rep_fin_defl a) oo udom_prj approx)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
104 |
apply (rule ep_pair.finite_deflation_e_d_p) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
105 |
apply (rule approx_chain.ep_pair_udom [OF approx]) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
106 |
apply (rule f, rule finite_deflation_Rep_fin_defl) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
107 |
done |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
108 |
show ?thesis |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
109 |
by (induct A rule: defl.principal_induct, simp) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
110 |
(simp only: defl_fun1_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
111 |
defl.basis_fun_principal |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
112 |
defl.basis_fun_mono |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
113 |
defl.principal_mono |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
114 |
Abs_fin_defl_mono [OF 1 1] |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
115 |
monofun_cfun below_refl |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
116 |
Rep_fin_defl_mono |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
117 |
cast_defl_principal |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
118 |
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
119 |
qed |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
120 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
121 |
lemma cast_defl_fun2: |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
122 |
assumes approx: "approx_chain approx" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
123 |
assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow> |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
124 |
finite_deflation (f\<cdot>a\<cdot>b)" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
125 |
shows "cast\<cdot>(defl_fun2 approx f\<cdot>A\<cdot>B) = |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
126 |
udom_emb approx oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj approx" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
127 |
proof - |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
128 |
have 1: "\<And>a b. finite_deflation (udom_emb approx oo |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
129 |
f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj approx)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
130 |
apply (rule ep_pair.finite_deflation_e_d_p) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
131 |
apply (rule ep_pair_udom [OF approx]) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
132 |
apply (rule f, (rule finite_deflation_Rep_fin_defl)+) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
133 |
done |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
134 |
show ?thesis |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
135 |
by (induct A B rule: defl.principal_induct2, simp, simp) |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
136 |
(simp only: defl_fun2_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
137 |
defl.basis_fun_principal |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
138 |
defl.basis_fun_mono |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
139 |
defl.principal_mono |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
140 |
Abs_fin_defl_mono [OF 1 1] |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
141 |
monofun_cfun below_refl |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
142 |
Rep_fin_defl_mono |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
143 |
cast_defl_principal |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
144 |
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1]) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
145 |
qed |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
146 |
|
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
147 |
subsection {* The universal domain is bifinite *} |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
148 |
|
39986 | 149 |
instantiation udom :: bifinite |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
150 |
begin |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
151 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
152 |
definition [simp]: |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
153 |
"emb = (ID :: udom \<rightarrow> udom)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
154 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
155 |
definition [simp]: |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
156 |
"prj = (ID :: udom \<rightarrow> udom)" |
25903 | 157 |
|
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
158 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
159 |
"defl (t::udom itself) = (\<Squnion>i. defl_principal (Abs_fin_defl (udom_approx i)))" |
33808 | 160 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
161 |
instance proof |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
162 |
show "ep_pair emb (prj :: udom \<rightarrow> udom)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
163 |
by (simp add: ep_pair.intro) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
164 |
next |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
165 |
show "cast\<cdot>DEFL(udom) = emb oo (prj :: udom \<rightarrow> udom)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
166 |
unfolding defl_udom_def |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
167 |
apply (subst contlub_cfun_arg) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
168 |
apply (rule chainI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
169 |
apply (rule defl.principal_mono) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
170 |
apply (simp add: below_fin_defl_def) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
171 |
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
172 |
apply (rule chainE) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
173 |
apply (rule chain_udom_approx) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
174 |
apply (subst cast_defl_principal) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
175 |
apply (simp add: Abs_fin_defl_inverse finite_deflation_udom_approx) |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
176 |
done |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
177 |
qed |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
178 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
179 |
end |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
180 |
|
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
181 |
subsection {* Continuous function space is a bifinite domain *} |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
182 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
183 |
definition |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
184 |
cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
185 |
where |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
186 |
"cfun_approx = (\<lambda>i. cfun_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
187 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
188 |
lemma cfun_approx: "approx_chain cfun_approx" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
189 |
proof (rule approx_chain.intro) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
190 |
show "chain (\<lambda>i. cfun_approx i)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
191 |
unfolding cfun_approx_def by simp |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
192 |
show "(\<Squnion>i. cfun_approx i) = ID" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
193 |
unfolding cfun_approx_def |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
194 |
by (simp add: lub_distribs cfun_map_ID) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
195 |
show "\<And>i. finite_deflation (cfun_approx i)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
196 |
unfolding cfun_approx_def |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
197 |
by (intro finite_deflation_cfun_map finite_deflation_udom_approx) |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
198 |
qed |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
199 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
200 |
definition cfun_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
201 |
where "cfun_defl = defl_fun2 cfun_approx cfun_map" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
202 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
203 |
lemma cast_cfun_defl: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
204 |
"cast\<cdot>(cfun_defl\<cdot>A\<cdot>B) = |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
205 |
udom_emb cfun_approx oo cfun_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj cfun_approx" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
206 |
unfolding cfun_defl_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
207 |
apply (rule cast_defl_fun2 [OF cfun_approx]) |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
208 |
apply (erule (1) finite_deflation_cfun_map) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
209 |
done |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
210 |
|
39986 | 211 |
instantiation cfun :: (bifinite, bifinite) bifinite |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
212 |
begin |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
213 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
214 |
definition |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
215 |
"emb = udom_emb cfun_approx oo cfun_map\<cdot>prj\<cdot>emb" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
216 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
217 |
definition |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
218 |
"prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj cfun_approx" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
219 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
220 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
221 |
"defl (t::('a \<rightarrow> 'b) itself) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
222 |
|
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
223 |
instance proof |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
224 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
225 |
unfolding emb_cfun_def prj_cfun_def |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
226 |
using ep_pair_udom [OF cfun_approx] |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
227 |
by (intro ep_pair_comp ep_pair_cfun_map ep_pair_emb_prj) |
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
228 |
next |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
229 |
show "cast\<cdot>DEFL('a \<rightarrow> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow> 'b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
230 |
unfolding emb_cfun_def prj_cfun_def defl_cfun_def cast_cfun_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
231 |
by (simp add: cast_DEFL oo_def cfun_eq_iff cfun_map_map) |
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset
|
232 |
qed |
25903 | 233 |
|
39985
310f98585107
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman
parents:
39974
diff
changeset
|
234 |
end |
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
31113
diff
changeset
|
235 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
236 |
lemma DEFL_cfun: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
237 |
"DEFL('a::bifinite \<rightarrow> 'b::bifinite) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
238 |
by (rule defl_cfun_def) |
39972
4244ff4f9649
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
Brian Huffman <brianh@cs.pdx.edu>
parents:
37678
diff
changeset
|
239 |
|
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
240 |
subsection {* Cartesian product is a bifinite domain *} |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
241 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
242 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
243 |
prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
244 |
where |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
245 |
"prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
246 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
247 |
lemma prod_approx: "approx_chain prod_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
248 |
proof (rule approx_chain.intro) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
249 |
show "chain (\<lambda>i. prod_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
250 |
unfolding prod_approx_def by simp |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
251 |
show "(\<Squnion>i. prod_approx i) = ID" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
252 |
unfolding prod_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
253 |
by (simp add: lub_distribs cprod_map_ID) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
254 |
show "\<And>i. finite_deflation (prod_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
255 |
unfolding prod_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
256 |
by (intro finite_deflation_cprod_map finite_deflation_udom_approx) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
257 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
258 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
259 |
definition prod_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
260 |
where "prod_defl = defl_fun2 prod_approx cprod_map" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
261 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
262 |
lemma cast_prod_defl: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
263 |
"cast\<cdot>(prod_defl\<cdot>A\<cdot>B) = udom_emb prod_approx oo |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
264 |
cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
265 |
unfolding prod_defl_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
266 |
apply (rule cast_defl_fun2 [OF prod_approx]) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
267 |
apply (erule (1) finite_deflation_cprod_map) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
268 |
done |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
269 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
270 |
instantiation prod :: (bifinite, bifinite) bifinite |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
271 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
272 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
273 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
274 |
"emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
275 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
276 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
277 |
"prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
278 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
279 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
280 |
"defl (t::('a \<times> 'b) itself) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
281 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
282 |
instance proof |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
283 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
284 |
unfolding emb_prod_def prj_prod_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
285 |
using ep_pair_udom [OF prod_approx] |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
286 |
by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
287 |
next |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
288 |
show "cast\<cdot>DEFL('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
289 |
unfolding emb_prod_def prj_prod_def defl_prod_def cast_prod_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
290 |
by (simp add: cast_DEFL oo_def cfun_eq_iff cprod_map_map) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
291 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
292 |
|
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset
|
293 |
end |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
294 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
295 |
lemma DEFL_prod: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
296 |
"DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
297 |
by (rule defl_prod_def) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
298 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
299 |
subsection {* Strict product is a bifinite domain *} |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
300 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
301 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
302 |
sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
303 |
where |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
304 |
"sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
305 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
306 |
lemma sprod_approx: "approx_chain sprod_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
307 |
proof (rule approx_chain.intro) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
308 |
show "chain (\<lambda>i. sprod_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
309 |
unfolding sprod_approx_def by simp |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
310 |
show "(\<Squnion>i. sprod_approx i) = ID" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
311 |
unfolding sprod_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
312 |
by (simp add: lub_distribs sprod_map_ID) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
313 |
show "\<And>i. finite_deflation (sprod_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
314 |
unfolding sprod_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
315 |
by (intro finite_deflation_sprod_map finite_deflation_udom_approx) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
316 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
317 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
318 |
definition sprod_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
319 |
where "sprod_defl = defl_fun2 sprod_approx sprod_map" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
320 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
321 |
lemma cast_sprod_defl: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
322 |
"cast\<cdot>(sprod_defl\<cdot>A\<cdot>B) = |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
323 |
udom_emb sprod_approx oo |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
324 |
sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
325 |
udom_prj sprod_approx" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
326 |
unfolding sprod_defl_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
327 |
apply (rule cast_defl_fun2 [OF sprod_approx]) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
328 |
apply (erule (1) finite_deflation_sprod_map) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
329 |
done |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
330 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
331 |
instantiation sprod :: (bifinite, bifinite) bifinite |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
332 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
333 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
334 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
335 |
"emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
336 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
337 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
338 |
"prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
339 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
340 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
341 |
"defl (t::('a \<otimes> 'b) itself) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
342 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
343 |
instance proof |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
344 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
345 |
unfolding emb_sprod_def prj_sprod_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
346 |
using ep_pair_udom [OF sprod_approx] |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
347 |
by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
348 |
next |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
349 |
show "cast\<cdot>DEFL('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
350 |
unfolding emb_sprod_def prj_sprod_def defl_sprod_def cast_sprod_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
351 |
by (simp add: cast_DEFL oo_def cfun_eq_iff sprod_map_map) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
352 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
353 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
354 |
end |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
355 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
356 |
lemma DEFL_sprod: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
357 |
"DEFL('a::bifinite \<otimes> 'b::bifinite) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
358 |
by (rule defl_sprod_def) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
359 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
360 |
subsection {* Lifted cpo is a bifinite domain *} |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
361 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
362 |
definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
363 |
where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
364 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
365 |
lemma u_approx: "approx_chain u_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
366 |
proof (rule approx_chain.intro) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
367 |
show "chain (\<lambda>i. u_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
368 |
unfolding u_approx_def by simp |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
369 |
show "(\<Squnion>i. u_approx i) = ID" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
370 |
unfolding u_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
371 |
by (simp add: lub_distribs u_map_ID) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
372 |
show "\<And>i. finite_deflation (u_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
373 |
unfolding u_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
374 |
by (intro finite_deflation_u_map finite_deflation_udom_approx) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
375 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
376 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
377 |
definition u_defl :: "defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
378 |
where "u_defl = defl_fun1 u_approx u_map" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
379 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
380 |
lemma cast_u_defl: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
381 |
"cast\<cdot>(u_defl\<cdot>A) = |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
382 |
udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
383 |
unfolding u_defl_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
384 |
apply (rule cast_defl_fun1 [OF u_approx]) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
385 |
apply (erule finite_deflation_u_map) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
386 |
done |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
387 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
388 |
instantiation u :: (bifinite) bifinite |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
389 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
390 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
391 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
392 |
"emb = udom_emb u_approx oo u_map\<cdot>emb" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
393 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
394 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
395 |
"prj = u_map\<cdot>prj oo udom_prj u_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
396 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
397 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
398 |
"defl (t::'a u itself) = u_defl\<cdot>DEFL('a)" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
399 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
400 |
instance proof |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
401 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a u)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
402 |
unfolding emb_u_def prj_u_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
403 |
using ep_pair_udom [OF u_approx] |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
404 |
by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
405 |
next |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
406 |
show "cast\<cdot>DEFL('a u) = emb oo (prj :: udom \<rightarrow> 'a u)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
407 |
unfolding emb_u_def prj_u_def defl_u_def cast_u_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
408 |
by (simp add: cast_DEFL oo_def cfun_eq_iff u_map_map) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
409 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
410 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
411 |
end |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
412 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
413 |
lemma DEFL_u: "DEFL('a::bifinite u) = u_defl\<cdot>DEFL('a)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
414 |
by (rule defl_u_def) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
415 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
416 |
subsection {* Lifted countable types are bifinite domains *} |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
417 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
418 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
419 |
lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
420 |
where |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
421 |
"lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
422 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
423 |
lemma chain_lift_approx [simp]: "chain lift_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
424 |
unfolding lift_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
425 |
by (rule chainI, simp add: FLIFT_mono) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
426 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
427 |
lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID" |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
428 |
apply (rule cfun_eqI) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
429 |
apply (simp add: contlub_cfun_fun) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
430 |
apply (simp add: lift_approx_def) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
431 |
apply (case_tac x, simp) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
432 |
apply (rule thelubI) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
433 |
apply (rule is_lubI) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
434 |
apply (rule ub_rangeI, simp) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
435 |
apply (drule ub_rangeD) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
436 |
apply (erule rev_below_trans) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
437 |
apply simp |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
438 |
apply (rule lessI) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
439 |
done |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
440 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
441 |
lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
442 |
proof |
40012 | 443 |
fix x :: "'a lift" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
444 |
show "lift_approx i\<cdot>x \<sqsubseteq> x" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
445 |
unfolding lift_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
446 |
by (cases x, simp, simp) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
447 |
show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
448 |
unfolding lift_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
449 |
by (cases x, simp, simp) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
450 |
show "finite {x::'a lift. lift_approx i\<cdot>x = x}" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
451 |
proof (rule finite_subset) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
452 |
let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
453 |
show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
454 |
unfolding lift_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
455 |
by (rule subsetI, case_tac x, simp, simp split: split_if_asm) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
456 |
show "finite ?S" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
457 |
by (simp add: finite_vimageI) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
458 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
459 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
460 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
461 |
lemma lift_approx: "approx_chain lift_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
462 |
using chain_lift_approx lub_lift_approx finite_deflation_lift_approx |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
463 |
by (rule approx_chain.intro) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
464 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
465 |
instantiation lift :: (countable) bifinite |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
466 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
467 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
468 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
469 |
"emb = udom_emb lift_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
470 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
471 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
472 |
"prj = udom_prj lift_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
473 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
474 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
475 |
"defl (t::'a lift itself) = |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
476 |
(\<Squnion>i. defl_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
477 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
478 |
instance proof |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
479 |
show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
480 |
unfolding emb_lift_def prj_lift_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
481 |
by (rule ep_pair_udom [OF lift_approx]) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
482 |
show "cast\<cdot>DEFL('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
483 |
unfolding defl_lift_def |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
484 |
apply (subst contlub_cfun_arg) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
485 |
apply (rule chainI) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
486 |
apply (rule defl.principal_mono) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
487 |
apply (simp add: below_fin_defl_def) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
488 |
apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
489 |
ep_pair.finite_deflation_e_d_p [OF ep]) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
490 |
apply (intro monofun_cfun below_refl) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
491 |
apply (rule chainE) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
492 |
apply (rule chain_lift_approx) |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
493 |
apply (subst cast_defl_principal) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
494 |
apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
495 |
ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
496 |
done |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
497 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
498 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
499 |
end |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
500 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
501 |
subsection {* Strict sum is a bifinite domain *} |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
502 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
503 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
504 |
ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
505 |
where |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
506 |
"ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
507 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
508 |
lemma ssum_approx: "approx_chain ssum_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
509 |
proof (rule approx_chain.intro) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
510 |
show "chain (\<lambda>i. ssum_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
511 |
unfolding ssum_approx_def by simp |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
512 |
show "(\<Squnion>i. ssum_approx i) = ID" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
513 |
unfolding ssum_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
514 |
by (simp add: lub_distribs ssum_map_ID) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
515 |
show "\<And>i. finite_deflation (ssum_approx i)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
516 |
unfolding ssum_approx_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
517 |
by (intro finite_deflation_ssum_map finite_deflation_udom_approx) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
518 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
519 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
520 |
definition ssum_defl :: "defl \<rightarrow> defl \<rightarrow> defl" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
521 |
where "ssum_defl = defl_fun2 ssum_approx ssum_map" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
522 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
523 |
lemma cast_ssum_defl: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
524 |
"cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
525 |
udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx" |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
526 |
unfolding ssum_defl_def |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
527 |
apply (rule cast_defl_fun2 [OF ssum_approx]) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
528 |
apply (erule (1) finite_deflation_ssum_map) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
529 |
done |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
530 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
531 |
instantiation ssum :: (bifinite, bifinite) bifinite |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
532 |
begin |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
533 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
534 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
535 |
"emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
536 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
537 |
definition |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
538 |
"prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
539 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
540 |
definition |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
541 |
"defl (t::('a \<oplus> 'b) itself) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
542 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
543 |
instance proof |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
544 |
show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
545 |
unfolding emb_ssum_def prj_ssum_def |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
546 |
using ep_pair_udom [OF ssum_approx] |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
547 |
by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj) |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
548 |
next |
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
549 |
show "cast\<cdot>DEFL('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
550 |
unfolding emb_ssum_def prj_ssum_def defl_ssum_def cast_ssum_defl |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39989
diff
changeset
|
551 |
by (simp add: cast_DEFL oo_def cfun_eq_iff ssum_map_map) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
552 |
qed |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
553 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
554 |
end |
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
555 |
|
39989
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
556 |
lemma DEFL_ssum: |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
557 |
"DEFL('a::bifinite \<oplus> 'b::bifinite) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
ad60d7311f43
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
huffman
parents:
39987
diff
changeset
|
558 |
by (rule defl_ssum_def) |
39987
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
559 |
|
8c2f449af35a
move all bifinite class instances to Bifinite.thy
huffman
parents:
39986
diff
changeset
|
560 |
end |