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))
```