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 +declare term_of_index.simps [code func del]
2.19
2.20 -definition
2.21 - naive_prime :: "nat \<Rightarrow> bool"
2.22 -where
2.23 - "naive_prime n \<longleftrightarrow> n \<ge> 2 \<and> filter (\<lambda>m. n mod m = 0) (to_n n) = []"
2.24 +declare char.recs [code func del]
2.25 + char.cases [code func del]
2.26 + char.size [code func del]
2.27 + term_of_char.simps [code func del]
2.28
2.29 -primrec
2.30 - fac :: "nat \<Rightarrow> nat"
2.31 -where
2.32 - "fac 0 = 1"
2.33 - | "fac (Suc n) = Suc n * fac n"
2.34 +declare isnorm.simps [code func del]
2.35
2.36 -primrec
2.37 - rat_of_nat :: "nat \<Rightarrow> rat"
2.38 -where
2.39 - "rat_of_nat 0 = 0"
2.40 - | "rat_of_nat (Suc n) = rat_of_nat n + 1"
2.41 +ML {* (*FIXME get rid of this*)
2.42 +nonfix union;
2.43 +nonfix inter;
2.44 +nonfix upto;
2.45 +*}
2.46
2.47 -primrec
2.48 - harmonic :: "nat \<Rightarrow> rat"
2.49 -where
2.50 - "harmonic 0 = 0"
2.51 - | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n"
2.52 +export_code * in SML module_name CodegenTest
2.53 + in OCaml module_name CodegenTest file -
2.54 + in Haskell file -
2.55
2.56 -lemma "harmonic 200 \<ge> 5"
2.57 - by eval
2.58 -
2.59 -lemma "harmonic 200 \<ge> 5"
2.60 - by evaluation
2.61 -
2.62 -lemma "harmonic 20 \<ge> 3"
2.63 - by normalization
2.64 -
2.65 -lemma "naive_prime 89"
2.66 - by eval
2.67 -
2.68 -lemma "naive_prime 89"
2.69 - by evaluation
2.70 -
2.71 -lemma "naive_prime 89"
2.72 - by normalization
2.73 -
2.74 -lemma "\<not> naive_prime 87"
2.75 - by eval
2.76 -
2.77 -lemma "\<not> naive_prime 87"
2.78 - by evaluation
2.79 -
2.80 -lemma "\<not> naive_prime 87"
2.81 - by normalization
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",