default replaces arbitrary
authorhaftmann
Sun Aug 24 14:42:24 2008 +0200 (2008-08-24)
changeset 279822aaa4a5569a6
parent 27981 feb0c01cf0fb
child 27983 00e005cdceb0
default replaces arbitrary
src/HOL/Extraction.thy
src/HOL/Extraction/Euclid.thy
src/HOL/Extraction/Greatest_Common_Divisor.thy
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Extraction/QuotRem.thy
src/HOL/Extraction/Warshall.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Extraction.thy	Sun Aug 24 14:42:22 2008 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Sun Aug 24 14:42:24 2008 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4            ProofRewriteRules.rprocs true) o
     1.5        Proofterm.rewrite_proof thy
     1.6          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
     1.7 -      ProofRewriteRules.elim_vars (curry Const "arbitrary"))
     1.8 +      ProofRewriteRules.elim_vars (curry Const @{const_name default}))
     1.9  end
    1.10  *}
    1.11  
    1.12 @@ -221,6 +221,10 @@
    1.13  theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow>
    1.14    (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp
    1.15  
    1.16 +setup {*
    1.17 +  Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"})
    1.18 +*}
    1.19 +
    1.20  realizers
    1.21    impI (P, Q): "\<lambda>pq. pq"
    1.22      "\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))"
    1.23 @@ -356,7 +360,7 @@
    1.24    disjE: "Null"
    1.25      "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _"
    1.26  
    1.27 -  FalseE (P): "arbitrary"
    1.28 +  FalseE (P): "default"
    1.29      "\<Lambda> P. FalseE \<cdot> _"
    1.30  
    1.31    FalseE: "Null" "FalseE"
    1.32 @@ -366,13 +370,13 @@
    1.33  
    1.34    notI: "Null" "notI"
    1.35  
    1.36 -  notE (P, R): "\<lambda>p. arbitrary"
    1.37 +  notE (P, R): "\<lambda>p. default"
    1.38      "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
    1.39  
    1.40    notE (P): "Null"
    1.41      "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)"
    1.42  
    1.43 -  notE (R): "arbitrary"
    1.44 +  notE (R): "default"
    1.45      "\<Lambda> P R. notE \<cdot> _ \<cdot> _"
    1.46  
    1.47    notE: "Null" "notE"
    1.48 @@ -432,4 +436,8 @@
    1.49      "\<Lambda> P. classical \<cdot> _"
    1.50  *)
    1.51  
    1.52 +setup {*
    1.53 +  Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"})
    1.54 +*}
    1.55 +
    1.56  end
     2.1 --- a/src/HOL/Extraction/Euclid.thy	Sun Aug 24 14:42:22 2008 +0200
     2.2 +++ b/src/HOL/Extraction/Euclid.thy	Sun Aug 24 14:42:24 2008 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Euclid's theorem *}
     2.5  
     2.6  theory Euclid
     2.7 -imports "~~/src/HOL/NumberTheory/Factorization" Efficient_Nat Util
     2.8 +imports "~~/src/HOL/NumberTheory/Factorization" Util Efficient_Nat
     2.9  begin
    2.10  
    2.11  text {*
    2.12 @@ -207,21 +207,47 @@
    2.13  @{thm [display] factor_exists_def}
    2.14  *}
    2.15  
    2.16 -consts_code
    2.17 -  arbitrary ("(error \"arbitrary\")")
    2.18 +instantiation nat :: default
    2.19 +begin
    2.20 +
    2.21 +definition "default = (0::nat)"
    2.22 +
    2.23 +instance ..
    2.24 +
    2.25 +end
    2.26  
    2.27 -code_module Prime
    2.28 -contains Euclid
    2.29 +instantiation list :: (type) default
    2.30 +begin
    2.31 +
    2.32 +definition "default = []"
    2.33 +
    2.34 +instance ..
    2.35 +
    2.36 +end
    2.37 +
    2.38 +consts_code
    2.39 +  default ("(error \"default\")")
    2.40  
    2.41 -ML "Prime.factor_exists 1007"
    2.42 -ML "Prime.factor_exists 567"
    2.43 -ML "Prime.factor_exists 345"
    2.44 -ML "Prime.factor_exists 999"
    2.45 -ML "Prime.factor_exists 876"
    2.46 +lemma "factor_exists 1007 = [53, 19]" by evaluation
    2.47 +lemma "factor_exists 1007 = [53, 19]" by eval
    2.48 +
    2.49 +lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation
    2.50 +lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
    2.51 +
    2.52 +lemma "factor_exists 345 = [23, 5, 3]" by evaluation
    2.53 +lemma "factor_exists 345 = [23, 5, 3]" by eval
    2.54 +
    2.55 +lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation
    2.56 +lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
    2.57  
    2.58 -ML "Prime.Euclid 0"
    2.59 -ML "Prime.Euclid it"
    2.60 -ML "Prime.Euclid it"
    2.61 -ML "Prime.Euclid it"
    2.62 - 
    2.63 +lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation
    2.64 +lemma "factor_exists 876 = [73, 3, 2, 2]" by eval
    2.65 +
    2.66 +primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
    2.67 +  "iterate 0 f x = []"
    2.68 +  | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
    2.69 +
    2.70 +lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation
    2.71 +lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval
    2.72 +
    2.73  end
     3.1 --- a/src/HOL/Extraction/Greatest_Common_Divisor.thy	Sun Aug 24 14:42:22 2008 +0200
     3.2 +++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy	Sun Aug 24 14:42:24 2008 +0200
     3.3 @@ -61,13 +61,37 @@
     3.4  @{thm [display] greatest_common_divisor_def}
     3.5  *}
     3.6  
     3.7 -consts_code
     3.8 -  arbitrary ("(error \"arbitrary\")")
     3.9 +instantiation nat :: default
    3.10 +begin
    3.11 +
    3.12 +definition "default = (0::nat)"
    3.13 +
    3.14 +instance ..
    3.15  
    3.16 -code_module GCD
    3.17 -contains
    3.18 -  test = "greatest_common_divisor 7 12"
    3.19 +end
    3.20  
    3.21 -ML GCD.test
    3.22 +instantiation * :: (default, default) default
    3.23 +begin
    3.24 +
    3.25 +definition "default = (default, default)"
    3.26 +
    3.27 +instance ..
    3.28  
    3.29  end
    3.30 +
    3.31 +instantiation "fun" :: (type, default) default
    3.32 +begin
    3.33 +
    3.34 +definition "default = (\<lambda>x. default)"
    3.35 +
    3.36 +instance ..
    3.37 +
    3.38 +end
    3.39 +
    3.40 +consts_code
    3.41 +  default ("(error \"default\")")
    3.42 +
    3.43 +lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by evaluation
    3.44 +lemma "greatest_common_divisor 7 12 = (4, 3, 2)" by eval
    3.45 +
    3.46 +end
     4.1 --- a/src/HOL/Extraction/Higman.thy	Sun Aug 24 14:42:22 2008 +0200
     4.2 +++ b/src/HOL/Extraction/Higman.thy	Sun Aug 24 14:42:24 2008 +0200
     4.3 @@ -339,6 +339,17 @@
     4.4  
     4.5  subsection {* Some examples *}
     4.6  
     4.7 +instantiation LT and TT :: default
     4.8 +begin
     4.9 +
    4.10 +definition "default = L0 [] []"
    4.11 +
    4.12 +definition "default = T0 A [] [] [] R0"
    4.13 +
    4.14 +instance ..
    4.15 +
    4.16 +end
    4.17 +
    4.18  (* an attempt to express examples in HOL -- function
    4.19    mk_word :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
    4.20  where
    4.21 @@ -354,16 +365,12 @@
    4.22  by pat_completeness auto
    4.23  termination by (relation "measure ((op -) 1001)") auto
    4.24  
    4.25 -fun
    4.26 +primrec
    4.27    mk_word' :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
    4.28  where
    4.29    "mk_word' 0 = mk_word 0"
    4.30    | "mk_word' (Suc n) = (do _ \<leftarrow> mk_word 0; mk_word' n done)"*)
    4.31  
    4.32 -consts_code
    4.33 -  "arbitrary :: LT"  ("({* L0 [] [] *})")
    4.34 -  "arbitrary :: TT"  ("({* T0 A [] [] [] R0 *})")
    4.35 -
    4.36  code_module Higman
    4.37  contains
    4.38    higman = higman_idx
    4.39 @@ -415,17 +422,6 @@
    4.40  end;
    4.41  *}
    4.42  
    4.43 -definition
    4.44 -  arbitrary_LT :: LT where
    4.45 -  [symmetric, code inline]: "arbitrary_LT = arbitrary"
    4.46 -
    4.47 -definition
    4.48 -  arbitrary_TT :: TT where
    4.49 -  [symmetric, code inline]: "arbitrary_TT = arbitrary"
    4.50 -
    4.51 -code_datatype L0 L1 arbitrary_LT
    4.52 -code_datatype T0 T1 T2 arbitrary_TT
    4.53 -
    4.54  ML {*
    4.55  val a = 16807.0;
    4.56  val m = 2147483647.0;
     5.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Sun Aug 24 14:42:22 2008 +0200
     5.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Sun Aug 24 14:42:24 2008 +0200
     5.3 @@ -219,6 +219,28 @@
     5.4  we generate ML code from them.
     5.5  *}
     5.6  
     5.7 +instantiation nat :: default
     5.8 +begin
     5.9 +
    5.10 +definition "default = (0::nat)"
    5.11 +
    5.12 +instance ..
    5.13 +
    5.14 +end
    5.15 +
    5.16 +instantiation * :: (default, default) default
    5.17 +begin
    5.18 +
    5.19 +definition "default = (default, default)"
    5.20 +
    5.21 +instance ..
    5.22 +
    5.23 +end
    5.24 +
    5.25 +consts_code
    5.26 +  "default :: nat" ("{* 0::nat *}")
    5.27 +  "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
    5.28 +
    5.29  definition
    5.30    "test n u = pigeonhole n (\<lambda>m. m - 1)"
    5.31  definition
    5.32 @@ -226,25 +248,6 @@
    5.33  definition
    5.34    "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
    5.35  
    5.36 -
    5.37 -consts_code
    5.38 -  "arbitrary :: nat" ("{* 0::nat *}")
    5.39 -  "arbitrary :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
    5.40 -
    5.41 -definition
    5.42 -  arbitrary_nat_pair :: "nat \<times> nat" where
    5.43 -  [symmetric, code inline]: "arbitrary_nat_pair = arbitrary"
    5.44 -
    5.45 -definition
    5.46 -  arbitrary_nat :: nat where
    5.47 -  [symmetric, code inline]: "arbitrary_nat = arbitrary"
    5.48 -
    5.49 -code_const arbitrary_nat_pair (SML "(~1, ~1)")
    5.50 -  (* this is justified since for valid inputs this "arbitrary" will be dropped
    5.51 -     in the next recursion step in pigeonhole_def *)
    5.52 -
    5.53 -code_const  arbitrary_nat (SML "~1")
    5.54 -
    5.55  code_module PH
    5.56  contains
    5.57    test = test
     6.1 --- a/src/HOL/Extraction/QuotRem.thy	Sun Aug 24 14:42:22 2008 +0200
     6.2 +++ b/src/HOL/Extraction/QuotRem.thy	Sun Aug 24 14:42:24 2008 +0200
     6.3 @@ -41,10 +41,7 @@
     6.4    @{thm [display] division_correctness [no_vars]}
     6.5  *}
     6.6  
     6.7 -code_module Div
     6.8 -contains
     6.9 -  test = "division 9 2"
    6.10 -
    6.11 +lemma "division 9 2 = (0, 3)" by evaluation
    6.12  lemma "division 9 2 = (0, 3)" by eval
    6.13  
    6.14  end
     7.1 --- a/src/HOL/Extraction/Warshall.thy	Sun Aug 24 14:42:22 2008 +0200
     7.2 +++ b/src/HOL/Extraction/Warshall.thy	Sun Aug 24 14:42:24 2008 +0200
     7.3 @@ -257,4 +257,6 @@
     7.4    @{thm [display] warshall_correctness [no_vars]}
     7.5  *}
     7.6  
     7.7 +ML "@{code warshall}"
     7.8 +
     7.9  end
     8.1 --- a/src/HOL/Lambda/WeakNorm.thy	Sun Aug 24 14:42:22 2008 +0200
     8.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Sun Aug 24 14:42:24 2008 +0200
     8.3 @@ -265,7 +265,6 @@
     8.4  lemmas [extraction_expand] = conj_assoc listall_cons_eq
     8.5  
     8.6  extract type_NF
     8.7 -
     8.8  lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
     8.9    apply (rule iffI)
    8.10    apply (erule rtranclpR.induct)
    8.11 @@ -332,21 +331,124 @@
    8.12  
    8.13  subsection {* Generating executable code *}
    8.14  
    8.15 +instantiation NFT :: default
    8.16 +begin
    8.17 +
    8.18 +definition "default = Dummy ()"
    8.19 +
    8.20 +instance ..
    8.21 +
    8.22 +end
    8.23 +
    8.24 +instantiation dB :: default
    8.25 +begin
    8.26 +
    8.27 +definition "default = dB.Var 0"
    8.28 +
    8.29 +instance ..
    8.30 +
    8.31 +end
    8.32 +
    8.33 +instantiation * :: (default, default) default
    8.34 +begin
    8.35 +
    8.36 +definition "default = (default, default)"
    8.37 +
    8.38 +instance ..
    8.39 +
    8.40 +end
    8.41 +
    8.42 +instantiation list :: (type) default
    8.43 +begin
    8.44 +
    8.45 +definition "default = []"
    8.46 +
    8.47 +instance ..
    8.48 +
    8.49 +end
    8.50 +
    8.51 +instantiation "fun" :: (type, default) default
    8.52 +begin
    8.53 +
    8.54 +definition "default = (\<lambda>x. default)"
    8.55 +
    8.56 +instance ..
    8.57 +
    8.58 +end
    8.59 +
    8.60 +definition int_of_nat :: "nat \<Rightarrow> int" where
    8.61 +  "int_of_nat = of_nat"
    8.62 +
    8.63 +text {*
    8.64 +  The following functions convert between Isabelle's built-in {\tt term}
    8.65 +  datatype and the generated {\tt dB} datatype. This allows to
    8.66 +  generate example terms using Isabelle's parser and inspect
    8.67 +  normalized terms using Isabelle's pretty printer.
    8.68 +*}
    8.69 +
    8.70 +ML {*
    8.71 +fun dBtype_of_typ (Type ("fun", [T, U])) =
    8.72 +      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
    8.73 +  | dBtype_of_typ (TFree (s, _)) = (case explode s of
    8.74 +        ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
    8.75 +      | _ => error "dBtype_of_typ: variable name")
    8.76 +  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
    8.77 +
    8.78 +fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i)
    8.79 +  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
    8.80 +  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
    8.81 +  | dB_of_term _ = error "dB_of_term: bad term";
    8.82 +
    8.83 +fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
    8.84 +      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
    8.85 +  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
    8.86 +and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n)
    8.87 +  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
    8.88 +      let val t = term_of_dB' Ts dBt
    8.89 +      in case fastype_of1 (Ts, t) of
    8.90 +          Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
    8.91 +        | _ => error "term_of_dB: function type expected"
    8.92 +      end
    8.93 +  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
    8.94 +
    8.95 +fun typing_of_term Ts e (Bound i) =
    8.96 +      @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i))
    8.97 +  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
    8.98 +        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
    8.99 +          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
   8.100 +          typing_of_term Ts e t, typing_of_term Ts e u)
   8.101 +      | _ => error "typing_of_term: function type expected")
   8.102 +  | typing_of_term Ts e (Abs (s, T, t)) =
   8.103 +      let val dBT = dBtype_of_typ T
   8.104 +      in @{code Abs} (e, dBT, dB_of_term t,
   8.105 +        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
   8.106 +        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
   8.107 +      end
   8.108 +  | typing_of_term _ _ _ = error "typing_of_term: bad term";
   8.109 +
   8.110 +fun dummyf _ = error "dummy";
   8.111 +
   8.112 +val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
   8.113 +val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
   8.114 +val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
   8.115 +
   8.116 +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)))))"};
   8.117 +val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
   8.118 +val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
   8.119 +*}
   8.120 +
   8.121 +text {*
   8.122 +The same story again for the SML code generator.
   8.123 +*}
   8.124 +
   8.125  consts_code
   8.126 -  "arbitrary :: 'a"       ("(error \"arbitrary\")")
   8.127 -  "arbitrary :: 'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
   8.128 +  "default" ("(error \"default\")")
   8.129 +  "default :: 'a \<Rightarrow> 'b::default" ("(fn '_ => error \"default\")")
   8.130  
   8.131  code_module Norm
   8.132  contains
   8.133    test = "type_NF"
   8.134  
   8.135 -text {*
   8.136 -The following functions convert between Isabelle's built-in {\tt term}
   8.137 -datatype and the generated {\tt dB} datatype. This allows to
   8.138 -generate example terms using Isabelle's parser and inspect
   8.139 -normalized terms using Isabelle's pretty printer.
   8.140 -*}
   8.141 -
   8.142  ML {*
   8.143  fun nat_of_int 0 = Norm.zero
   8.144    | nat_of_int n = Norm.Suc (nat_of_int (n-1));
   8.145 @@ -410,66 +512,4 @@
   8.146  val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
   8.147  *}
   8.148  
   8.149 -text {*
   8.150 -The same story again for code next generation.
   8.151 -*}
   8.152 -
   8.153 -setup {*
   8.154 -  CodeTarget.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
   8.155 -*}
   8.156 -
   8.157 -definition int_of_nat :: "nat \<Rightarrow> int" where
   8.158 -  "int_of_nat = of_nat"
   8.159 -
   8.160 -ML {*
   8.161 -fun dBtype_of_typ (Type ("fun", [T, U])) =
   8.162 -      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
   8.163 -  | dBtype_of_typ (TFree (s, _)) = (case explode s of
   8.164 -        ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
   8.165 -      | _ => error "dBtype_of_typ: variable name")
   8.166 -  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
   8.167 -
   8.168 -fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i)
   8.169 -  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
   8.170 -  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
   8.171 -  | dB_of_term _ = error "dB_of_term: bad term";
   8.172 -
   8.173 -fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
   8.174 -      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
   8.175 -  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
   8.176 -and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n)
   8.177 -  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
   8.178 -      let val t = term_of_dB' Ts dBt
   8.179 -      in case fastype_of1 (Ts, t) of
   8.180 -          Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
   8.181 -        | _ => error "term_of_dB: function type expected"
   8.182 -      end
   8.183 -  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
   8.184 -
   8.185 -fun typing_of_term Ts e (Bound i) =
   8.186 -      @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i))
   8.187 -  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
   8.188 -        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
   8.189 -          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
   8.190 -          typing_of_term Ts e t, typing_of_term Ts e u)
   8.191 -      | _ => error "typing_of_term: function type expected")
   8.192 -  | typing_of_term Ts e (Abs (s, T, t)) =
   8.193 -      let val dBT = dBtype_of_typ T
   8.194 -      in @{code Abs} (e, dBT, dB_of_term t,
   8.195 -        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
   8.196 -        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
   8.197 -      end
   8.198 -  | typing_of_term _ _ _ = error "typing_of_term: bad term";
   8.199 -
   8.200 -fun dummyf _ = error "dummy";
   8.201 -
   8.202 -val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
   8.203 -val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
   8.204 -val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
   8.205 -
   8.206 -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)))))"};
   8.207 -val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
   8.208 -val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
   8.209 -*}
   8.210 -
   8.211  end
     9.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Aug 24 14:42:22 2008 +0200
     9.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Aug 24 14:42:24 2008 +0200
     9.3 @@ -211,7 +211,7 @@
     9.4        let
     9.5          val fs = map (fn (rule, (ivs, intr)) =>
     9.6            fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
     9.7 -      in if dummy then Const ("arbitrary",
     9.8 +      in if dummy then Const ("HOL.default_class.default",
     9.9            HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
    9.10          else fs
    9.11        end) (premss ~~ dummies);
    9.12 @@ -438,7 +438,7 @@
    9.13          val r = if null Ps then Extraction.nullt
    9.14            else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
    9.15              (if dummy then
    9.16 -               [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
    9.17 +               [Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))]
    9.18               else []) @
    9.19              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
    9.20              [Bound (length prems)]));