--- a/src/HOL/Extraction.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction.thy Sun Aug 24 14:42:24 2008 +0200
@@ -44,7 +44,7 @@
ProofRewriteRules.rprocs true) o
Proofterm.rewrite_proof thy
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
- ProofRewriteRules.elim_vars (curry Const "arbitrary"))
+ ProofRewriteRules.elim_vars (curry Const @{const_name default}))
end
*}
@@ -221,6 +221,10 @@
theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
(\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
+setup {*
+ Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"})
+*}
+
realizers
impI (P, Q): "\<lambda>pq. pq"
"\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
@@ -356,7 +360,7 @@
disjE: "Null"
"\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
- FalseE (P): "arbitrary"
+ FalseE (P): "default"
"\<Lambda> P. FalseE \<cdot> _"
FalseE: "Null" "FalseE"
@@ -366,13 +370,13 @@
notI: "Null" "notI"
- notE (P, R): "\<lambda>p. arbitrary"
+ notE (P, R): "\<lambda>p. default"
"\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
notE (P): "Null"
"\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
- notE (R): "arbitrary"
+ notE (R): "default"
"\<Lambda> P R. notE \<cdot> _ \<cdot> _"
notE: "Null" "notE"
@@ -432,4 +436,8 @@
"\<Lambda> P. classical \<cdot> _"
*)
+setup {*
+ Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"})
+*}
+
end
--- a/src/HOL/Extraction/Euclid.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/Euclid.thy Sun Aug 24 14:42:24 2008 +0200
@@ -8,7 +8,7 @@
header {* Euclid's theorem *}
theory Euclid
-imports "~~/src/HOL/NumberTheory/Factorization" Efficient_Nat Util
+imports "~~/src/HOL/NumberTheory/Factorization" Util Efficient_Nat
begin
text {*
@@ -207,21 +207,47 @@
@{thm [display] factor_exists_def}
*}
-consts_code
- arbitrary ("(error \"arbitrary\")")
+instantiation nat :: default
+begin
+
+definition "default = (0::nat)"
+
+instance ..
+
+end
-code_module Prime
-contains Euclid
+instantiation list :: (type) default
+begin
+
+definition "default = []"
+
+instance ..
+
+end
+
+consts_code
+ default ("(error \"default\")")
-ML "Prime.factor_exists 1007"
-ML "Prime.factor_exists 567"
-ML "Prime.factor_exists 345"
-ML "Prime.factor_exists 999"
-ML "Prime.factor_exists 876"
+lemma "factor_exists 1007 = [53, 19]" by evaluation
+lemma "factor_exists 1007 = [53, 19]" by eval
+
+lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation
+lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
+
+lemma "factor_exists 345 = [23, 5, 3]" by evaluation
+lemma "factor_exists 345 = [23, 5, 3]" by eval
+
+lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
+lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
-ML "Prime.Euclid 0"
-ML "Prime.Euclid it"
-ML "Prime.Euclid it"
-ML "Prime.Euclid it"
-
+lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
+lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
+
+primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
+ "iterate 0 f x = []"
+ | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
+
+lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
+lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
+
end
--- a/src/HOL/Extraction/Greatest_Common_Divisor.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy Sun Aug 24 14:42:24 2008 +0200
@@ -61,13 +61,37 @@
@{thm [display] greatest_common_divisor_def}
*}
-consts_code
- arbitrary ("(error \"arbitrary\")")
+instantiation nat :: default
+begin
+
+definition "default = (0::nat)"
+
+instance ..
-code_module GCD
-contains
- test = "greatest_common_divisor 7 12"
+end
-ML GCD.test
+instantiation * :: (default, default) default
+begin
+
+definition "default = (default, default)"
+
+instance ..
end
+
+instantiation "fun" :: (type, default) default
+begin
+
+definition "default = (\<lambda>x. default)"
+
+instance ..
+
+end
+
+consts_code
+ default ("(error \"default\")")
+
+lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by evaluation
+lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval
+
+end
--- a/src/HOL/Extraction/Higman.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/Higman.thy Sun Aug 24 14:42:24 2008 +0200
@@ -339,6 +339,17 @@
subsection {* Some examples *}
+instantiation LT and TT :: default
+begin
+
+definition "default = L0 [] []"
+
+definition "default = T0 A [] [] [] R0"
+
+instance ..
+
+end
+
(* an attempt to express examples in HOL -- function
mk_word :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
where
@@ -354,16 +365,12 @@
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto
-fun
+primrec
mk_word' :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
where
"mk_word' 0 = mk_word 0"
| "mk_word' (Suc n) = (do _ \<leftarrow> mk_word 0; mk_word' n done)"*)
-consts_code
- "arbitrary :: LT" ("({* L0 [] [] *})")
- "arbitrary :: TT" ("({* T0 A [] [] [] R0 *})")
-
code_module Higman
contains
higman = higman_idx
@@ -415,17 +422,6 @@
end;
*}
-definition
- arbitrary_LT :: LT where
- [symmetric, code inline]: "arbitrary_LT = arbitrary"
-
-definition
- arbitrary_TT :: TT where
- [symmetric, code inline]: "arbitrary_TT = arbitrary"
-
-code_datatype L0 L1 arbitrary_LT
-code_datatype T0 T1 T2 arbitrary_TT
-
ML {*
val a = 16807.0;
val m = 2147483647.0;
--- a/src/HOL/Extraction/Pigeonhole.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy Sun Aug 24 14:42:24 2008 +0200
@@ -219,6 +219,28 @@
we generate ML code from them.
*}
+instantiation nat :: default
+begin
+
+definition "default = (0::nat)"
+
+instance ..
+
+end
+
+instantiation * :: (default, default) default
+begin
+
+definition "default = (default, default)"
+
+instance ..
+
+end
+
+consts_code
+ "default :: nat" ("{* 0::nat *}")
+ "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
+
definition
"test n u = pigeonhole n (\<lambda>m. m - 1)"
definition
@@ -226,25 +248,6 @@
definition
"test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
-
-consts_code
- "arbitrary :: nat" ("{* 0::nat *}")
- "arbitrary :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
-
-definition
- arbitrary_nat_pair :: "nat \<times> nat" where
- [symmetric, code inline]: "arbitrary_nat_pair = arbitrary"
-
-definition
- arbitrary_nat :: nat where
- [symmetric, code inline]: "arbitrary_nat = arbitrary"
-
-code_const arbitrary_nat_pair (SML "(~1, ~1)")
- (* this is justified since for valid inputs this "arbitrary" will be dropped
- in the next recursion step in pigeonhole_def *)
-
-code_const arbitrary_nat (SML "~1")
-
code_module PH
contains
test = test
--- a/src/HOL/Extraction/QuotRem.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/QuotRem.thy Sun Aug 24 14:42:24 2008 +0200
@@ -41,10 +41,7 @@
@{thm [display] division_correctness [no_vars]}
*}
-code_module Div
-contains
- test = "division 9 2"
-
+lemma "division 9 2 = (0, 3)" by evaluation
lemma "division 9 2 = (0, 3)" by eval
end
--- a/src/HOL/Extraction/Warshall.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/Warshall.thy Sun Aug 24 14:42:24 2008 +0200
@@ -257,4 +257,6 @@
@{thm [display] warshall_correctness [no_vars]}
*}
+ML "@{code warshall}"
+
end
--- a/src/HOL/Lambda/WeakNorm.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Sun Aug 24 14:42:24 2008 +0200
@@ -265,7 +265,6 @@
lemmas [extraction_expand] = conj_assoc listall_cons_eq
extract type_NF
-
lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
apply (rule iffI)
apply (erule rtranclpR.induct)
@@ -332,21 +331,124 @@
subsection {* Generating executable code *}
+instantiation NFT :: default
+begin
+
+definition "default = Dummy ()"
+
+instance ..
+
+end
+
+instantiation dB :: default
+begin
+
+definition "default = dB.Var 0"
+
+instance ..
+
+end
+
+instantiation * :: (default, default) default
+begin
+
+definition "default = (default, default)"
+
+instance ..
+
+end
+
+instantiation list :: (type) default
+begin
+
+definition "default = []"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, default) default
+begin
+
+definition "default = (\<lambda>x. default)"
+
+instance ..
+
+end
+
+definition int_of_nat :: "nat \<Rightarrow> int" where
+ "int_of_nat = of_nat"
+
+text {*
+ The following functions convert between Isabelle's built-in {\tt term}
+ datatype and the generated {\tt dB} datatype. This allows to
+ generate example terms using Isabelle's parser and inspect
+ normalized terms using Isabelle's pretty printer.
+*}
+
+ML {*
+fun dBtype_of_typ (Type ("fun", [T, U])) =
+ @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
+ | dBtype_of_typ (TFree (s, _)) = (case explode s of
+ ["'", 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) = @{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])) (@{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 (@{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
+ | _ => error "term_of_dB: function type expected"
+ end
+ | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
+
+fun typing_of_term Ts e (Bound 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]) => @{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 @{code Abs} (e, dBT, dB_of_term t,
+ dBtype_of_typ (fastype_of1 (T :: Ts, 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";
+
+val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
+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, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
+val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
+*}
+
+text {*
+The same story again for the SML code generator.
+*}
+
consts_code
- "arbitrary :: 'a" ("(error \"arbitrary\")")
- "arbitrary :: 'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
+ "default" ("(error \"default\")")
+ "default :: 'a \<Rightarrow> 'b::default" ("(fn '_ => error \"default\")")
code_module Norm
contains
test = "type_NF"
-text {*
-The following functions convert between Isabelle's built-in {\tt term}
-datatype and the generated {\tt dB} datatype. This allows to
-generate example terms using Isabelle's parser and inspect
-normalized terms using Isabelle's pretty printer.
-*}
-
ML {*
fun nat_of_int 0 = Norm.zero
| nat_of_int n = Norm.Suc (nat_of_int (n-1));
@@ -410,66 +512,4 @@
val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
*}
-text {*
-The same story again for code next generation.
-*}
-
-setup {*
- CodeTarget.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
-*}
-
-definition int_of_nat :: "nat \<Rightarrow> int" where
- "int_of_nat = of_nat"
-
-ML {*
-fun dBtype_of_typ (Type ("fun", [T, U])) =
- @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
- | dBtype_of_typ (TFree (s, _)) = (case explode s of
- ["'", 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) = @{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])) (@{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 (@{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
- | _ => error "term_of_dB: function type expected"
- end
- | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
-
-fun typing_of_term Ts e (Bound 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]) => @{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 @{code Abs} (e, dBT, dB_of_term t,
- dBtype_of_typ (fastype_of1 (T :: Ts, 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";
-
-val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
-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, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
-val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
-*}
-
end
--- a/src/HOL/Tools/inductive_realizer.ML Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Aug 24 14:42:24 2008 +0200
@@ -211,7 +211,7 @@
let
val fs = map (fn (rule, (ivs, intr)) =>
fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
- in if dummy then Const ("arbitrary",
+ in if dummy then Const ("HOL.default_class.default",
HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
else fs
end) (premss ~~ dummies);
@@ -438,7 +438,7 @@
val r = if null Ps then Extraction.nullt
else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
(if dummy then
- [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
+ [Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))]
else []) @
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
[Bound (length prems)]));