src/HOL/Library/Numeral_Type.thy
changeset 51288 be7e9a675ec9
parent 51175 9f472d5f112c
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Feb 25 20:55:48 2013 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Feb 27 10:33:30 2013 +0100
     1.3 @@ -287,10 +287,9 @@
     1.4  declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
     1.5  declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
     1.6  
     1.7 -subsection {* Linorder instance *}
     1.8 +subsection {* Order instances *}
     1.9  
    1.10  instantiation bit0 and bit1 :: (finite) linorder begin
    1.11 -
    1.12  definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b"
    1.13  definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b"
    1.14  definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b"
    1.15 @@ -299,8 +298,23 @@
    1.16  instance
    1.17    by(intro_classes)
    1.18      (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
    1.19 +end
    1.20  
    1.21 -end
    1.22 +lemma (in preorder) tranclp_less: "op <\<^sup>+\<^sup>+ = op <"
    1.23 +by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
    1.24 +
    1.25 +instance bit0 and bit1 :: (finite) wellorder
    1.26 +proof -
    1.27 +  have "wf {(x :: 'a bit0, y). x < y}"
    1.28 +    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
    1.29 +  thus "OFCLASS('a bit0, wellorder_class)"
    1.30 +    by(rule wf_wellorderI) intro_classes
    1.31 +next
    1.32 +  have "wf {(x :: 'a bit1, y). x < y}"
    1.33 +    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
    1.34 +  thus "OFCLASS('a bit1, wellorder_class)"
    1.35 +    by(rule wf_wellorderI) intro_classes
    1.36 +qed
    1.37  
    1.38  subsection {* Code setup and type classes for code generation *}
    1.39