src/HOL/Corec_Examples/Paper_Examples.thy
changeset 67051 e7e54a0b9197
parent 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Corec_Examples/Paper_Examples.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -96,9 +96,9 @@
     1.4  where "primes m n =
     1.5    (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
     1.6  apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
     1.7 -apply (auto simp: mod_Suc intro: Suc_lessI )
     1.8 -apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
     1.9 -by (metis diff_less_mono2 lessI mod_less_divisor)
    1.10 +   apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
    1.11 +   apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
    1.12 +  done
    1.13  
    1.14  corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
    1.15  where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"