proper meaningful examples
authorhaftmann
Mon Jan 21 08:43:33 2008 +0100 (2008-01-21)
changeset 259337fc0f4065251
parent 25932 db0fd0ecdcd4
child 25934 7b8f3a9efa03
proper meaningful examples
src/HOL/ex/Codegenerator_Pretty.thy
     1.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Mon Jan 21 08:43:32 2008 +0100
     1.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Mon Jan 21 08:43:33 2008 +0100
     1.3 @@ -9,52 +9,71 @@
     1.4  imports "~~/src/HOL/Real/RealDef" Efficient_Nat
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
     1.9 -  "foo r s t = (t + s) / t"
    1.10 -
    1.11 -definition
    1.12 -  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
    1.13 -  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
    1.14 -
    1.15 -definition
    1.16 -  "R1 = Fract 3 7"
    1.17 -
    1.18 -definition
    1.19 -  "R2 = Fract (-7) 5"
    1.20 -
    1.21 -definition
    1.22 -  "R3 = Fract 11 (-9)"
    1.23 -
    1.24 -definition
    1.25 -  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
    1.26 -
    1.27 -definition
    1.28 -  foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
    1.29 -  "foo' r s t = (t + s) / t"
    1.30 +fun
    1.31 +  to_n :: "nat \<Rightarrow> nat list"
    1.32 +where
    1.33 +  "to_n 0 = []"
    1.34 +  | "to_n (Suc 0) = []"
    1.35 +  | "to_n (Suc (Suc 0)) = []"
    1.36 +  | "to_n (Suc n) = n # to_n n"
    1.37  
    1.38  definition
    1.39 -  bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
    1.40 -  "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
    1.41 +  naive_prime :: "nat \<Rightarrow> bool"
    1.42 +where
    1.43 +  "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
    1.44 +
    1.45 +primrec
    1.46 +  fac :: "nat \<Rightarrow> nat"
    1.47 +where
    1.48 +  "fac 0 = 1"
    1.49 +  | "fac (Suc n) = Suc n * fac n"
    1.50  
    1.51 -definition
    1.52 -  "R1' = real_of_rat (Fract 3 7)"
    1.53 +primrec
    1.54 +  rat_of_nat :: "nat \<Rightarrow> rat"
    1.55 +where
    1.56 +  "rat_of_nat 0 = 0"
    1.57 +  | "rat_of_nat (Suc n) = rat_of_nat n + 1"
    1.58  
    1.59 -definition
    1.60 -  "R2' = real_of_rat (Fract (-7) 5)"
    1.61 +primrec
    1.62 +  harmonic :: "nat \<Rightarrow> rat"
    1.63 +where
    1.64 +  "harmonic 0 = 0"
    1.65 +  | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n"
    1.66 +
    1.67 +lemma "harmonic 200 \<ge> 5"
    1.68 +  by eval
    1.69 +
    1.70 +lemma "harmonic 200 \<ge> 5"
    1.71 +  by evaluation
    1.72  
    1.73 -definition
    1.74 -  "R3' = real_of_rat (Fract 11 (-9))"
    1.75 +lemma "harmonic 20 \<ge> 3"
    1.76 +  by normalization
    1.77 +
    1.78 +lemma "naive_prime 89"
    1.79 +  by eval
    1.80  
    1.81 -definition
    1.82 -  "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
    1.83 +lemma "naive_prime 89"
    1.84 +  by evaluation
    1.85 +
    1.86 +lemma "naive_prime 89"
    1.87 +  by normalization
    1.88 +
    1.89 +lemma "\<not> naive_prime 87"
    1.90 +  by eval
    1.91  
    1.92 -definition
    1.93 -  "(doodle :: nat) = 1705 div 42 * 42 + 1705 mod 42"
    1.94 +lemma "\<not> naive_prime 87"
    1.95 +  by evaluation
    1.96 +
    1.97 +lemma "\<not> naive_prime 87"
    1.98 +  by normalization
    1.99  
   1.100 -export_code foobar foobar' doodle in SML module_name Foo
   1.101 -  in OCaml file -
   1.102 -  in Haskell file -
   1.103 -ML {* (Foo.foobar, Foo.foobar', Foo.doodle) *}
   1.104 +lemma "fac 10 > 3000000"
   1.105 +  by eval
   1.106 +
   1.107 +lemma "fac 10 > 3000000"
   1.108 +  by evaluation
   1.109 +
   1.110 +lemma "fac 10 > 3000000"
   1.111 +  by normalization
   1.112  
   1.113  end