# HG changeset patch
# User haftmann
# Date 1219581744 -7200
# Node ID 2aaa4a5569a6c45fa8a96c9534e30a5a0e2ff7fc
# Parent  feb0c01cf0fb168f6b6c93afa783d288609383e0
default replaces arbitrary

diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction.thy
--- 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
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction/Euclid.thy
--- 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
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction/Greatest_Common_Divisor.thy
--- 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
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction/Higman.thy
--- 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;
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction/Pigeonhole.thy
--- 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
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction/QuotRem.thy
--- 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
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Extraction/Warshall.thy
--- 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
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Lambda/WeakNorm.thy
--- 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
diff -r feb0c01cf0fb -r 2aaa4a5569a6 src/HOL/Tools/inductive_realizer.ML
--- 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)]));