# HG changeset patch # User haftmann # Date 1201269236 -3600 # Node ID 07e08dad8a7733f7252970e64f10c32f85aabdca # Parent 13b6c0b310056d644b892e886242bb501849247f distinguished examples for Efficient_Nat.thy diff -r 13b6c0b31005 -r 07e08dad8a77 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jan 25 14:53:55 2008 +0100 +++ b/src/HOL/IsaMakefile Fri Jan 25 14:53:56 2008 +0100 @@ -672,7 +672,7 @@ ex/Chinese.thy ex/Classical.thy ex/Dense_Linear_Order_Ex.thy \ ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \ ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \ - ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \ + ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy ex/Hex_Bin_Examples.thy \ ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \ ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \ ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \ diff -r 13b6c0b31005 -r 07e08dad8a77 src/HOL/ex/Codegenerator_Pretty.thy --- a/src/HOL/ex/Codegenerator_Pretty.thy Fri Jan 25 14:53:55 2008 +0100 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Fri Jan 25 14:53:56 2008 +0100 @@ -6,74 +6,32 @@ header {* Simple examples for pretty numerals and such *} theory Codegenerator_Pretty -imports "~~/src/HOL/Real/RealDef" Efficient_Nat +imports ExecutableContent Code_Char Efficient_Nat begin -fun - to_n :: "nat \ nat list" -where - "to_n 0 = []" - | "to_n (Suc 0) = []" - | "to_n (Suc (Suc 0)) = []" - | "to_n (Suc n) = n # to_n n" - -definition - naive_prime :: "nat \ bool" -where - "naive_prime n \ n \ 2 \ filter (\m. n mod m = 0) (to_n n) = []" +declare term_of_index.simps [code func del] -primrec - fac :: "nat \ nat" -where - "fac 0 = 1" - | "fac (Suc n) = Suc n * fac n" +declare char.recs [code func del] + char.cases [code func del] + char.size [code func del] + term_of_char.simps [code func del] -primrec - rat_of_nat :: "nat \ rat" -where - "rat_of_nat 0 = 0" - | "rat_of_nat (Suc n) = rat_of_nat n + 1" - -primrec - harmonic :: "nat \ rat" -where - "harmonic 0 = 0" - | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n" +declare isnorm.simps [code func del] -lemma "harmonic 200 \ 5" - by eval - -lemma "harmonic 200 \ 5" - by evaluation - -lemma "harmonic 20 \ 3" - by normalization - -lemma "naive_prime 89" - by eval - -lemma "naive_prime 89" - by evaluation - -lemma "naive_prime 89" - by normalization +ML {* (*FIXME get rid of this*) +nonfix union; +nonfix inter; +nonfix upto; +*} -lemma "\ naive_prime 87" - by eval - -lemma "\ naive_prime 87" - by evaluation - -lemma "\ naive_prime 87" - by normalization +export_code * in SML module_name CodegenTest + in OCaml module_name CodegenTest file - + in Haskell file - -lemma "fac 10 > 3000000" - by eval - -lemma "fac 10 > 3000000" - by evaluation - -lemma "fac 10 > 3000000" - by normalization +ML {* +infix union; +infix inter; +infix 4 upto; +*} end diff -r 13b6c0b31005 -r 07e08dad8a77 src/HOL/ex/Efficient_Nat_examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Efficient_Nat_examples.thy Fri Jan 25 14:53:56 2008 +0100 @@ -0,0 +1,79 @@ +(* Title: HOL/ex/Efficient_Nat_examples.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Simple examples for Efficient\_Nat theory. *} + +theory Efficient_Nat_examples +imports "~~/src/HOL/Real/RealDef" Efficient_Nat +begin + +fun + to_n :: "nat \ nat list" +where + "to_n 0 = []" + | "to_n (Suc 0) = []" + | "to_n (Suc (Suc 0)) = []" + | "to_n (Suc n) = n # to_n n" + +definition + naive_prime :: "nat \ bool" +where + "naive_prime n \ n \ 2 \ filter (\m. n mod m = 0) (to_n n) = []" + +primrec + fac :: "nat \ nat" +where + "fac 0 = 1" + | "fac (Suc n) = Suc n * fac n" + +primrec + rat_of_nat :: "nat \ rat" +where + "rat_of_nat 0 = 0" + | "rat_of_nat (Suc n) = rat_of_nat n + 1" + +primrec + harmonic :: "nat \ rat" +where + "harmonic 0 = 0" + | "harmonic (Suc n) = 1 / rat_of_nat (Suc n) + harmonic n" + +lemma "harmonic 200 \ 5" + by eval + +lemma "harmonic 200 \ 5" + by evaluation + +lemma "harmonic 20 \ 3" + by normalization + +lemma "naive_prime 89" + by eval + +lemma "naive_prime 89" + by evaluation + +lemma "naive_prime 89" + by normalization + +lemma "\ naive_prime 87" + by eval + +lemma "\ naive_prime 87" + by evaluation + +lemma "\ naive_prime 87" + by normalization + +lemma "fac 10 > 3000000" + by eval + +lemma "fac 10 > 3000000" + by evaluation + +lemma "fac 10 > 3000000" + by normalization + +end diff -r 13b6c0b31005 -r 07e08dad8a77 src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Fri Jan 25 14:53:55 2008 +0100 +++ b/src/HOL/ex/ExecutableContent.thy Fri Jan 25 14:53:56 2008 +0100 @@ -8,6 +8,7 @@ imports Main Eval + Code_Index "~~/src/HOL/ex/Records" AssocList Binomial @@ -28,93 +29,7 @@ Word begin -definition - n :: nat where - "n = 42" - -definition - k :: "int" where - "k = -42" - -datatype mut1 = Tip | Top mut2 - and mut2 = Tip | Top mut1 - -primrec - mut1 :: "mut1 \ mut1" - and mut2 :: "mut2 \ mut2" -where - "mut1 mut1.Tip = mut1.Tip" - | "mut1 (mut1.Top x) = mut1.Top (mut2 x)" - | "mut2 mut2.Tip = mut2.Tip" - | "mut2 (mut2.Top x) = mut2.Top (mut1 x)" - -definition - "mystring = ''my home is my castle''" - -text {* nested lets and such *} - -definition - "abs_let x = (let (y, z) = x in (\u. case u of () \ (y + y)))" - -definition - "nested_let x = (let (y, z) = x in let w = y z in w * w)" - -definition - "case_let x = (let (y, z) = x in case y of () => z)" - -definition - "base_case f = f list_case" - -definition - "apply_tower = (\x. x (\x. x (\x. x)))" - -definition - "keywords fun datatype x instance funa classa = - Suc fun + datatype * x mod instance - funa - classa" - -hide (open) const keywords - -definition - "shadow keywords = keywords @ [ExecutableContent.keywords 0 0 0 0 0 0]" - -definition - foo :: "rat \ rat \ rat \ rat" where - "foo r s t = (t + s) / t" - -definition - bar :: "rat \ rat \ rat \ bool" where - "bar r s t \ (r - s) \ t \ (s - t) \ r" - -definition - "R1 = Fract 3 7" - -definition - "R2 = Fract (-7) 5" - -definition - "R3 = Fract 11 (-9)" - -definition - "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)" - -definition - foo' :: "real \ real \ real \ real" where - "foo' r s t = (t + s) / t" - -definition - bar' :: "real \ real \ real \ bool" where - "bar' r s t \ (r - s) \ t \ (s - t) \ r" - -definition - "R1' = real_of_rat (Fract 3 7)" - -definition - "R2' = real_of_rat (Fract (-7) 5)" - -definition - "R3' = real_of_rat (Fract 11 (-9))" - -definition - "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')" +declare term_of_index.simps [code func del] +declare fast_bv_to_nat_helper.simps [code func del] end diff -r 13b6c0b31005 -r 07e08dad8a77 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Fri Jan 25 14:53:55 2008 +0100 +++ b/src/HOL/ex/ROOT.ML Fri Jan 25 14:53:56 2008 +0100 @@ -9,12 +9,17 @@ "GCD", "Eval", "State_Monad", - "Code_Integer", - "Efficient_Nat", + "Efficient_Nat_examples", + "ExecutableContent", + "FuncSet", + "Word", + "Eval_Examples", + "Random" +]; + +no_document use_thys [ "Codegenerator", - "Codegenerator_Pretty", - "FuncSet", - "Word" + "Codegenerator_Pretty" ]; use_thys [ @@ -49,8 +54,6 @@ "Unification", "Commutative_RingEx", "Commutative_Ring_Complete", - "Eval_Examples", - "Random", "Primrec", "Tarski", "Adder",