src/HOLCF/Pcpodef.thy
changeset 28073 5e9f00f4f209
parent 27296 eec7a1889ca5
child 29138 661a8db7e647
equal deleted inserted replaced
28072:a45e8c872dc1 28073:5e9f00f4f209
    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"