distinguished examples for Efficient_Nat.thy
authorhaftmann
Fri Jan 25 14:53:56 2008 +0100 (2008-01-25)
changeset 2596307e08dad8a77
parent 25962 13b6c0b31005
child 25964 080f89d89990
distinguished examples for Efficient_Nat.thy
src/HOL/IsaMakefile
src/HOL/ex/Codegenerator_Pretty.thy
src/HOL/ex/Efficient_Nat_examples.thy
src/HOL/ex/ExecutableContent.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 25 14:53:55 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 25 14:53:56 2008 +0100
     1.3 @@ -672,7 +672,7 @@
     1.4    ex/Chinese.thy ex/Classical.thy ex/Dense_Linear_Order_Ex.thy \
     1.5    ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \
     1.6    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
     1.7 -  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
     1.8 +  ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy ex/Hex_Bin_Examples.thy \
     1.9    ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
    1.10    ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
    1.11    ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
     2.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Fri Jan 25 14:53:55 2008 +0100
     2.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Fri Jan 25 14:53:56 2008 +0100
     2.3 @@ -6,74 +6,32 @@
     2.4  header {* Simple examples for pretty numerals and such *}
     2.5  
     2.6  theory Codegenerator_Pretty
     2.7 -imports "~~/src/HOL/Real/RealDef" Efficient_Nat
     2.8 +imports ExecutableContent Code_Char Efficient_Nat
     2.9  begin
    2.10  
    2.11 -fun
    2.12 -  to_n :: "nat \<Rightarrow> nat list"
    2.13 -where
    2.14 -  "to_n 0 = []"
    2.15 -  | "to_n (Suc 0) = []"
    2.16 -  | "to_n (Suc (Suc 0)) = []"
    2.17 -  | "to_n (Suc n) = n # to_n n"
    2.18 -
    2.19 -definition
    2.20 -  naive_prime :: "nat \<Rightarrow> bool"
    2.21 -where
    2.22 -  "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
    2.23 +declare term_of_index.simps [code func del]
    2.24  
    2.25 -primrec
    2.26 -  fac :: "nat \<Rightarrow> nat"
    2.27 -where
    2.28 -  "fac 0 = 1"
    2.29 -  | "fac (Suc n) = Suc n * fac n"
    2.30 +declare char.recs [code func del]
    2.31 +  char.cases [code func del]
    2.32 +  char.size [code func del]
    2.33 +  term_of_char.simps [code func del]
    2.34  
    2.35 -primrec
    2.36 -  rat_of_nat :: "nat \<Rightarrow> rat"
    2.37 -where
    2.38 -  "rat_of_nat 0 = 0"
    2.39 -  | "rat_of_nat (Suc n) = rat_of_nat n + 1"
    2.40 -
    2.41 -primrec
    2.42 -  harmonic :: "nat \<Rightarrow> rat"
    2.43 -where
    2.44 -  "harmonic 0 = 0"
    2.45 -  | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n"
    2.46 +declare isnorm.simps [code func del]
    2.47  
    2.48 -lemma "harmonic 200 \<ge> 5"
    2.49 -  by eval
    2.50 -
    2.51 -lemma "harmonic 200 \<ge> 5"
    2.52 -  by evaluation
    2.53 -
    2.54 -lemma "harmonic 20 \<ge> 3"
    2.55 -  by normalization
    2.56 -
    2.57 -lemma "naive_prime 89"
    2.58 -  by eval
    2.59 -
    2.60 -lemma "naive_prime 89"
    2.61 -  by evaluation
    2.62 -
    2.63 -lemma "naive_prime 89"
    2.64 -  by normalization
    2.65 +ML {* (*FIXME get rid of this*)
    2.66 +nonfix union;
    2.67 +nonfix inter;
    2.68 +nonfix upto;
    2.69 +*}
    2.70  
    2.71 -lemma "\<not> naive_prime 87"
    2.72 -  by eval
    2.73 -
    2.74 -lemma "\<not> naive_prime 87"
    2.75 -  by evaluation
    2.76 -
    2.77 -lemma "\<not> naive_prime 87"
    2.78 -  by normalization
    2.79 +export_code * in SML module_name CodegenTest
    2.80 +  in OCaml module_name CodegenTest file -
    2.81 +  in Haskell file -
    2.82  
    2.83 -lemma "fac 10 > 3000000"
    2.84 -  by eval
    2.85 -
    2.86 -lemma "fac 10 > 3000000"
    2.87 -  by evaluation
    2.88 -
    2.89 -lemma "fac 10 > 3000000"
    2.90 -  by normalization
    2.91 +ML {*
    2.92 +infix union;
    2.93 +infix inter;
    2.94 +infix 4 upto;
    2.95 +*}
    2.96  
    2.97  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Efficient_Nat_examples.thy	Fri Jan 25 14:53:56 2008 +0100
     3.3 @@ -0,0 +1,79 @@
     3.4 +(*  Title:      HOL/ex/Efficient_Nat_examples.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Florian Haftmann, TU Muenchen
     3.7 +*)
     3.8 +
     3.9 +header {* Simple examples for Efficient\_Nat theory.  *}
    3.10 +
    3.11 +theory Efficient_Nat_examples
    3.12 +imports "~~/src/HOL/Real/RealDef" Efficient_Nat
    3.13 +begin
    3.14 +
    3.15 +fun
    3.16 +  to_n :: "nat \<Rightarrow> nat list"
    3.17 +where
    3.18 +  "to_n 0 = []"
    3.19 +  | "to_n (Suc 0) = []"
    3.20 +  | "to_n (Suc (Suc 0)) = []"
    3.21 +  | "to_n (Suc n) = n # to_n n"
    3.22 +
    3.23 +definition
    3.24 +  naive_prime :: "nat \<Rightarrow> bool"
    3.25 +where
    3.26 +  "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
    3.27 +
    3.28 +primrec
    3.29 +  fac :: "nat \<Rightarrow> nat"
    3.30 +where
    3.31 +  "fac 0 = 1"
    3.32 +  | "fac (Suc n) = Suc n * fac n"
    3.33 +
    3.34 +primrec
    3.35 +  rat_of_nat :: "nat \<Rightarrow> rat"
    3.36 +where
    3.37 +  "rat_of_nat 0 = 0"
    3.38 +  | "rat_of_nat (Suc n) = rat_of_nat n + 1"
    3.39 +
    3.40 +primrec
    3.41 +  harmonic :: "nat \<Rightarrow> rat"
    3.42 +where
    3.43 +  "harmonic 0 = 0"
    3.44 +  | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n"
    3.45 +
    3.46 +lemma "harmonic 200 \<ge> 5"
    3.47 +  by eval
    3.48 +
    3.49 +lemma "harmonic 200 \<ge> 5"
    3.50 +  by evaluation
    3.51 +
    3.52 +lemma "harmonic 20 \<ge> 3"
    3.53 +  by normalization
    3.54 +
    3.55 +lemma "naive_prime 89"
    3.56 +  by eval
    3.57 +
    3.58 +lemma "naive_prime 89"
    3.59 +  by evaluation
    3.60 +
    3.61 +lemma "naive_prime 89"
    3.62 +  by normalization
    3.63 +
    3.64 +lemma "\<not> naive_prime 87"
    3.65 +  by eval
    3.66 +
    3.67 +lemma "\<not> naive_prime 87"
    3.68 +  by evaluation
    3.69 +
    3.70 +lemma "\<not> naive_prime 87"
    3.71 +  by normalization
    3.72 +
    3.73 +lemma "fac 10 > 3000000"
    3.74 +  by eval
    3.75 +
    3.76 +lemma "fac 10 > 3000000"
    3.77 +  by evaluation
    3.78 +
    3.79 +lemma "fac 10 > 3000000"
    3.80 +  by normalization
    3.81 +
    3.82 +end
     4.1 --- a/src/HOL/ex/ExecutableContent.thy	Fri Jan 25 14:53:55 2008 +0100
     4.2 +++ b/src/HOL/ex/ExecutableContent.thy	Fri Jan 25 14:53:56 2008 +0100
     4.3 @@ -8,6 +8,7 @@
     4.4  imports
     4.5    Main
     4.6    Eval
     4.7 +  Code_Index
     4.8    "~~/src/HOL/ex/Records"
     4.9    AssocList
    4.10    Binomial
    4.11 @@ -28,93 +29,7 @@
    4.12    Word
    4.13  begin
    4.14  
    4.15 -definition
    4.16 -  n :: nat where
    4.17 -  "n = 42"
    4.18 -
    4.19 -definition
    4.20 -  k :: "int" where
    4.21 -  "k = -42"
    4.22 -
    4.23 -datatype mut1 = Tip | Top mut2
    4.24 -  and mut2 = Tip | Top mut1
    4.25 -
    4.26 -primrec
    4.27 -  mut1 :: "mut1 \<Rightarrow> mut1"
    4.28 -  and mut2 :: "mut2 \<Rightarrow> mut2"
    4.29 -where
    4.30 -  "mut1 mut1.Tip = mut1.Tip"
    4.31 -  | "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    4.32 -  | "mut2 mut2.Tip = mut2.Tip"
    4.33 -  | "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    4.34 -
    4.35 -definition
    4.36 -  "mystring = ''my home is my castle''"
    4.37 -
    4.38 -text {* nested lets and such *}
    4.39 -
    4.40 -definition
    4.41 -  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
    4.42 -
    4.43 -definition
    4.44 -  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
    4.45 -
    4.46 -definition
    4.47 -  "case_let x = (let (y, z) = x in case y of () => z)"
    4.48 -
    4.49 -definition
    4.50 -  "base_case f = f list_case"
    4.51 -
    4.52 -definition
    4.53 -  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
    4.54 -
    4.55 -definition
    4.56 -  "keywords fun datatype x instance funa classa =
    4.57 -    Suc fun + datatype * x mod instance - funa - classa"
    4.58 -
    4.59 -hide (open) const keywords
    4.60 -
    4.61 -definition
    4.62 -  "shadow keywords = keywords @ [ExecutableContent.keywords 0 0 0 0 0 0]"
    4.63 -
    4.64 -definition
    4.65 -  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
    4.66 -  "foo r s t = (t + s) / t"
    4.67 -
    4.68 -definition
    4.69 -  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
    4.70 -  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
    4.71 -
    4.72 -definition
    4.73 -  "R1 = Fract 3 7"
    4.74 -
    4.75 -definition
    4.76 -  "R2 = Fract (-7) 5"
    4.77 -
    4.78 -definition
    4.79 -  "R3 = Fract 11 (-9)"
    4.80 -
    4.81 -definition
    4.82 -  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
    4.83 -
    4.84 -definition
    4.85 -  foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
    4.86 -  "foo' r s t = (t + s) / t"
    4.87 -
    4.88 -definition
    4.89 -  bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
    4.90 -  "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
    4.91 -
    4.92 -definition
    4.93 -  "R1' = real_of_rat (Fract 3 7)"
    4.94 -
    4.95 -definition
    4.96 -  "R2' = real_of_rat (Fract (-7) 5)"
    4.97 -
    4.98 -definition
    4.99 -  "R3' = real_of_rat (Fract 11 (-9))"
   4.100 -
   4.101 -definition
   4.102 -  "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
   4.103 +declare term_of_index.simps [code func del]
   4.104 +declare fast_bv_to_nat_helper.simps [code func del]
   4.105  
   4.106  end
     5.1 --- a/src/HOL/ex/ROOT.ML	Fri Jan 25 14:53:55 2008 +0100
     5.2 +++ b/src/HOL/ex/ROOT.ML	Fri Jan 25 14:53:56 2008 +0100
     5.3 @@ -9,12 +9,17 @@
     5.4    "GCD",
     5.5    "Eval",
     5.6    "State_Monad",
     5.7 -  "Code_Integer",
     5.8 -  "Efficient_Nat",
     5.9 +  "Efficient_Nat_examples",
    5.10 +  "ExecutableContent",
    5.11 +  "FuncSet",
    5.12 +  "Word",
    5.13 +  "Eval_Examples",
    5.14 +  "Random"
    5.15 +];
    5.16 +
    5.17 +no_document use_thys [
    5.18    "Codegenerator",
    5.19 -  "Codegenerator_Pretty",
    5.20 -  "FuncSet",
    5.21 -  "Word"
    5.22 +  "Codegenerator_Pretty"
    5.23  ];
    5.24  
    5.25  use_thys [
    5.26 @@ -49,8 +54,6 @@
    5.27    "Unification",
    5.28    "Commutative_RingEx",
    5.29    "Commutative_Ring_Complete",
    5.30 -  "Eval_Examples",
    5.31 -  "Random",
    5.32    "Primrec",
    5.33    "Tarski",
    5.34    "Adder",