src/HOL/Library/Countable.thy
changeset 61115 3a4400985780
parent 61076 bdc1e2f0a86a
child 62087 44841d07ef1d
     1.1 --- a/src/HOL/Library/Countable.thy	Fri Sep 04 16:01:58 2015 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Fri Sep 04 19:22:13 2015 +0200
     1.3 @@ -66,15 +66,17 @@
     1.4  
     1.5  subsection \<open>Automatically proving countability of old-style datatypes\<close>
     1.6  
     1.7 -inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
     1.8 +context
     1.9 +begin
    1.10 +
    1.11 +qualified inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
    1.12    undefined: "finite_item undefined"
    1.13  | In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)"
    1.14  | In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)"
    1.15  | Leaf: "finite_item (Old_Datatype.Leaf a)"
    1.16  | Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)"
    1.17  
    1.18 -function
    1.19 -  nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
    1.20 +qualified function nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
    1.21  where
    1.22    "nth_item 0 = undefined"
    1.23  | "nth_item (Suc n) =
    1.24 @@ -97,7 +99,7 @@
    1.25  lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)"
    1.26  unfolding sum_encode_def by simp
    1.27  
    1.28 -termination
    1.29 +qualified termination
    1.30  by (relation "measure id")
    1.31    (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
    1.32      le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
    1.33 @@ -193,7 +195,7 @@
    1.34        end)
    1.35  \<close>
    1.36  
    1.37 -hide_const (open) finite_item nth_item
    1.38 +end
    1.39  
    1.40  
    1.41  subsection \<open>Automatically proving countability of datatypes\<close>