--- a/src/HOL/Complex/NSCA.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Complex/NSCA.thy Wed Jul 02 07:11:57 2008 +0200
@@ -14,10 +14,9 @@
SComplex :: "hcomplex set" where
"SComplex \<equiv> Standard"
-definition
- stc :: "hcomplex => hcomplex" where
- --{* standard part map*}
- "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+definition --{* standard part map*}
+ stc :: "hcomplex => hcomplex" where
+ [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
--- a/src/HOL/Complex/NSComplex.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Complex/NSComplex.thy Wed Jul 02 07:11:57 2008 +0200
@@ -26,11 +26,11 @@
definition
hRe :: "hcomplex => hypreal" where
- "hRe = *f* Re"
+ [code func del]: "hRe = *f* Re"
definition
hIm :: "hcomplex => hypreal" where
- "hIm = *f* Im"
+ [code func del]: "hIm = *f* Im"
(*------ imaginary unit ----------*)
@@ -43,22 +43,22 @@
definition
hcnj :: "hcomplex => hcomplex" where
- "hcnj = *f* cnj"
+ [code func del]: "hcnj = *f* cnj"
(*------------ Argand -------------*)
definition
hsgn :: "hcomplex => hcomplex" where
- "hsgn = *f* sgn"
+ [code func del]: "hsgn = *f* sgn"
definition
harg :: "hcomplex => hypreal" where
- "harg = *f* arg"
+ [code func del]: "harg = *f* arg"
definition
(* abbreviation for (cos a + i sin a) *)
hcis :: "hypreal => hcomplex" where
- "hcis = *f* cis"
+ [code func del]:"hcis = *f* cis"
(*----- injection from hyperreals -----*)
@@ -69,16 +69,16 @@
definition
(* abbreviation for r*(cos a + i sin a) *)
hrcis :: "[hypreal, hypreal] => hcomplex" where
- "hrcis = *f2* rcis"
+ [code func del]: "hrcis = *f2* rcis"
(*------------ e ^ (x + iy) ------------*)
definition
hexpi :: "hcomplex => hcomplex" where
- "hexpi = *f* expi"
+ [code func del]: "hexpi = *f* expi"
definition
HComplex :: "[hypreal,hypreal] => hcomplex" where
- "HComplex = *f2* Complex"
+ [code func del]: "HComplex = *f2* Complex"
lemmas hcomplex_defs [transfer_unfold] =
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
--- a/src/HOL/Hyperreal/HDeriv.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HDeriv.thy Wed Jul 02 07:11:57 2008 +0200
@@ -27,7 +27,7 @@
definition
increment :: "[real=>real,real,hypreal] => hypreal" where
- "increment f x h = (@inc. f NSdifferentiable x &
+ [code func del]: "increment f x h = (@inc. f NSdifferentiable x &
inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
--- a/src/HOL/Hyperreal/HLim.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HLim.thy Wed Jul 02 07:11:57 2008 +0200
@@ -16,18 +16,18 @@
definition
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
- "f -- a --NS> L =
+ [code func del]: "f -- a --NS> L =
(\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
definition
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
--{*NS definition dispenses with limit notions*}
- "isNSCont f a = (\<forall>y. y @= star_of a -->
+ [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
( *f* f) y @= star_of (f a))"
definition
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+ [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
subsection {* Limits of Functions *}
--- a/src/HOL/Hyperreal/HLog.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HLog.thy Wed Jul 02 07:11:57 2008 +0200
@@ -20,14 +20,11 @@
definition
powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
- "x powhr a = starfun2 (op powr) x a"
+ [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
definition
hlog :: "[hypreal,hypreal] => hypreal" where
- "hlog a x = starfun2 log a x"
-
-declare powhr_def [transfer_unfold]
-declare hlog_def [transfer_unfold]
+ [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
by (simp add: powhr_def starfun2_star_n)
--- a/src/HOL/Hyperreal/HSEQ.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HSEQ.thy Wed Jul 02 07:11:57 2008 +0200
@@ -16,7 +16,7 @@
NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----NS> (_))" [60, 60] 60) where
--{*Nonstandard definition of convergence of sequence*}
- "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+ [code func del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
definition
nslim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -31,12 +31,12 @@
definition
NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition for bounded sequence*}
- "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+ [code func del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
definition
NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
--{*Nonstandard definition*}
- "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+ [code func del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
subsection {* Limits of Sequences *}
--- a/src/HOL/Hyperreal/HSeries.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy Wed Jul 02 07:11:57 2008 +0200
@@ -13,7 +13,7 @@
definition
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
- "sumhr =
+ [code func del]: "sumhr =
(%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
definition
@@ -22,7 +22,7 @@
definition
NSsummable :: "(nat=>real) => bool" where
- "NSsummable f = (\<exists>s. f NSsums s)"
+ [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
definition
NSsuminf :: "(nat=>real) => real" where
--- a/src/HOL/Hyperreal/HyperDef.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Wed Jul 02 07:11:57 2008 +0200
@@ -47,7 +47,7 @@
begin
definition
- star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
+ star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)"
instance ..
@@ -111,9 +111,7 @@
definition
of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
- "of_hypreal = *f* of_real"
-
-declare of_hypreal_def [transfer_unfold]
+ [transfer_unfold, code func del]: "of_hypreal = *f* of_real"
lemma Standard_of_hypreal [simp]:
"r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
@@ -427,11 +425,9 @@
subsection{*Powers with Hypernatural Exponents*}
-definition
+definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
+ hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N"
(* hypernatural powers of hyperreals *)
- pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
- hyperpow_def [transfer_unfold]:
- "R pow N = ( *f2* op ^) R N"
lemma Standard_hyperpow [simp]:
"\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"
--- a/src/HOL/Hyperreal/HyperNat.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Wed Jul 02 07:11:57 2008 +0200
@@ -19,7 +19,7 @@
definition
hSuc :: "hypnat => hypnat" where
- hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
+ hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
subsection{*Properties Transferred from Naturals*}
@@ -367,7 +367,7 @@
definition
of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
- of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
+ of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
by transfer (rule of_nat_0)
--- a/src/HOL/Hyperreal/Integration.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Wed Jul 02 07:11:57 2008 +0200
@@ -16,29 +16,29 @@
--{*Partitions and tagged partitions etc.*}
partition :: "[(real*real),nat => real] => bool" where
- "partition = (%(a,b) D. D 0 = a &
+ [code func del]: "partition = (%(a,b) D. D 0 = a &
(\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
(\<forall>n \<ge> N. D(n) = b)))"
definition
psize :: "(nat => real) => nat" where
- "psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+ [code func del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
(\<forall>n \<ge> N. D(n) = D(N)))"
definition
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
- "tpart = (%(a,b) (D,p). partition(a,b) D &
+ [code func del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
(\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
--{*Gauges and gauge-fine divisions*}
definition
gauge :: "[real => bool, real => real] => bool" where
- "gauge E g = (\<forall>x. E x --> 0 < g(x))"
+ [code func del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
definition
fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
- "fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
+ [code func del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
--{*Riemann sum*}
@@ -50,7 +50,7 @@
definition
Integral :: "[(real*real),real=>real,real] => bool" where
- "Integral = (%(a,b) f k. \<forall>e > 0.
+ [code func del]: "Integral = (%(a,b) f k. \<forall>e > 0.
(\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
\<bar>rsum(D,p) f - k\<bar> < e)))"
--- a/src/HOL/Hyperreal/Lim.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Jul 02 07:11:57 2008 +0200
@@ -16,7 +16,7 @@
definition
LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
- "f -- a --> L =
+ [code func del]: "f -- a --> L =
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
--> norm (f x - L) < r)"
@@ -26,7 +26,7 @@
definition
isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
+ [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)"
subsection {* Limits of Functions *}
--- a/src/HOL/Hyperreal/NSA.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Jul 02 07:11:57 2008 +0200
@@ -13,19 +13,19 @@
definition
hnorm :: "'a::norm star \<Rightarrow> real star" where
- "hnorm = *f* norm"
+ [transfer_unfold]: "hnorm = *f* norm"
definition
Infinitesimal :: "('a::real_normed_vector) star set" where
- "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
+ [code func del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
definition
HFinite :: "('a::real_normed_vector) star set" where
- "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
+ [code func del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
definition
HInfinite :: "('a::real_normed_vector) star set" where
- "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
+ [code func del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
definition
approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
@@ -58,10 +58,7 @@
definition
scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
- "scaleHR = starfun2 scaleR"
-
-declare hnorm_def [transfer_unfold]
-declare scaleHR_def [transfer_unfold]
+ [transfer_unfold, code func del]: "scaleHR = starfun2 scaleR"
lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
by (simp add: hnorm_def)
--- a/src/HOL/Hyperreal/SEQ.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Wed Jul 02 07:11:57 2008 +0200
@@ -15,13 +15,13 @@
definition
Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
--{*Standard definition of sequence converging to zero*}
- "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
+ [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
definition
LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----> (_))" [60, 60] 60) where
--{*Standard definition of convergence of sequence*}
- "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
+ [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
definition
lim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -36,22 +36,22 @@
definition
Bseq :: "(nat => 'a::real_normed_vector) => bool" where
--{*Standard definition for bounded sequence*}
- "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+ [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
definition
monoseq :: "(nat=>real)=>bool" where
--{*Definition for monotonicity*}
- "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
+ [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))"
definition
subseq :: "(nat => nat) => bool" where
--{*Definition of subsequence*}
- "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
+ [code func del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
definition
Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
--{*Standard definition of the Cauchy condition*}
- "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
+ [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
subsection {* Bounded Sequences *}
--- a/src/HOL/Hyperreal/Star.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/Star.thy Wed Jul 02 07:11:57 2008 +0200
@@ -17,12 +17,12 @@
definition
InternalSets :: "'a star set set" where
- "InternalSets = {X. \<exists>As. X = *sn* As}"
+ [code func del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
definition
(* nonstandard extension of function *)
is_starext :: "['a star => 'a star, 'a => 'a] => bool" where
- "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+ [code func del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
definition
@@ -32,7 +32,7 @@
definition
InternalFuns :: "('a star => 'b star) set" where
- "InternalFuns = {X. \<exists>F. X = *fn* F}"
+ [code func del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
(*--------------------------------------------------------
--- a/src/HOL/Hyperreal/StarDef.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy Wed Jul 02 07:11:57 2008 +0200
@@ -290,9 +290,8 @@
subsection {* Internal predicates *}
-definition
- unstar :: "bool star \<Rightarrow> bool" where
- "unstar b = (b = star_of True)"
+definition unstar :: "bool star \<Rightarrow> bool" where
+ [code func del]: "unstar b \<longleftrightarrow> b = star_of True"
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -433,7 +432,7 @@
begin
definition
- star_zero_def: "0 \<equiv> star_of 0"
+ star_zero_def [code func del]: "0 \<equiv> star_of 0"
instance ..
@@ -443,7 +442,7 @@
begin
definition
- star_one_def: "1 \<equiv> star_of 1"
+ star_one_def [code func del]: "1 \<equiv> star_of 1"
instance ..
@@ -453,7 +452,7 @@
begin
definition
- star_add_def: "(op +) \<equiv> *f2* (op +)"
+ star_add_def [code func del]: "(op +) \<equiv> *f2* (op +)"
instance ..
@@ -463,7 +462,7 @@
begin
definition
- star_mult_def: "(op *) \<equiv> *f2* (op *)"
+ star_mult_def [code func del]: "(op *) \<equiv> *f2* (op *)"
instance ..
@@ -473,7 +472,7 @@
begin
definition
- star_minus_def: "uminus \<equiv> *f* uminus"
+ star_minus_def [code func del]: "uminus \<equiv> *f* uminus"
instance ..
@@ -483,7 +482,7 @@
begin
definition
- star_diff_def: "(op -) \<equiv> *f2* (op -)"
+ star_diff_def [code func del]: "(op -) \<equiv> *f2* (op -)"
instance ..
--- a/src/HOL/Lambda/WeakNorm.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Wed Jul 02 07:11:57 2008 +0200
@@ -418,33 +418,27 @@
CodeTarget.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
*}
-definition
- int_of_nat :: "nat \<Rightarrow> int" where
+definition int_of_nat :: "nat \<Rightarrow> int" where
"int_of_nat = of_nat"
-export_code type_NF nat int_of_nat in SML module_name Norm
-
ML {*
-val nat_of_int = Norm.nat;
-val int_of_nat = Norm.int_of_nat;
-
fun dBtype_of_typ (Type ("fun", [T, U])) =
- Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
+ @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
| dBtype_of_typ (TFree (s, _)) = (case explode s of
- ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
+ ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
| _ => error "dBtype_of_typ: variable name")
| dBtype_of_typ _ = error "dBtype_of_typ: bad type";
-fun dB_of_term (Bound i) = Norm.Var (nat_of_int i)
- | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u)
- | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)
+fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i)
+ | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
+ | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
| dB_of_term _ = error "dB_of_term: bad term";
-fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =
+fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
Abs ("x", T, term_of_dB (T :: Ts) U dBt)
| term_of_dB Ts _ dBt = term_of_dB' Ts dBt
-and term_of_dB' Ts (Norm.Var n) = Bound (int_of_nat n)
- | term_of_dB' Ts (Norm.App (dBt, dBu)) =
+and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n)
+ | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
let val t = term_of_dB' Ts dBt
in case fastype_of1 (Ts, t) of
Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
@@ -453,30 +447,28 @@
| term_of_dB' _ _ = error "term_of_dB: term not in normal form";
fun typing_of_term Ts e (Bound i) =
- Norm.Vara (e, nat_of_int i, dBtype_of_typ (nth Ts i))
+ @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i))
| typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
- Type ("fun", [T, U]) => Norm.Appb (e, dB_of_term t,
+ Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
typing_of_term Ts e t, typing_of_term Ts e u)
| _ => error "typing_of_term: function type expected")
| typing_of_term Ts e (Abs (s, T, t)) =
let val dBT = dBtype_of_typ T
- in Norm.Absb (e, dBT, dB_of_term t,
+ in @{code Abs} (e, dBT, dB_of_term t,
dBtype_of_typ (fastype_of1 (T :: Ts, t)),
- typing_of_term (T :: Ts) (Norm.shift e Norm.Zero_nat dBT) t)
+ typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
end
| typing_of_term _ _ _ = error "typing_of_term: bad term";
fun dummyf _ = error "dummy";
-*}
-ML {*
val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
-val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
+val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
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)))))"};
-val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
+val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
--- a/src/HOL/Library/Univ_Poly.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Wed Jul 02 07:11:57 2008 +0200
@@ -72,7 +72,7 @@
definition (in semiring_0)
divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "divides" 70) where
- "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+ [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
--{*order of a polynomial*}
definition (in ring_1) order :: "'a => 'a list => nat" where
--- a/src/HOL/Real/ContNotDenum.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Real/ContNotDenum.thy Wed Jul 02 07:11:57 2008 +0200
@@ -393,16 +393,17 @@
subsubsection {* Definition *}
-consts newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
-primrec
-"newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
-"newInt (Suc n) f =
- (SOME e. (\<exists>e1 e2.
- e1 < e2 \<and>
- e = closed_int e1 e2 \<and>
- e \<subseteq> (newInt n f) \<and>
- (f (Suc n)) \<notin> e)
- )"
+primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
+ "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
+ | "newInt (Suc n) f =
+ (SOME e. (\<exists>e1 e2.
+ e1 < e2 \<and>
+ e = closed_int e1 e2 \<and>
+ e \<subseteq> (newInt n f) \<and>
+ (f (Suc n)) \<notin> e)
+ )"
+
+declare newInt.simps [code func del]
subsubsection {* Properties *}
--- a/src/HOL/Real/RComplete.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Real/RComplete.thy Wed Jul 02 07:11:57 2008 +0200
@@ -434,7 +434,7 @@
definition
floor :: "real => int" where
- "floor r = (LEAST n::int. r < real (n+1))"
+ [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
definition
ceiling :: "real => int" where
--- a/src/HOL/Real/RealVector.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Real/RealVector.thy Wed Jul 02 07:11:57 2008 +0200
@@ -264,7 +264,7 @@
definition
Reals :: "'a::real_algebra_1 set" where
- "Reals \<equiv> range of_real"
+ [code func del]: "Reals \<equiv> range of_real"
notation (xsymbols)
Reals ("\<real>")
--- a/src/HOL/ex/ExecutableContent.thy Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/ex/ExecutableContent.thy Wed Jul 02 07:11:57 2008 +0200
@@ -33,63 +33,25 @@
(*FIXME distribute to theories*)
declare divides_def [code func del] -- "Univ_Poly"
-declare unstar_def [code func del] -- "StarDef"
-declare star_one_def [code func del] -- "StarDef"
-declare star_mult_def [code func del] -- "StarDef"
-declare star_add_def [code func del] -- "StarDef"
-declare star_zero_def [code func del] -- "StarDef"
declare star_minus_def [code func del] -- "StarDef"
-declare star_diff_def [code func del] -- "StarDef"
-declare Reals_def [code func del] -- "RealVector"
-declare star_scaleR_def [code func del] -- "HyperDef"
-declare hyperpow_def [code func del] -- HyperDef
-declare Infinitesimal_def [code func del] -- NSA
-declare HFinite_def [code func del] -- NSA
-declare floor_def [code func del] -- RComplete
-declare LIMSEQ_def [code func del] -- SEQ
-declare partition_def [code func del] -- Integration
-declare Integral_def [code func del] -- Integration
-declare tpart_def [code func del] -- Integration
-declare psize_def [code func del] -- Integration
-declare gauge_def [code func del] -- Integration
-declare fine_def [code func del] -- Integration
-declare sumhr_def [code func del] -- HSeries
-declare NSsummable_def [code func del] -- HSeries
-declare NSLIMSEQ_def [code func del] -- HSEQ
-declare newInt.simps [code func del] -- ContNotDenum
-declare LIM_def [code func del] -- Lim
-declare NSLIM_def [code func del] -- HLim
-declare HComplex_def [code func del]
-declare of_hypnat_def [code func del]
-declare InternalSets_def [code func del]
-declare InternalFuns_def [code func del]
-declare increment_def [code func del]
-declare is_starext_def [code func del]
-declare hrcis_def [code func del]
-declare hexpi_def [code func del]
-declare hsgn_def [code func del]
-declare hcnj_def [code func del]
-declare hcis_def [code func del]
-declare harg_def [code func del]
-declare isNSUCont_def [code func del]
-declare hRe_def [code func del]
-declare hIm_def [code func del]
-declare HInfinite_def [code func del]
-declare hSuc_def [code func del]
-declare NSCauchy_def [code func del]
-declare of_hypreal_def [code func del]
-declare isNSCont_def [code func del]
+declare Zseq_def [code func del]
+declare Bseq_def [code func del]
declare monoseq_def [code func del]
-declare scaleHR_def [code func del]
-declare isUCont_def [code func del]
-declare NSBseq_def [code func del]
+declare Cauchy_def [code func del]
declare subseq_def [code func del]
-declare Cauchy_def [code func del]
declare powhr_def [code func del]
declare hlog_def [code func del]
-declare Zseq_def [code func del]
-declare Bseq_def [code func del]
+declare scaleHR_def [code func del]
declare stc_def [code func del]
+declare increment_def [code func del]
+declare of_hypreal_def [code func del]
+declare HInfinite_def [code func del]
+declare is_starext_def [code func del]
+declare isNSUCont_def [code func del]
+declare isNSCont_def [code func del]
+declare isUCont_def [code func del]
+declare NSCauchy_def [code func del]
+declare NSBseq_def [code func del]
setup {*
Code.del_funcs