equal
deleted
inserted
replaced
22 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
22 and below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
23 shows "class.po below" |
23 shows "class.po below" |
24 apply (rule class.po.intro) |
24 apply (rule class.po.intro) |
25 apply (unfold below) |
25 apply (unfold below) |
26 apply (rule below_refl) |
26 apply (rule below_refl) |
27 apply (erule (1) below_trans) |
27 apply (fact below_trans) |
28 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
28 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
29 apply (erule (1) below_antisym) |
29 apply (fact below_antisym) |
30 done |
30 done |
31 |
31 |
32 lemmas typedef_po_class = below.typedef_class_po [THEN po.intro_of_class] |
32 lemmas typedef_po_class = below.typedef_class_po [THEN po.intro_of_class] |
33 |
33 |
34 |
34 |