27 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
27 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
28 apply (erule (1) antisym_less) |
28 apply (erule (1) antisym_less) |
29 apply (erule (1) trans_less) |
29 apply (erule (1) trans_less) |
30 done |
30 done |
31 |
31 |
|
32 |
|
33 subsection {* Proving a subtype is finite *} |
|
34 |
|
35 context type_definition |
|
36 begin |
|
37 |
|
38 lemma Abs_image: |
|
39 shows "Abs ` A = UNIV" |
|
40 proof |
|
41 show "Abs ` A <= UNIV" by simp |
|
42 show "UNIV <= Abs ` A" |
|
43 proof |
|
44 fix x |
|
45 have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) |
|
46 thus "x : Abs ` A" using Rep by (rule image_eqI) |
|
47 qed |
|
48 qed |
|
49 |
|
50 lemma finite_UNIV: "finite A \<Longrightarrow> finite (UNIV :: 'b set)" |
|
51 proof - |
|
52 assume "finite A" |
|
53 hence "finite (Abs ` A)" by (rule finite_imageI) |
|
54 thus "finite (UNIV :: 'b set)" by (simp only: Abs_image) |
|
55 qed |
|
56 |
|
57 end |
|
58 |
|
59 theorem typedef_finite_po: |
|
60 fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po" |
|
61 assumes type: "type_definition Rep Abs A" |
|
62 shows "OFCLASS('b, finite_po_class)" |
|
63 apply (intro_classes) |
|
64 apply (rule type_definition.finite_UNIV [OF type]) |
|
65 apply (rule finite) |
|
66 done |
32 |
67 |
33 subsection {* Proving a subtype is chain-finite *} |
68 subsection {* Proving a subtype is chain-finite *} |
34 |
69 |
35 lemma monofun_Rep: |
70 lemma monofun_Rep: |
36 assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
71 assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |