3 *) |
3 *) |
4 |
4 |
5 header {* Representable Types *} |
5 header {* Representable Types *} |
6 |
6 |
7 theory Representable |
7 theory Representable |
8 imports Algebraic Universal Ssum Sprod One Fixrec |
8 imports Algebraic Universal Ssum Sprod One Fixrec Domain_Aux |
9 uses |
9 uses |
10 ("Tools/repdef.ML") |
10 ("Tools/repdef.ML") |
11 ("Tools/Domain/domain_take_proofs.ML") |
|
12 ("Tools/Domain/domain_isomorphism.ML") |
11 ("Tools/Domain/domain_isomorphism.ML") |
13 begin |
12 begin |
14 |
|
15 subsection {* Preliminaries: Take proofs *} |
|
16 |
|
17 text {* |
|
18 This section contains lemmas that are used in a module that supports |
|
19 the domain isomorphism package; the module contains proofs related |
|
20 to take functions and the finiteness predicate. |
|
21 *} |
|
22 |
|
23 lemma deflation_abs_rep: |
|
24 fixes abs and rep and d |
|
25 assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" |
|
26 assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" |
|
27 shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" |
|
28 by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) |
|
29 |
|
30 lemma deflation_chain_min: |
|
31 assumes chain: "chain d" |
|
32 assumes defl: "\<And>n. deflation (d n)" |
|
33 shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x" |
|
34 proof (rule linorder_le_cases) |
|
35 assume "m \<le> n" |
|
36 with chain have "d m \<sqsubseteq> d n" by (rule chain_mono) |
|
37 then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x" |
|
38 by (rule deflation_below_comp1 [OF defl defl]) |
|
39 moreover from `m \<le> n` have "min m n = m" by simp |
|
40 ultimately show ?thesis by simp |
|
41 next |
|
42 assume "n \<le> m" |
|
43 with chain have "d n \<sqsubseteq> d m" by (rule chain_mono) |
|
44 then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x" |
|
45 by (rule deflation_below_comp2 [OF defl defl]) |
|
46 moreover from `n \<le> m` have "min m n = n" by simp |
|
47 ultimately show ?thesis by simp |
|
48 qed |
|
49 |
|
50 use "Tools/Domain/domain_take_proofs.ML" |
|
51 |
|
52 |
13 |
53 subsection {* Class of representable types *} |
14 subsection {* Class of representable types *} |
54 |
15 |
55 text "Overloaded embedding and projection functions between |
16 text "Overloaded embedding and projection functions between |
56 a representable type and the universal domain." |
17 a representable type and the universal domain." |