15 text {* |
15 text {* |
16 A subtype of a partial order is itself a partial order, |
16 A subtype of a partial order is itself a partial order, |
17 if the ordering is defined in the standard way. |
17 if the ordering is defined in the standard way. |
18 *} |
18 *} |
19 |
19 |
|
20 setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, NONE) *} |
|
21 |
20 theorem typedef_po: |
22 theorem typedef_po: |
21 fixes Abs :: "'a::po \<Rightarrow> 'b::sq_ord" |
23 fixes Abs :: "'a::po \<Rightarrow> 'b::type" |
22 assumes type: "type_definition Rep Abs A" |
24 assumes type: "type_definition Rep Abs A" |
23 and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
25 and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
24 shows "OFCLASS('b, po_class)" |
26 shows "OFCLASS('b, po_class)" |
25 apply (intro_classes, unfold less) |
27 apply (intro_classes, unfold less) |
26 apply (rule refl_less) |
28 apply (rule refl_less) |
27 apply (erule (1) trans_less) |
29 apply (erule (1) trans_less) |
28 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
30 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
29 apply (erule (1) antisym_less) |
31 apply (erule (1) antisym_less) |
30 done |
32 done |
|
33 |
|
34 setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, |
|
35 SOME @{typ "'a::sq_ord \<Rightarrow> 'a::sq_ord \<Rightarrow> bool"}) *} |
31 |
36 |
32 subsection {* Proving a subtype is finite *} |
37 subsection {* Proving a subtype is finite *} |
33 |
38 |
34 lemma typedef_finite_UNIV: |
39 lemma typedef_finite_UNIV: |
35 fixes Abs :: "'a::type \<Rightarrow> 'b::type" |
40 fixes Abs :: "'a::type \<Rightarrow> 'b::type" |