1.1 --- a/src/HOL/Complex/NSCA.thy Tue Jul 01 21:30:12 2008 +0200
1.2 +++ b/src/HOL/Complex/NSCA.thy Wed Jul 02 07:11:57 2008 +0200
1.3 @@ -14,10 +14,9 @@
1.4 SComplex :: "hcomplex set" where
1.5 "SComplex \<equiv> Standard"
1.6
1.7 -definition
1.8 - stc :: "hcomplex => hcomplex" where
1.9 - --{* standard part map*}
1.10 - "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
1.11 +definition --{* standard part map*}
1.12 + stc :: "hcomplex => hcomplex" where
1.13 + [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
1.14
1.15
1.16 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
2.1 --- a/src/HOL/Complex/NSComplex.thy Tue Jul 01 21:30:12 2008 +0200
2.2 +++ b/src/HOL/Complex/NSComplex.thy Wed Jul 02 07:11:57 2008 +0200
2.3 @@ -26,11 +26,11 @@
2.4
2.5 definition
2.6 hRe :: "hcomplex => hypreal" where
2.7 - "hRe = *f* Re"
2.8 + [code func del]: "hRe = *f* Re"
2.9
2.10 definition
2.11 hIm :: "hcomplex => hypreal" where
2.12 - "hIm = *f* Im"
2.13 + [code func del]: "hIm = *f* Im"
2.14
2.15
2.16 (*------ imaginary unit ----------*)
2.17 @@ -43,22 +43,22 @@
2.18
2.19 definition
2.20 hcnj :: "hcomplex => hcomplex" where
2.21 - "hcnj = *f* cnj"
2.22 + [code func del]: "hcnj = *f* cnj"
2.23
2.24 (*------------ Argand -------------*)
2.25
2.26 definition
2.27 hsgn :: "hcomplex => hcomplex" where
2.28 - "hsgn = *f* sgn"
2.29 + [code func del]: "hsgn = *f* sgn"
2.30
2.31 definition
2.32 harg :: "hcomplex => hypreal" where
2.33 - "harg = *f* arg"
2.34 + [code func del]: "harg = *f* arg"
2.35
2.36 definition
2.37 (* abbreviation for (cos a + i sin a) *)
2.38 hcis :: "hypreal => hcomplex" where
2.39 - "hcis = *f* cis"
2.40 + [code func del]:"hcis = *f* cis"
2.41
2.42 (*----- injection from hyperreals -----*)
2.43
2.44 @@ -69,16 +69,16 @@
2.45 definition
2.46 (* abbreviation for r*(cos a + i sin a) *)
2.47 hrcis :: "[hypreal, hypreal] => hcomplex" where
2.48 - "hrcis = *f2* rcis"
2.49 + [code func del]: "hrcis = *f2* rcis"
2.50
2.51 (*------------ e ^ (x + iy) ------------*)
2.52 definition
2.53 hexpi :: "hcomplex => hcomplex" where
2.54 - "hexpi = *f* expi"
2.55 + [code func del]: "hexpi = *f* expi"
2.56
2.57 definition
2.58 HComplex :: "[hypreal,hypreal] => hcomplex" where
2.59 - "HComplex = *f2* Complex"
2.60 + [code func del]: "HComplex = *f2* Complex"
2.61
2.62 lemmas hcomplex_defs [transfer_unfold] =
2.63 hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
3.1 --- a/src/HOL/Hyperreal/HDeriv.thy Tue Jul 01 21:30:12 2008 +0200
3.2 +++ b/src/HOL/Hyperreal/HDeriv.thy Wed Jul 02 07:11:57 2008 +0200
3.3 @@ -27,7 +27,7 @@
3.4
3.5 definition
3.6 increment :: "[real=>real,real,hypreal] => hypreal" where
3.7 - "increment f x h = (@inc. f NSdifferentiable x &
3.8 + [code func del]: "increment f x h = (@inc. f NSdifferentiable x &
3.9 inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
3.10
3.11
4.1 --- a/src/HOL/Hyperreal/HLim.thy Tue Jul 01 21:30:12 2008 +0200
4.2 +++ b/src/HOL/Hyperreal/HLim.thy Wed Jul 02 07:11:57 2008 +0200
4.3 @@ -16,18 +16,18 @@
4.4 definition
4.5 NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
4.6 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
4.7 - "f -- a --NS> L =
4.8 + [code func del]: "f -- a --NS> L =
4.9 (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
4.10
4.11 definition
4.12 isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
4.13 --{*NS definition dispenses with limit notions*}
4.14 - "isNSCont f a = (\<forall>y. y @= star_of a -->
4.15 + [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
4.16 ( *f* f) y @= star_of (f a))"
4.17
4.18 definition
4.19 isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
4.20 - "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
4.21 + [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
4.22
4.23
4.24 subsection {* Limits of Functions *}
5.1 --- a/src/HOL/Hyperreal/HLog.thy Tue Jul 01 21:30:12 2008 +0200
5.2 +++ b/src/HOL/Hyperreal/HLog.thy Wed Jul 02 07:11:57 2008 +0200
5.3 @@ -20,14 +20,11 @@
5.4
5.5 definition
5.6 powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
5.7 - "x powhr a = starfun2 (op powr) x a"
5.8 + [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
5.9
5.10 definition
5.11 hlog :: "[hypreal,hypreal] => hypreal" where
5.12 - "hlog a x = starfun2 log a x"
5.13 -
5.14 -declare powhr_def [transfer_unfold]
5.15 -declare hlog_def [transfer_unfold]
5.16 + [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
5.17
5.18 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
5.19 by (simp add: powhr_def starfun2_star_n)
6.1 --- a/src/HOL/Hyperreal/HSEQ.thy Tue Jul 01 21:30:12 2008 +0200
6.2 +++ b/src/HOL/Hyperreal/HSEQ.thy Wed Jul 02 07:11:57 2008 +0200
6.3 @@ -16,7 +16,7 @@
6.4 NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
6.5 ("((_)/ ----NS> (_))" [60, 60] 60) where
6.6 --{*Nonstandard definition of convergence of sequence*}
6.7 - "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
6.8 + [code func del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
6.9
6.10 definition
6.11 nslim :: "(nat => 'a::real_normed_vector) => 'a" where
6.12 @@ -31,12 +31,12 @@
6.13 definition
6.14 NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
6.15 --{*Nonstandard definition for bounded sequence*}
6.16 - "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
6.17 + [code func del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
6.18
6.19 definition
6.20 NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
6.21 --{*Nonstandard definition*}
6.22 - "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
6.23 + [code func del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
6.24
6.25 subsection {* Limits of Sequences *}
6.26
7.1 --- a/src/HOL/Hyperreal/HSeries.thy Tue Jul 01 21:30:12 2008 +0200
7.2 +++ b/src/HOL/Hyperreal/HSeries.thy Wed Jul 02 07:11:57 2008 +0200
7.3 @@ -13,7 +13,7 @@
7.4
7.5 definition
7.6 sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
7.7 - "sumhr =
7.8 + [code func del]: "sumhr =
7.9 (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
7.10
7.11 definition
7.12 @@ -22,7 +22,7 @@
7.13
7.14 definition
7.15 NSsummable :: "(nat=>real) => bool" where
7.16 - "NSsummable f = (\<exists>s. f NSsums s)"
7.17 + [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
7.18
7.19 definition
7.20 NSsuminf :: "(nat=>real) => real" where
8.1 --- a/src/HOL/Hyperreal/HyperDef.thy Tue Jul 01 21:30:12 2008 +0200
8.2 +++ b/src/HOL/Hyperreal/HyperDef.thy Wed Jul 02 07:11:57 2008 +0200
8.3 @@ -47,7 +47,7 @@
8.4 begin
8.5
8.6 definition
8.7 - star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
8.8 + star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)"
8.9
8.10 instance ..
8.11
8.12 @@ -111,9 +111,7 @@
8.13
8.14 definition
8.15 of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
8.16 - "of_hypreal = *f* of_real"
8.17 -
8.18 -declare of_hypreal_def [transfer_unfold]
8.19 + [transfer_unfold, code func del]: "of_hypreal = *f* of_real"
8.20
8.21 lemma Standard_of_hypreal [simp]:
8.22 "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
8.23 @@ -427,11 +425,9 @@
8.24
8.25 subsection{*Powers with Hypernatural Exponents*}
8.26
8.27 -definition
8.28 +definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
8.29 + hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N"
8.30 (* hypernatural powers of hyperreals *)
8.31 - pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
8.32 - hyperpow_def [transfer_unfold]:
8.33 - "R pow N = ( *f2* op ^) R N"
8.34
8.35 lemma Standard_hyperpow [simp]:
8.36 "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"
9.1 --- a/src/HOL/Hyperreal/HyperNat.thy Tue Jul 01 21:30:12 2008 +0200
9.2 +++ b/src/HOL/Hyperreal/HyperNat.thy Wed Jul 02 07:11:57 2008 +0200
9.3 @@ -19,7 +19,7 @@
9.4
9.5 definition
9.6 hSuc :: "hypnat => hypnat" where
9.7 - hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
9.8 + hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
9.9
9.10 subsection{*Properties Transferred from Naturals*}
9.11
9.12 @@ -367,7 +367,7 @@
9.13
9.14 definition
9.15 of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
9.16 - of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
9.17 + of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
9.18
9.19 lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
9.20 by transfer (rule of_nat_0)
10.1 --- a/src/HOL/Hyperreal/Integration.thy Tue Jul 01 21:30:12 2008 +0200
10.2 +++ b/src/HOL/Hyperreal/Integration.thy Wed Jul 02 07:11:57 2008 +0200
10.3 @@ -16,29 +16,29 @@
10.4 --{*Partitions and tagged partitions etc.*}
10.5
10.6 partition :: "[(real*real),nat => real] => bool" where
10.7 - "partition = (%(a,b) D. D 0 = a &
10.8 + [code func del]: "partition = (%(a,b) D. D 0 = a &
10.9 (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
10.10 (\<forall>n \<ge> N. D(n) = b)))"
10.11
10.12 definition
10.13 psize :: "(nat => real) => nat" where
10.14 - "psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
10.15 + [code func del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
10.16 (\<forall>n \<ge> N. D(n) = D(N)))"
10.17
10.18 definition
10.19 tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
10.20 - "tpart = (%(a,b) (D,p). partition(a,b) D &
10.21 + [code func del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
10.22 (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
10.23
10.24 --{*Gauges and gauge-fine divisions*}
10.25
10.26 definition
10.27 gauge :: "[real => bool, real => real] => bool" where
10.28 - "gauge E g = (\<forall>x. E x --> 0 < g(x))"
10.29 + [code func del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
10.30
10.31 definition
10.32 fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
10.33 - "fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
10.34 + [code func del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
10.35
10.36 --{*Riemann sum*}
10.37
10.38 @@ -50,7 +50,7 @@
10.39
10.40 definition
10.41 Integral :: "[(real*real),real=>real,real] => bool" where
10.42 - "Integral = (%(a,b) f k. \<forall>e > 0.
10.43 + [code func del]: "Integral = (%(a,b) f k. \<forall>e > 0.
10.44 (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
10.45 (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
10.46 \<bar>rsum(D,p) f - k\<bar> < e)))"
11.1 --- a/src/HOL/Hyperreal/Lim.thy Tue Jul 01 21:30:12 2008 +0200
11.2 +++ b/src/HOL/Hyperreal/Lim.thy Wed Jul 02 07:11:57 2008 +0200
11.3 @@ -16,7 +16,7 @@
11.4 definition
11.5 LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
11.6 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
11.7 - "f -- a --> L =
11.8 + [code func del]: "f -- a --> L =
11.9 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
11.10 --> norm (f x - L) < r)"
11.11
11.12 @@ -26,7 +26,7 @@
11.13
11.14 definition
11.15 isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
11.16 - "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
11.17 + [code func del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
11.18
11.19
11.20 subsection {* Limits of Functions *}
12.1 --- a/src/HOL/Hyperreal/NSA.thy Tue Jul 01 21:30:12 2008 +0200
12.2 +++ b/src/HOL/Hyperreal/NSA.thy Wed Jul 02 07:11:57 2008 +0200
12.3 @@ -13,19 +13,19 @@
12.4
12.5 definition
12.6 hnorm :: "'a::norm star \<Rightarrow> real star" where
12.7 - "hnorm = *f* norm"
12.8 + [transfer_unfold]: "hnorm = *f* norm"
12.9
12.10 definition
12.11 Infinitesimal :: "('a::real_normed_vector) star set" where
12.12 - "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
12.13 + [code func del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
12.14
12.15 definition
12.16 HFinite :: "('a::real_normed_vector) star set" where
12.17 - "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
12.18 + [code func del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
12.19
12.20 definition
12.21 HInfinite :: "('a::real_normed_vector) star set" where
12.22 - "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
12.23 + [code func del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
12.24
12.25 definition
12.26 approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
12.27 @@ -58,10 +58,7 @@
12.28
12.29 definition
12.30 scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
12.31 - "scaleHR = starfun2 scaleR"
12.32 -
12.33 -declare hnorm_def [transfer_unfold]
12.34 -declare scaleHR_def [transfer_unfold]
12.35 + [transfer_unfold, code func del]: "scaleHR = starfun2 scaleR"
12.36
12.37 lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
12.38 by (simp add: hnorm_def)
13.1 --- a/src/HOL/Hyperreal/SEQ.thy Tue Jul 01 21:30:12 2008 +0200
13.2 +++ b/src/HOL/Hyperreal/SEQ.thy Wed Jul 02 07:11:57 2008 +0200
13.3 @@ -15,13 +15,13 @@
13.4 definition
13.5 Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
13.6 --{*Standard definition of sequence converging to zero*}
13.7 - "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
13.8 + [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
13.9
13.10 definition
13.11 LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
13.12 ("((_)/ ----> (_))" [60, 60] 60) where
13.13 --{*Standard definition of convergence of sequence*}
13.14 - "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
13.15 + [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
13.16
13.17 definition
13.18 lim :: "(nat => 'a::real_normed_vector) => 'a" where
13.19 @@ -36,22 +36,22 @@
13.20 definition
13.21 Bseq :: "(nat => 'a::real_normed_vector) => bool" where
13.22 --{*Standard definition for bounded sequence*}
13.23 - "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
13.24 + [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
13.25
13.26 definition
13.27 monoseq :: "(nat=>real)=>bool" where
13.28 --{*Definition for monotonicity*}
13.29 - "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
13.30 + [code func del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
13.31
13.32 definition
13.33 subseq :: "(nat => nat) => bool" where
13.34 --{*Definition of subsequence*}
13.35 - "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
13.36 + [code func del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
13.37
13.38 definition
13.39 Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
13.40 --{*Standard definition of the Cauchy condition*}
13.41 - "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
13.42 + [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
13.43
13.44
13.45 subsection {* Bounded Sequences *}
14.1 --- a/src/HOL/Hyperreal/Star.thy Tue Jul 01 21:30:12 2008 +0200
14.2 +++ b/src/HOL/Hyperreal/Star.thy Wed Jul 02 07:11:57 2008 +0200
14.3 @@ -17,12 +17,12 @@
14.4
14.5 definition
14.6 InternalSets :: "'a star set set" where
14.7 - "InternalSets = {X. \<exists>As. X = *sn* As}"
14.8 + [code func del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
14.9
14.10 definition
14.11 (* nonstandard extension of function *)
14.12 is_starext :: "['a star => 'a star, 'a => 'a] => bool" where
14.13 - "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
14.14 + [code func del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
14.15 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
14.16
14.17 definition
14.18 @@ -32,7 +32,7 @@
14.19
14.20 definition
14.21 InternalFuns :: "('a star => 'b star) set" where
14.22 - "InternalFuns = {X. \<exists>F. X = *fn* F}"
14.23 + [code func del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
14.24
14.25
14.26 (*--------------------------------------------------------
15.1 --- a/src/HOL/Hyperreal/StarDef.thy Tue Jul 01 21:30:12 2008 +0200
15.2 +++ b/src/HOL/Hyperreal/StarDef.thy Wed Jul 02 07:11:57 2008 +0200
15.3 @@ -290,9 +290,8 @@
15.4
15.5 subsection {* Internal predicates *}
15.6
15.7 -definition
15.8 - unstar :: "bool star \<Rightarrow> bool" where
15.9 - "unstar b = (b = star_of True)"
15.10 +definition unstar :: "bool star \<Rightarrow> bool" where
15.11 + [code func del]: "unstar b \<longleftrightarrow> b = star_of True"
15.12
15.13 lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
15.14 by (simp add: unstar_def star_of_def star_n_eq_iff)
15.15 @@ -433,7 +432,7 @@
15.16 begin
15.17
15.18 definition
15.19 - star_zero_def: "0 \<equiv> star_of 0"
15.20 + star_zero_def [code func del]: "0 \<equiv> star_of 0"
15.21
15.22 instance ..
15.23
15.24 @@ -443,7 +442,7 @@
15.25 begin
15.26
15.27 definition
15.28 - star_one_def: "1 \<equiv> star_of 1"
15.29 + star_one_def [code func del]: "1 \<equiv> star_of 1"
15.30
15.31 instance ..
15.32
15.33 @@ -453,7 +452,7 @@
15.34 begin
15.35
15.36 definition
15.37 - star_add_def: "(op +) \<equiv> *f2* (op +)"
15.38 + star_add_def [code func del]: "(op +) \<equiv> *f2* (op +)"
15.39
15.40 instance ..
15.41
15.42 @@ -463,7 +462,7 @@
15.43 begin
15.44
15.45 definition
15.46 - star_mult_def: "(op *) \<equiv> *f2* (op *)"
15.47 + star_mult_def [code func del]: "(op *) \<equiv> *f2* (op *)"
15.48
15.49 instance ..
15.50
15.51 @@ -473,7 +472,7 @@
15.52 begin
15.53
15.54 definition
15.55 - star_minus_def: "uminus \<equiv> *f* uminus"
15.56 + star_minus_def [code func del]: "uminus \<equiv> *f* uminus"
15.57
15.58 instance ..
15.59
15.60 @@ -483,7 +482,7 @@
15.61 begin
15.62
15.63 definition
15.64 - star_diff_def: "(op -) \<equiv> *f2* (op -)"
15.65 + star_diff_def [code func del]: "(op -) \<equiv> *f2* (op -)"
15.66
15.67 instance ..
15.68
16.1 --- a/src/HOL/Lambda/WeakNorm.thy Tue Jul 01 21:30:12 2008 +0200
16.2 +++ b/src/HOL/Lambda/WeakNorm.thy Wed Jul 02 07:11:57 2008 +0200
16.3 @@ -418,33 +418,27 @@
16.4 CodeTarget.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
16.5 *}
16.6
16.7 -definition
16.8 - int_of_nat :: "nat \<Rightarrow> int" where
16.9 +definition int_of_nat :: "nat \<Rightarrow> int" where
16.10 "int_of_nat = of_nat"
16.11
16.12 -export_code type_NF nat int_of_nat in SML module_name Norm
16.13 -
16.14 ML {*
16.15 -val nat_of_int = Norm.nat;
16.16 -val int_of_nat = Norm.int_of_nat;
16.17 -
16.18 fun dBtype_of_typ (Type ("fun", [T, U])) =
16.19 - Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
16.20 + @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
16.21 | dBtype_of_typ (TFree (s, _)) = (case explode s of
16.22 - ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
16.23 + ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
16.24 | _ => error "dBtype_of_typ: variable name")
16.25 | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
16.26
16.27 -fun dB_of_term (Bound i) = Norm.Var (nat_of_int i)
16.28 - | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u)
16.29 - | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)
16.30 +fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i)
16.31 + | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
16.32 + | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
16.33 | dB_of_term _ = error "dB_of_term: bad term";
16.34
16.35 -fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =
16.36 +fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
16.37 Abs ("x", T, term_of_dB (T :: Ts) U dBt)
16.38 | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
16.39 -and term_of_dB' Ts (Norm.Var n) = Bound (int_of_nat n)
16.40 - | term_of_dB' Ts (Norm.App (dBt, dBu)) =
16.41 +and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n)
16.42 + | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
16.43 let val t = term_of_dB' Ts dBt
16.44 in case fastype_of1 (Ts, t) of
16.45 Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
16.46 @@ -453,30 +447,28 @@
16.47 | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
16.48
16.49 fun typing_of_term Ts e (Bound i) =
16.50 - Norm.Vara (e, nat_of_int i, dBtype_of_typ (nth Ts i))
16.51 + @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i))
16.52 | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
16.53 - Type ("fun", [T, U]) => Norm.Appb (e, dB_of_term t,
16.54 + Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
16.55 dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
16.56 typing_of_term Ts e t, typing_of_term Ts e u)
16.57 | _ => error "typing_of_term: function type expected")
16.58 | typing_of_term Ts e (Abs (s, T, t)) =
16.59 let val dBT = dBtype_of_typ T
16.60 - in Norm.Absb (e, dBT, dB_of_term t,
16.61 + in @{code Abs} (e, dBT, dB_of_term t,
16.62 dBtype_of_typ (fastype_of1 (T :: Ts, t)),
16.63 - typing_of_term (T :: Ts) (Norm.shift e Norm.Zero_nat dBT) t)
16.64 + typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
16.65 end
16.66 | typing_of_term _ _ _ = error "typing_of_term: bad term";
16.67
16.68 fun dummyf _ = error "dummy";
16.69 -*}
16.70
16.71 -ML {*
16.72 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
16.73 -val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
16.74 +val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
16.75 val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
16.76
16.77 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
16.78 -val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
16.79 +val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
16.80 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
16.81 *}
16.82
17.1 --- a/src/HOL/Library/Univ_Poly.thy Tue Jul 01 21:30:12 2008 +0200
17.2 +++ b/src/HOL/Library/Univ_Poly.thy Wed Jul 02 07:11:57 2008 +0200
17.3 @@ -72,7 +72,7 @@
17.4
17.5 definition (in semiring_0)
17.6 divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where
17.7 - "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
17.8 + [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
17.9
17.10 --{*order of a polynomial*}
17.11 definition (in ring_1) order :: "'a => 'a list => nat" where
18.1 --- a/src/HOL/Real/ContNotDenum.thy Tue Jul 01 21:30:12 2008 +0200
18.2 +++ b/src/HOL/Real/ContNotDenum.thy Wed Jul 02 07:11:57 2008 +0200
18.3 @@ -393,16 +393,17 @@
18.4
18.5 subsubsection {* Definition *}
18.6
18.7 -consts newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
18.8 -primrec
18.9 -"newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
18.10 -"newInt (Suc n) f =
18.11 - (SOME e. (\<exists>e1 e2.
18.12 - e1 < e2 \<and>
18.13 - e = closed_int e1 e2 \<and>
18.14 - e \<subseteq> (newInt n f) \<and>
18.15 - (f (Suc n)) \<notin> e)
18.16 - )"
18.17 +primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
18.18 + "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
18.19 + | "newInt (Suc n) f =
18.20 + (SOME e. (\<exists>e1 e2.
18.21 + e1 < e2 \<and>
18.22 + e = closed_int e1 e2 \<and>
18.23 + e \<subseteq> (newInt n f) \<and>
18.24 + (f (Suc n)) \<notin> e)
18.25 + )"
18.26 +
18.27 +declare newInt.simps [code func del]
18.28
18.29 subsubsection {* Properties *}
18.30
19.1 --- a/src/HOL/Real/RComplete.thy Tue Jul 01 21:30:12 2008 +0200
19.2 +++ b/src/HOL/Real/RComplete.thy Wed Jul 02 07:11:57 2008 +0200
19.3 @@ -434,7 +434,7 @@
19.4
19.5 definition
19.6 floor :: "real => int" where
19.7 - "floor r = (LEAST n::int. r < real (n+1))"
19.8 + [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
19.9
19.10 definition
19.11 ceiling :: "real => int" where
20.1 --- a/src/HOL/Real/RealVector.thy Tue Jul 01 21:30:12 2008 +0200
20.2 +++ b/src/HOL/Real/RealVector.thy Wed Jul 02 07:11:57 2008 +0200
20.3 @@ -264,7 +264,7 @@
20.4
20.5 definition
20.6 Reals :: "'a::real_algebra_1 set" where
20.7 - "Reals \<equiv> range of_real"
20.8 + [code func del]: "Reals \<equiv> range of_real"
20.9
20.10 notation (xsymbols)
20.11 Reals ("\<real>")
21.1 --- a/src/HOL/ex/ExecutableContent.thy Tue Jul 01 21:30:12 2008 +0200
21.2 +++ b/src/HOL/ex/ExecutableContent.thy Wed Jul 02 07:11:57 2008 +0200
21.3 @@ -33,63 +33,25 @@
21.4
21.5 (*FIXME distribute to theories*)
21.6 declare divides_def [code func del] -- "Univ_Poly"
21.7 -declare unstar_def [code func del] -- "StarDef"
21.8 -declare star_one_def [code func del] -- "StarDef"
21.9 -declare star_mult_def [code func del] -- "StarDef"
21.10 -declare star_add_def [code func del] -- "StarDef"
21.11 -declare star_zero_def [code func del] -- "StarDef"
21.12 declare star_minus_def [code func del] -- "StarDef"
21.13 -declare star_diff_def [code func del] -- "StarDef"
21.14 -declare Reals_def [code func del] -- "RealVector"
21.15 -declare star_scaleR_def [code func del] -- "HyperDef"
21.16 -declare hyperpow_def [code func del] -- HyperDef
21.17 -declare Infinitesimal_def [code func del] -- NSA
21.18 -declare HFinite_def [code func del] -- NSA
21.19 -declare floor_def [code func del] -- RComplete
21.20 -declare LIMSEQ_def [code func del] -- SEQ
21.21 -declare partition_def [code func del] -- Integration
21.22 -declare Integral_def [code func del] -- Integration
21.23 -declare tpart_def [code func del] -- Integration
21.24 -declare psize_def [code func del] -- Integration
21.25 -declare gauge_def [code func del] -- Integration
21.26 -declare fine_def [code func del] -- Integration
21.27 -declare sumhr_def [code func del] -- HSeries
21.28 -declare NSsummable_def [code func del] -- HSeries
21.29 -declare NSLIMSEQ_def [code func del] -- HSEQ
21.30 -declare newInt.simps [code func del] -- ContNotDenum
21.31 -declare LIM_def [code func del] -- Lim
21.32 -declare NSLIM_def [code func del] -- HLim
21.33 -declare HComplex_def [code func del]
21.34 -declare of_hypnat_def [code func del]
21.35 -declare InternalSets_def [code func del]
21.36 -declare InternalFuns_def [code func del]
21.37 -declare increment_def [code func del]
21.38 -declare is_starext_def [code func del]
21.39 -declare hrcis_def [code func del]
21.40 -declare hexpi_def [code func del]
21.41 -declare hsgn_def [code func del]
21.42 -declare hcnj_def [code func del]
21.43 -declare hcis_def [code func del]
21.44 -declare harg_def [code func del]
21.45 -declare isNSUCont_def [code func del]
21.46 -declare hRe_def [code func del]
21.47 -declare hIm_def [code func del]
21.48 -declare HInfinite_def [code func del]
21.49 -declare hSuc_def [code func del]
21.50 -declare NSCauchy_def [code func del]
21.51 -declare of_hypreal_def [code func del]
21.52 -declare isNSCont_def [code func del]
21.53 +declare Zseq_def [code func del]
21.54 +declare Bseq_def [code func del]
21.55 declare monoseq_def [code func del]
21.56 -declare scaleHR_def [code func del]
21.57 -declare isUCont_def [code func del]
21.58 -declare NSBseq_def [code func del]
21.59 +declare Cauchy_def [code func del]
21.60 declare subseq_def [code func del]
21.61 -declare Cauchy_def [code func del]
21.62 declare powhr_def [code func del]
21.63 declare hlog_def [code func del]
21.64 -declare Zseq_def [code func del]
21.65 -declare Bseq_def [code func del]
21.66 +declare scaleHR_def [code func del]
21.67 declare stc_def [code func del]
21.68 +declare increment_def [code func del]
21.69 +declare of_hypreal_def [code func del]
21.70 +declare HInfinite_def [code func del]
21.71 +declare is_starext_def [code func del]
21.72 +declare isNSUCont_def [code func del]
21.73 +declare isNSCont_def [code func del]
21.74 +declare isUCont_def [code func del]
21.75 +declare NSCauchy_def [code func del]
21.76 +declare NSBseq_def [code func del]
21.77
21.78 setup {*
21.79 Code.del_funcs