src/HOL/Lazy_Sequence.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 55413 a8e96847523c
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -169,13 +169,14 @@
     1.4  where
     1.5    "those xq = Option.map lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
     1.6    
     1.7 -function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a lazy_sequence"
     1.8 +function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
     1.9  where
    1.10    "iterate_upto f n m =
    1.11      Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
    1.12    by pat_completeness auto
    1.13  
    1.14 -termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
    1.15 +termination by (relation "measure (\<lambda>(f, n, m). nat_of_natural (m + 1 - n))")
    1.16 +  (auto simp add: less_natural_def)
    1.17  
    1.18  definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
    1.19  where
    1.20 @@ -225,7 +226,7 @@
    1.21  subsubsection {* Small lazy typeclasses *}
    1.22  
    1.23  class small_lazy =
    1.24 -  fixes small_lazy :: "code_numeral \<Rightarrow> 'a lazy_sequence"
    1.25 +  fixes small_lazy :: "natural \<Rightarrow> 'a lazy_sequence"
    1.26  
    1.27  instantiation unit :: small_lazy
    1.28  begin
    1.29 @@ -252,7 +253,7 @@
    1.30    by (relation "measure (%(d, i). nat (d + 1 - i))") auto
    1.31  
    1.32  definition
    1.33 -  "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.34 +  "small_lazy d = small_lazy' (int (nat_of_natural d)) (- (int (nat_of_natural d)))"
    1.35  
    1.36  instance ..
    1.37  
    1.38 @@ -271,7 +272,7 @@
    1.39  instantiation list :: (small_lazy) small_lazy
    1.40  begin
    1.41  
    1.42 -fun small_lazy_list :: "code_numeral \<Rightarrow> 'a list lazy_sequence"
    1.43 +fun small_lazy_list :: "natural \<Rightarrow> 'a list lazy_sequence"
    1.44  where
    1.45    "small_lazy_list d = append (single [])
    1.46      (if d > 0 then bind (product (small_lazy (d - 1))