merged
authornipkow
Mon Dec 15 10:19:02 2008 +0100 (2008-12-15)
changeset 29111d2b60c49a713
parent 29105 8f38bf68d42e
parent 29110 476c46e99ada
child 29112 f2b45eea6dac
child 29680 a88b62dc3821
merged
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Divides.thy	Mon Dec 15 09:58:45 2008 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Dec 15 10:19:02 2008 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4    note that ultimately show thesis by blast
     1.5  qed
     1.6  
     1.7 -lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.8 +lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
     1.9  proof
    1.10    assume "b mod a = 0"
    1.11    with mod_div_equality [of b a] have "b div a * a = b" by simp
     2.1 --- a/src/HOL/IsaMakefile	Mon Dec 15 09:58:45 2008 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Mon Dec 15 10:19:02 2008 +0100
     2.3 @@ -777,6 +777,7 @@
     2.4    ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
     2.5    ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
     2.6    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
     2.7 +  ex/CodegenSML_Test.thy 						\
     2.8    ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\
     2.9    ex/Hex_Bin_Examples.thy ex/Commutative_Ring_Complete.thy		\
    2.10    ex/ExecutableContent.thy ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy	\
     3.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Dec 15 09:58:45 2008 +0100
     3.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Dec 15 10:19:02 2008 +0100
     3.3 @@ -28,6 +28,10 @@
     3.4  lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
     3.5    unfolding eq_set_def by auto
     3.6  
     3.7 +(* FIXME allow for Stefan's code generator:
     3.8 +declare set_eq_subset[code unfold]
     3.9 +*)
    3.10 +
    3.11  lemma [code]:
    3.12    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    3.13    unfolding bex_triv_one_point1 ..
    3.14 @@ -35,6 +39,8 @@
    3.15  definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    3.16    "filter_set P xs = {x\<in>xs. P x}"
    3.17  
    3.18 +declare filter_set_def[symmetric, code unfold] 
    3.19 +
    3.20  
    3.21  subsection {* Operations on lists *}
    3.22  
    3.23 @@ -269,5 +275,6 @@
    3.24    Ball ("{*Blall*}")
    3.25    Bex ("{*Blex*}")
    3.26    filter_set ("{*filter*}")
    3.27 +  fold ("{* foldl o flip *}")
    3.28  
    3.29  end
     4.1 --- a/src/HOL/Real.thy	Mon Dec 15 09:58:45 2008 +0100
     4.2 +++ b/src/HOL/Real.thy	Mon Dec 15 10:19:02 2008 +0100
     4.3 @@ -1,5 +1,5 @@
     4.4  theory Real
     4.5 -imports "~~/src/HOL/Real/RealVector"
     4.6 +imports RComplete "~~/src/HOL/Real/RealVector"
     4.7  begin
     4.8  
     4.9  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ex/CodegenSML_Test.thy	Mon Dec 15 10:19:02 2008 +0100
     5.3 @@ -0,0 +1,54 @@
     5.4 +(*  Title:      Test file for Stefan Berghofer's SML code generator
     5.5 +    Author:     Tobias Nipkow, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +theory CodegenSML_Test
     5.9 +imports Executable_Set
    5.10 +begin
    5.11 +
    5.12 +lemma "True : {False, True} & False ~: {True}"
    5.13 +by evaluation
    5.14 +
    5.15 +lemma
    5.16 +"eq_set ({1::nat,2,3,2} \<union> {3,1,2,1}) {2,2,3,1} &
    5.17 + eq_set ({1::nat,2,3,2} \<union> {4,1,5,1}) {4,4,5,1,2,3}"
    5.18 +by evaluation
    5.19 +
    5.20 +lemma
    5.21 +"eq_set ({1::nat,2,3,2} \<inter> {3,1,2,1}) {2,2,3,1} & 
    5.22 + eq_set ({1::nat,2,3,2} \<inter> {4,1,5,2}) {2,1,2}"
    5.23 +by evaluation
    5.24 +
    5.25 +lemma
    5.26 +"eq_set ({1::nat,2,3,2} - {3,1,2,1}) {} & 
    5.27 + eq_set ({1::nat,2,3,2} - {4,1,5,2}) {3}"
    5.28 +by evaluation
    5.29 +
    5.30 +lemma
    5.31 +"eq_set (Union{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} &
    5.32 + eq_set (Union{{1::nat,2,3,2}, {4,1,5,1}}) {4,4,5,1,2,3}"
    5.33 +by evaluation
    5.34 +
    5.35 +lemma
    5.36 +"eq_set (Inter{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} & 
    5.37 + eq_set (Inter{{1::nat,2,3,2}, {4,1,5,2}}) {2,1,2}"
    5.38 +by evaluation
    5.39 +
    5.40 +lemma "eq_set ((%x. x+2) ` {1::nat,2,3,2}) {4,5,3,3}"
    5.41 +by evaluation
    5.42 +
    5.43 +lemma
    5.44 +"(ALL x:{1::nat,2,3,2}. EX y : {4,5,2}. x < y) &
    5.45 + (EX x:{1::nat,2,3,2}. ALL y : {4,5,6}. x < y)"
    5.46 +by evaluation
    5.47 +
    5.48 +lemma
    5.49 +"eq_set {x : {4::nat,7,10}. 2 dvd x } {4,10}"
    5.50 +by evaluation
    5.51 +
    5.52 +lemma
    5.53 +"fold (op +) (5::int) {3,7,9} = 24 &
    5.54 + fold_image (op *) id (2::int) {3,4,5} = 120"
    5.55 +by evaluation
    5.56 +
    5.57 +end