Isar definitions are now added explicitly to code theorem table
authorhaftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 227445cbe966d67a2
parent 22743 e2b06bfe471a
child 22745 17bc6af2011e
Isar definitions are now added explicitly to code theorem table
src/HOL/Code_Generator.thy
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/FixedPoint.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/Numeral.thy
src/HOL/Integ/Presburger.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/SCT_Definition.thy
src/HOL/Library/SCT_Implementation.thy
src/HOL/Map.thy
src/HOL/Nat.thy
src/HOL/Presburger.thy
src/HOL/Product_Type.thy
src/HOL/Record.thy
src/HOL/Set.thy
src/Pure/Isar/ROOT.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/specification.ML
src/Pure/Tools/ROOT.ML
src/Pure/Tools/codegen_data.ML
     1.1 --- a/src/HOL/Code_Generator.thy	Fri Apr 20 11:21:41 2007 +0200
     1.2 +++ b/src/HOL/Code_Generator.thy	Fri Apr 20 11:21:42 2007 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4  
     1.5  definition
     1.6    if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
     1.7 -  "if_delayed b f g = (if b then f True else g False)"
     1.8 +  [code nofunc]: "if_delayed b f g = (if b then f True else g False)"
     1.9  
    1.10  lemma [code func]:
    1.11    shows "if_delayed True f g = f True"
    1.12 @@ -230,7 +230,6 @@
    1.13    "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
    1.14    unfolding if_delayed_def ..
    1.15  
    1.16 -
    1.17  hide (open) const if_delayed
    1.18  
    1.19  end
     2.1 --- a/src/HOL/Datatype.thy	Fri Apr 20 11:21:41 2007 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Fri Apr 20 11:21:42 2007 +0200
     2.3 @@ -102,7 +102,7 @@
     2.4  
     2.5  (** apfst -- can be used in similar type definitions **)
     2.6  
     2.7 -lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)"
     2.8 +lemma apfst_conv [simp, code func]: "apfst f (a, b) = (f a, b)"
     2.9  by (simp add: apfst_def)
    2.10  
    2.11  
    2.12 @@ -697,10 +697,10 @@
    2.13    option_map :: "('a => 'b) => ('a option => 'b option)"
    2.14    "option_map == %f y. case y of None => None | Some x => Some (f x)"
    2.15  
    2.16 -lemma option_map_None [simp]: "option_map f None = None"
    2.17 +lemma option_map_None [simp, code func]: "option_map f None = None"
    2.18    by (simp add: option_map_def)
    2.19  
    2.20 -lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
    2.21 +lemma option_map_Some [simp, code func]: "option_map f (Some x) = Some (f x)"
    2.22    by (simp add: option_map_def)
    2.23  
    2.24  lemma option_map_is_None [iff]:
     3.1 --- a/src/HOL/Divides.thy	Fri Apr 20 11:21:41 2007 +0200
     3.2 +++ b/src/HOL/Divides.thy	Fri Apr 20 11:21:42 2007 +0200
     3.3 @@ -871,9 +871,9 @@
     3.4    done
     3.5  
     3.6  
     3.7 -subsection {* Code generation for div and mod *}
     3.8 +subsection {* Code generation for div, mod and dvd on nat *}
     3.9  
    3.10 -definition
    3.11 +definition [code nofunc]:
    3.12    "divmod (m\<Colon>nat) n = (m div n, m mod n)"
    3.13  
    3.14  lemma divmod_zero [code]: "divmod m 0 = (0, m)"
    3.15 @@ -893,13 +893,22 @@
    3.16  lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
    3.17    unfolding divmod_def by simp
    3.18  
    3.19 +definition
    3.20 +  dvd_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
    3.21 +where
    3.22 +  "dvd_nat m n \<longleftrightarrow> n mod m = (0 \<Colon> nat)"
    3.23 +
    3.24 +lemma [code inline]:
    3.25 +  "op dvd = dvd_nat"
    3.26 +  by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)
    3.27 +
    3.28  code_modulename SML
    3.29    Divides Integer
    3.30  
    3.31  code_modulename OCaml
    3.32    Divides Integer
    3.33  
    3.34 -hide (open) const divmod
    3.35 +hide (open) const divmod dvd_nat
    3.36  
    3.37  subsection {* Legacy bindings *}
    3.38  
     4.1 --- a/src/HOL/FixedPoint.thy	Fri Apr 20 11:21:41 2007 +0200
     4.2 +++ b/src/HOL/FixedPoint.thy	Fri Apr 20 11:21:42 2007 +0200
     4.3 @@ -198,6 +198,8 @@
     4.4    apply (iprover elim: le_funE)
     4.5    done
     4.6  
     4.7 +lemmas [code nofunc] = Inf_fun_def
     4.8 +
     4.9  theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
    4.10    apply (rule order_antisym)
    4.11    apply (rule Sup_least)
    4.12 @@ -219,6 +221,8 @@
    4.13    Inf_set_def: "Inf S \<equiv> \<Inter>S"
    4.14    by intro_classes (auto simp add: Inf_set_def)
    4.15  
    4.16 +lemmas [code nofunc] = Inf_set_def
    4.17 +
    4.18  theorem Sup_set_eq: "Sup S = \<Union>S"
    4.19    apply (rule subset_antisym)
    4.20    apply (rule Sup_least)
     5.1 --- a/src/HOL/Fun.thy	Fri Apr 20 11:21:41 2007 +0200
     5.2 +++ b/src/HOL/Fun.thy	Fri Apr 20 11:21:42 2007 +0200
     5.3 @@ -12,7 +12,7 @@
     5.4  
     5.5  constdefs
     5.6    fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
     5.7 -   "fun_upd f a b == % x. if x=a then b else f x"
     5.8 +  [code func]: "fun_upd f a b == % x. if x=a then b else f x"
     5.9  
    5.10  nonterminals
    5.11    updbinds updbind
    5.12 @@ -34,15 +34,20 @@
    5.13   "fun_sum" == sum_case
    5.14  *)
    5.15  
    5.16 -constdefs
    5.17 -  override_on :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
    5.18 -  "override_on f g A == %a. if a : A then g a else f a"
    5.19 +definition
    5.20 +  override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
    5.21 +where
    5.22 +  "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
    5.23  
    5.24 -  id :: "'a => 'a"
    5.25 -  "id == %x. x"
    5.26 +definition
    5.27 +  id :: "'a \<Rightarrow> 'a"
    5.28 +where
    5.29 +  "id = (\<lambda>x. x)"
    5.30  
    5.31 -  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    5.32 -  "f o g == %x. f(g(x))"
    5.33 +definition
    5.34 +  comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
    5.35 +where
    5.36 +  "f o g = (\<lambda>x. f (g x))"
    5.37  
    5.38  notation (xsymbols)
    5.39    comp  (infixl "\<circ>" 55)
    5.40 @@ -404,9 +409,10 @@
    5.41  
    5.42  subsection{* swap *}
    5.43  
    5.44 -constdefs
    5.45 -  swap :: "['a, 'a, 'a => 'b] => ('a => 'b)"
    5.46 -   "swap a b f == f(a := f b, b:= f a)"
    5.47 +definition
    5.48 +  swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
    5.49 +where
    5.50 +  "swap a b f = f (a := f b, b:= f a)"
    5.51  
    5.52  lemma swap_self: "swap a a f = f"
    5.53  by (simp add: swap_def)
    5.54 @@ -418,7 +424,7 @@
    5.55  by (rule ext, simp add: fun_upd_def swap_def)
    5.56  
    5.57  lemma inj_on_imp_inj_on_swap:
    5.58 -     "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
    5.59 +  "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
    5.60  by (simp add: inj_on_def swap_def, blast)
    5.61  
    5.62  lemma inj_on_swap_iff [simp]:
    5.63 @@ -460,6 +466,8 @@
    5.64    le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
    5.65    less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
    5.66  
    5.67 +lemmas [code nofunc] = le_fun_def less_fun_def
    5.68 +
    5.69  instance "fun" :: (type, preorder) preorder
    5.70    by default (auto simp add: le_fun_def less_fun_def intro: order_trans)
    5.71  
    5.72 @@ -528,6 +536,8 @@
    5.73  apply (auto dest: le_funD)
    5.74  done
    5.75  
    5.76 +lemmas [code nofunc] = inf_fun_eq sup_fun_eq
    5.77 +
    5.78  instance "fun" :: (type, distrib_lattice) distrib_lattice
    5.79    by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
    5.80  
     6.1 --- a/src/HOL/HOL.thy	Fri Apr 20 11:21:41 2007 +0200
     6.2 +++ b/src/HOL/HOL.thy	Fri Apr 20 11:21:42 2007 +0200
     6.3 @@ -165,7 +165,7 @@
     6.4    True_or_False:  "(P=True) | (P=False)"
     6.5  
     6.6  defs
     6.7 -  Let_def:      "Let s f == f(s)"
     6.8 +  Let_def [code func]: "Let s f == f(s)"
     6.9    if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
    6.10  
    6.11  finalconsts
    6.12 @@ -177,7 +177,7 @@
    6.13  axiomatization
    6.14    undefined :: 'a
    6.15  
    6.16 -axioms
    6.17 +axiomatization where
    6.18    undefined_fun: "undefined x = undefined"
    6.19  
    6.20  
    6.21 @@ -912,8 +912,8 @@
    6.22  structure Blast = BlastFun(
    6.23  struct
    6.24    type claset = Classical.claset
    6.25 -  val equality_name = "op ="
    6.26 -  val not_name = "Not"
    6.27 +  val equality_name = @{const_name "op ="}
    6.28 +  val not_name = @{const_name "Not"}
    6.29    val notE = @{thm HOL.notE}
    6.30    val ccontr = @{thm HOL.ccontr}
    6.31    val contr_tac = Classical.contr_tac
     7.1 --- a/src/HOL/Integ/IntDef.thy	Fri Apr 20 11:21:41 2007 +0200
     7.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Apr 20 11:21:42 2007 +0200
     7.3 @@ -517,15 +517,16 @@
     7.4  
     7.5  subsection{*The Constants @{term neg} and @{term iszero}*}
     7.6  
     7.7 -constdefs
     7.8 -
     7.9 -  neg   :: "'a::ordered_idom => bool"
    7.10 -  "neg(Z) == Z < 0"
    7.11 +definition
    7.12 +  neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
    7.13 +where
    7.14 +  "neg Z \<longleftrightarrow> Z < 0"
    7.15  
    7.16 +definition
    7.17    (*For simplifying equalities*)
    7.18 -  iszero :: "'a::comm_semiring_1_cancel => bool"
    7.19 -  "iszero z == z = (0)"
    7.20 -
    7.21 +  iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
    7.22 +where
    7.23 +  "iszero z \<longleftrightarrow> z = 0"
    7.24  
    7.25  lemma not_neg_int [simp]: "~ neg(int n)"
    7.26  by (simp add: neg_def)
     8.1 --- a/src/HOL/Integ/IntDiv.thy	Fri Apr 20 11:21:41 2007 +0200
     8.2 +++ b/src/HOL/Integ/IntDiv.thy	Fri Apr 20 11:21:42 2007 +0200
     8.3 @@ -18,13 +18,13 @@
     8.4  constdefs
     8.5    quorem :: "(int*int) * (int*int) => bool"
     8.6      --{*definition of quotient and remainder*}
     8.7 -    "quorem == %((a,b), (q,r)).
     8.8 +    [code func]: "quorem == %((a,b), (q,r)).
     8.9                        a = b*q + r &
    8.10                        (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
    8.11  
    8.12    adjust :: "[int, int*int] => int*int"
    8.13      --{*for the division algorithm*}
    8.14 -    "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
    8.15 +    [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
    8.16                           else (2*q, r)"
    8.17  
    8.18  text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
    8.19 @@ -44,13 +44,13 @@
    8.20  text{*algorithm for the general case @{term "b\<noteq>0"}*}
    8.21  constdefs
    8.22    negateSnd :: "int*int => int*int"
    8.23 -    "negateSnd == %(q,r). (q,-r)"
    8.24 +    [code func]: "negateSnd == %(q,r). (q,-r)"
    8.25  
    8.26    divAlg :: "int*int => int*int"
    8.27      --{*The full division algorithm considers all possible signs for a, b
    8.28         including the special case @{text "a=0, b<0"} because 
    8.29         @{term negDivAlg} requires @{term "a<0"}.*}
    8.30 -    "divAlg ==
    8.31 +    [code func]: "divAlg ==
    8.32         %(a,b). if 0\<le>a then
    8.33                    if 0\<le>b then posDivAlg (a,b)
    8.34                    else if a=0 then (0,0)
    8.35 @@ -65,8 +65,8 @@
    8.36  text{*The operators are defined with reference to the algorithm, which is
    8.37  proved to satisfy the specification.*}
    8.38  defs
    8.39 -  div_def:   "a div b == fst (divAlg (a,b))"
    8.40 -  mod_def:   "a mod b == snd (divAlg (a,b))"
    8.41 +  div_def [code func]: "a div b == fst (divAlg (a,b))"
    8.42 +  mod_def [code func]: "a mod b == snd (divAlg (a,b))"
    8.43  
    8.44  
    8.45  text{*
     9.1 --- a/src/HOL/Integ/Numeral.thy	Fri Apr 20 11:21:41 2007 +0200
     9.2 +++ b/src/HOL/Integ/Numeral.thy	Fri Apr 20 11:21:42 2007 +0200
     9.3 @@ -32,15 +32,15 @@
     9.4  
     9.5  definition
     9.6    Pls :: int where
     9.7 -  "Pls = 0"
     9.8 +  [code nofunc]:"Pls = 0"
     9.9  
    9.10  definition
    9.11    Min :: int where
    9.12 -  "Min = - 1"
    9.13 +  [code nofunc]:"Min = - 1"
    9.14  
    9.15  definition
    9.16    Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
    9.17 -  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
    9.18 +  [code nofunc]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
    9.19  
    9.20  class number = type + -- {* for numeric types: nat, int, real, \dots *}
    9.21    fixes number_of :: "int \<Rightarrow> 'a"
    9.22 @@ -68,11 +68,11 @@
    9.23  
    9.24  definition
    9.25    succ :: "int \<Rightarrow> int" where
    9.26 -  "succ k = k + 1"
    9.27 +  [code nofunc]: "succ k = k + 1"
    9.28  
    9.29  definition
    9.30    pred :: "int \<Rightarrow> int" where
    9.31 -  "pred k = k - 1"
    9.32 +  [code nofunc]: "pred k = k - 1"
    9.33  
    9.34  declare
    9.35   max_def[of "number_of u" "number_of v", standard, simp]
    10.1 --- a/src/HOL/Integ/Presburger.thy	Fri Apr 20 11:21:41 2007 +0200
    10.2 +++ b/src/HOL/Integ/Presburger.thy	Fri Apr 20 11:21:42 2007 +0200
    10.3 @@ -1069,11 +1069,12 @@
    10.4  lemma eq_number_of [code func]:
    10.5    "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    10.6    unfolding number_of_is_id ..
    10.7 +
    10.8  lemma eq_Pls_Pls:
    10.9 -  "Numeral.Pls = Numeral.Pls" ..
   10.10 +  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
   10.11  
   10.12  lemma eq_Pls_Min:
   10.13 -  "Numeral.Pls \<noteq> Numeral.Min"
   10.14 +  "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   10.15    unfolding Pls_def Min_def by auto
   10.16  
   10.17  lemma eq_Pls_Bit0:
   10.18 @@ -1081,18 +1082,18 @@
   10.19    unfolding Pls_def Bit_def bit.cases by auto
   10.20  
   10.21  lemma eq_Pls_Bit1:
   10.22 -  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
   10.23 +  "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   10.24    unfolding Pls_def Bit_def bit.cases by arith
   10.25  
   10.26  lemma eq_Min_Pls:
   10.27 -  "Numeral.Min \<noteq> Numeral.Pls"
   10.28 +  "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   10.29    unfolding Pls_def Min_def by auto
   10.30  
   10.31  lemma eq_Min_Min:
   10.32 -  "Numeral.Min = Numeral.Min" ..
   10.33 +  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
   10.34  
   10.35  lemma eq_Min_Bit0:
   10.36 -  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
   10.37 +  "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   10.38    unfolding Min_def Bit_def bit.cases by arith
   10.39  
   10.40  lemma eq_Min_Bit1:
   10.41 @@ -1104,11 +1105,11 @@
   10.42    unfolding Pls_def Bit_def bit.cases by auto
   10.43  
   10.44  lemma eq_Bit1_Pls:
   10.45 -  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
   10.46 +  "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   10.47    unfolding Pls_def Bit_def bit.cases by arith
   10.48  
   10.49  lemma eq_Bit0_Min:
   10.50 -  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
   10.51 +  "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   10.52    unfolding Min_def Bit_def bit.cases by arith
   10.53  
   10.54  lemma eq_Bit1_Min:
   10.55 @@ -1140,10 +1141,10 @@
   10.56    unfolding number_of_is_id ..
   10.57  
   10.58  lemma less_eq_Pls_Pls:
   10.59 -  "Numeral.Pls \<le> Numeral.Pls" ..
   10.60 +  "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   10.61  
   10.62  lemma less_eq_Pls_Min:
   10.63 -  "\<not> (Numeral.Pls \<le> Numeral.Min)"
   10.64 +  "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   10.65    unfolding Pls_def Min_def by auto
   10.66  
   10.67  lemma less_eq_Pls_Bit:
   10.68 @@ -1151,11 +1152,11 @@
   10.69    unfolding Pls_def Bit_def by (cases v) auto
   10.70  
   10.71  lemma less_eq_Min_Pls:
   10.72 -  "Numeral.Min \<le> Numeral.Pls"
   10.73 +  "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   10.74    unfolding Pls_def Min_def by auto
   10.75  
   10.76  lemma less_eq_Min_Min:
   10.77 -  "Numeral.Min \<le> Numeral.Min" ..
   10.78 +  "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   10.79  
   10.80  lemma less_eq_Min_Bit0:
   10.81    "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   10.82 @@ -1198,10 +1199,10 @@
   10.83    unfolding number_of_is_id ..
   10.84  
   10.85  lemma less_Pls_Pls:
   10.86 -  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
   10.87 +  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
   10.88  
   10.89  lemma less_Pls_Min:
   10.90 -  "\<not> (Numeral.Pls < Numeral.Min)"
   10.91 +  "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   10.92    unfolding Pls_def Min_def by auto
   10.93  
   10.94  lemma less_Pls_Bit0:
   10.95 @@ -1213,11 +1214,11 @@
   10.96    unfolding Pls_def Bit_def by auto
   10.97  
   10.98  lemma less_Min_Pls:
   10.99 -  "Numeral.Min < Numeral.Pls"
  10.100 +  "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
  10.101    unfolding Pls_def Min_def by auto
  10.102  
  10.103  lemma less_Min_Min:
  10.104 -  "\<not> (Numeral.Min < Numeral.Min)" by auto
  10.105 +  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
  10.106  
  10.107  lemma less_Min_Bit:
  10.108    "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
    11.1 --- a/src/HOL/Library/ExecutableSet.thy	Fri Apr 20 11:21:41 2007 +0200
    11.2 +++ b/src/HOL/Library/ExecutableSet.thy	Fri Apr 20 11:21:42 2007 +0200
    11.3 @@ -287,6 +287,12 @@
    11.4    "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
    11.5  
    11.6  lemma [code func]:
    11.7 +  "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
    11.8 +
    11.9 +lemma [code func]:
   11.10 +  "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
   11.11 +
   11.12 +lemma [code func]:
   11.13    "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
   11.14  
   11.15  lemma [code func]:
   11.16 @@ -301,6 +307,7 @@
   11.17  lemma [code func]:
   11.18    "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
   11.19  
   11.20 +
   11.21  code_abstype "'a set" "'a list" where
   11.22    "{}" \<equiv> empty_list
   11.23    insert \<equiv> insertl
    12.1 --- a/src/HOL/Library/Graphs.thy	Fri Apr 20 11:21:41 2007 +0200
    12.2 +++ b/src/HOL/Library/Graphs.thy	Fri Apr 20 11:21:42 2007 +0200
    12.3 @@ -73,13 +73,14 @@
    12.4    by auto
    12.5  qed
    12.6  
    12.7 +lemmas [code nofunc] = graph_plus_def
    12.8  
    12.9  instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
   12.10    graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
   12.11    graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
   12.12    "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
   12.13    "sup G H \<equiv> G + H"
   12.14 -  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
   12.15 +  Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
   12.16  proof
   12.17    fix x y z :: "('a,'b) graph"
   12.18    fix A :: "('a, 'b) graph set"
   12.19 @@ -122,6 +123,9 @@
   12.20      unfolding Inf_graph_def graph_leq_def by auto }
   12.21  qed
   12.22  
   12.23 +lemmas [code nofunc] = graph_leq_def graph_less_def
   12.24 +  inf_graph_def sup_graph_def Inf_graph_def
   12.25 +
   12.26  lemma in_grplus:
   12.27    "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
   12.28    by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
   12.29 @@ -146,6 +150,8 @@
   12.30      by (cases a) (simp add:grcomp.simps)
   12.31  qed
   12.32  
   12.33 +lemmas [code nofunc] = graph_mult_def
   12.34 +
   12.35  instance graph :: (type, one) one 
   12.36    graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
   12.37  
    13.1 --- a/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:41 2007 +0200
    13.2 +++ b/src/HOL/Library/List_lexord.thy	Fri Apr 20 11:21:42 2007 +0200
    13.3 @@ -13,7 +13,7 @@
    13.4    list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
    13.5    list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
    13.6  
    13.7 -lemmas list_ord_defs = list_less_def list_le_def
    13.8 +lemmas list_ord_defs [code nofunc] = list_less_def list_le_def
    13.9  
   13.10  instance list :: (order) order
   13.11    apply (intro_classes, unfold list_ord_defs)
   13.12 @@ -40,6 +40,8 @@
   13.13    by intro_classes
   13.14      (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
   13.15  
   13.16 +lemmas [code nofunc] = inf_list_def sup_list_def
   13.17 +
   13.18  lemma not_less_Nil [simp]: "\<not> (x < [])"
   13.19    by (unfold list_less_def) simp
   13.20  
    14.1 --- a/src/HOL/Library/Product_ord.thy	Fri Apr 20 11:21:41 2007 +0200
    14.2 +++ b/src/HOL/Library/Product_ord.thy	Fri Apr 20 11:21:42 2007 +0200
    14.3 @@ -13,7 +13,7 @@
    14.4    prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
    14.5    prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
    14.6  
    14.7 -lemmas prod_ord_defs = prod_less_def prod_le_def
    14.8 +lemmas prod_ord_defs [code nofunc] = prod_less_def prod_le_def
    14.9  
   14.10  lemma [code func]:
   14.11    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    15.1 --- a/src/HOL/Library/SCT_Definition.thy	Fri Apr 20 11:21:41 2007 +0200
    15.2 +++ b/src/HOL/Library/SCT_Definition.thy	Fri Apr 20 11:21:42 2007 +0200
    15.3 @@ -15,12 +15,11 @@
    15.4      LESS ("\<down>")
    15.5    | LEQ ("\<Down>")
    15.6  
    15.7 -instance sedge :: times ..
    15.8 -instance sedge :: one ..
    15.9 +instance sedge :: one
   15.10 +  one_sedge_def: "1 \<equiv> \<Down>" ..
   15.11  
   15.12 -defs (overloaded)
   15.13 -  one_sedge_def: "1 == \<Down>"
   15.14 -  mult_sedge_def:" a * b == (if a = \<down> then \<down> else b)"
   15.15 +instance sedge :: times
   15.16 +  mult_sedge_def:" a * b \<equiv> if a = \<down> then \<down> else b" ..
   15.17  
   15.18  instance sedge :: comm_monoid_mult
   15.19  proof
   15.20 @@ -31,14 +30,18 @@
   15.21      by (cases a, simp) (cases b, auto)
   15.22  qed
   15.23  
   15.24 +lemma sedge_UNIV:
   15.25 +  "UNIV = { LESS, LEQ }"
   15.26 +  by auto (case_tac x, auto) (*FIXME*)
   15.27 +
   15.28  instance sedge :: finite
   15.29  proof
   15.30 -  have a: "UNIV = { LESS, LEQ }"
   15.31 -    by auto (case_tac x, auto) (* FIXME *)
   15.32    show "finite (UNIV::sedge set)"
   15.33 -    by (simp add:a)
   15.34 +    by (simp add: sedge_UNIV)
   15.35  qed
   15.36  
   15.37 +lemmas [code func] = sedge_UNIV
   15.38 +
   15.39  
   15.40  types scg = "(nat, sedge) graph"
   15.41  types acg = "(nat, scg) graph"
    16.1 --- a/src/HOL/Library/SCT_Implementation.thy	Fri Apr 20 11:21:41 2007 +0200
    16.2 +++ b/src/HOL/Library/SCT_Implementation.thy	Fri Apr 20 11:21:42 2007 +0200
    16.3 @@ -19,11 +19,10 @@
    16.4  where
    16.5    "connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
    16.6  
    16.7 -lemma grcomp_code[code]:
    16.8 +lemma grcomp_code [code]:
    16.9    "grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
   16.10    by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
   16.11  
   16.12 -
   16.13  definition test_SCT :: "acg \<Rightarrow> bool"
   16.14  where
   16.15    "test_SCT \<A> = 
   16.16 @@ -119,6 +118,6 @@
   16.17    Kleene_Algebras SCT
   16.18    SCT_Implementation SCT
   16.19  
   16.20 -code_gen test_SCT (SML -)
   16.21 +code_gen test_SCT (SML #)
   16.22  
   16.23  end
    17.1 --- a/src/HOL/Map.thy	Fri Apr 20 11:21:41 2007 +0200
    17.2 +++ b/src/HOL/Map.thy	Fri Apr 20 11:21:42 2007 +0200
    17.3 @@ -84,7 +84,7 @@
    17.4    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    17.5  
    17.6  defs
    17.7 -  map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    17.8 +  map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    17.9  
   17.10  
   17.11  subsection {* @{term [source] empty} *}
    18.1 --- a/src/HOL/Nat.thy	Fri Apr 20 11:21:41 2007 +0200
    18.2 +++ b/src/HOL/Nat.thy	Fri Apr 20 11:21:42 2007 +0200
    18.3 @@ -62,7 +62,9 @@
    18.4    Zero_nat_def: "0 == Abs_Nat Zero_Rep"
    18.5    One_nat_def [simp]: "1 == Suc 0"
    18.6    less_def: "m < n == (m, n) : pred_nat^+"
    18.7 -  le_def: "m \<le> (n::nat) == ~ (n < m)" ..
    18.8 +  le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
    18.9 +
   18.10 +lemmas [code nofunc] = less_def le_def
   18.11  
   18.12  text {* Induction *}
   18.13  
    19.1 --- a/src/HOL/Presburger.thy	Fri Apr 20 11:21:41 2007 +0200
    19.2 +++ b/src/HOL/Presburger.thy	Fri Apr 20 11:21:42 2007 +0200
    19.3 @@ -1069,11 +1069,12 @@
    19.4  lemma eq_number_of [code func]:
    19.5    "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    19.6    unfolding number_of_is_id ..
    19.7 +
    19.8  lemma eq_Pls_Pls:
    19.9 -  "Numeral.Pls = Numeral.Pls" ..
   19.10 +  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
   19.11  
   19.12  lemma eq_Pls_Min:
   19.13 -  "Numeral.Pls \<noteq> Numeral.Min"
   19.14 +  "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   19.15    unfolding Pls_def Min_def by auto
   19.16  
   19.17  lemma eq_Pls_Bit0:
   19.18 @@ -1081,18 +1082,18 @@
   19.19    unfolding Pls_def Bit_def bit.cases by auto
   19.20  
   19.21  lemma eq_Pls_Bit1:
   19.22 -  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
   19.23 +  "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   19.24    unfolding Pls_def Bit_def bit.cases by arith
   19.25  
   19.26  lemma eq_Min_Pls:
   19.27 -  "Numeral.Min \<noteq> Numeral.Pls"
   19.28 +  "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   19.29    unfolding Pls_def Min_def by auto
   19.30  
   19.31  lemma eq_Min_Min:
   19.32 -  "Numeral.Min = Numeral.Min" ..
   19.33 +  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
   19.34  
   19.35  lemma eq_Min_Bit0:
   19.36 -  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
   19.37 +  "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   19.38    unfolding Min_def Bit_def bit.cases by arith
   19.39  
   19.40  lemma eq_Min_Bit1:
   19.41 @@ -1104,11 +1105,11 @@
   19.42    unfolding Pls_def Bit_def bit.cases by auto
   19.43  
   19.44  lemma eq_Bit1_Pls:
   19.45 -  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
   19.46 +  "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   19.47    unfolding Pls_def Bit_def bit.cases by arith
   19.48  
   19.49  lemma eq_Bit0_Min:
   19.50 -  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
   19.51 +  "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   19.52    unfolding Min_def Bit_def bit.cases by arith
   19.53  
   19.54  lemma eq_Bit1_Min:
   19.55 @@ -1140,10 +1141,10 @@
   19.56    unfolding number_of_is_id ..
   19.57  
   19.58  lemma less_eq_Pls_Pls:
   19.59 -  "Numeral.Pls \<le> Numeral.Pls" ..
   19.60 +  "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   19.61  
   19.62  lemma less_eq_Pls_Min:
   19.63 -  "\<not> (Numeral.Pls \<le> Numeral.Min)"
   19.64 +  "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   19.65    unfolding Pls_def Min_def by auto
   19.66  
   19.67  lemma less_eq_Pls_Bit:
   19.68 @@ -1151,11 +1152,11 @@
   19.69    unfolding Pls_def Bit_def by (cases v) auto
   19.70  
   19.71  lemma less_eq_Min_Pls:
   19.72 -  "Numeral.Min \<le> Numeral.Pls"
   19.73 +  "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   19.74    unfolding Pls_def Min_def by auto
   19.75  
   19.76  lemma less_eq_Min_Min:
   19.77 -  "Numeral.Min \<le> Numeral.Min" ..
   19.78 +  "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   19.79  
   19.80  lemma less_eq_Min_Bit0:
   19.81    "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   19.82 @@ -1198,10 +1199,10 @@
   19.83    unfolding number_of_is_id ..
   19.84  
   19.85  lemma less_Pls_Pls:
   19.86 -  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
   19.87 +  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
   19.88  
   19.89  lemma less_Pls_Min:
   19.90 -  "\<not> (Numeral.Pls < Numeral.Min)"
   19.91 +  "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   19.92    unfolding Pls_def Min_def by auto
   19.93  
   19.94  lemma less_Pls_Bit0:
   19.95 @@ -1213,11 +1214,11 @@
   19.96    unfolding Pls_def Bit_def by auto
   19.97  
   19.98  lemma less_Min_Pls:
   19.99 -  "Numeral.Min < Numeral.Pls"
  19.100 +  "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
  19.101    unfolding Pls_def Min_def by auto
  19.102  
  19.103  lemma less_Min_Min:
  19.104 -  "\<not> (Numeral.Min < Numeral.Min)" by auto
  19.105 +  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
  19.106  
  19.107  lemma less_Min_Bit:
  19.108    "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
    20.1 --- a/src/HOL/Product_Type.thy	Fri Apr 20 11:21:41 2007 +0200
    20.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 20 11:21:42 2007 +0200
    20.3 @@ -104,10 +104,10 @@
    20.4    Pair_def:     "Pair a b == Abs_Prod (Pair_Rep a b)"
    20.5    fst_def:      "fst p == THE a. EX b. p = Pair a b"
    20.6    snd_def:      "snd p == THE b. EX a. p = Pair a b"
    20.7 -  split_def:    "split == (%c p. c (fst p) (snd p))"
    20.8 -  curry_def:    "curry == (%c x y. c (Pair x y))"
    20.9 -  prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
   20.10 -  Sigma_def:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
   20.11 +  split_def [code func]:    "split == (%c p. c (fst p) (snd p))"
   20.12 +  curry_def [code func]:    "curry == (%c x y. c (Pair x y))"
   20.13 +  prod_fun_def [code func]: "prod_fun f g == split (%x y. Pair (f x) (g y))"
   20.14 +  Sigma_def [code func]:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
   20.15  
   20.16  abbreviation
   20.17    Times :: "['a set, 'b set] => ('a * 'b) set"
   20.18 @@ -599,17 +599,22 @@
   20.19    done
   20.20  
   20.21  
   20.22 -constdefs
   20.23 -  upd_fst :: "('a => 'c) => 'a * 'b => 'c * 'b"
   20.24 - "upd_fst f == prod_fun f id"
   20.25 +definition
   20.26 +  upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
   20.27 +where
   20.28 +  "upd_fst f = prod_fun f id"
   20.29  
   20.30 -  upd_snd :: "('b => 'c) => 'a * 'b => 'a * 'c"
   20.31 - "upd_snd f == prod_fun id f"
   20.32 +definition
   20.33 +  upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
   20.34 +where
   20.35 +  "upd_snd f = prod_fun id f"
   20.36  
   20.37 -lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)" 
   20.38 +lemma upd_fst_conv [simp, code func]:
   20.39 +  "upd_fst f (x, y) = (f x, y)" 
   20.40    by (simp add: upd_fst_def)
   20.41  
   20.42 -lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)" 
   20.43 +lemma upd_snd_conv [simp, code func]:
   20.44 +  "upd_snd f (x, y) = (x, f y)" 
   20.45    by (simp add: upd_snd_def)
   20.46  
   20.47  text {*
    21.1 --- a/src/HOL/Record.thy	Fri Apr 20 11:21:41 2007 +0200
    21.2 +++ b/src/HOL/Record.thy	Fri Apr 20 11:21:42 2007 +0200
    21.3 @@ -17,11 +17,10 @@
    21.4  lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    21.5    by simp
    21.6  
    21.7 -constdefs K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
    21.8 -"K_record c x \<equiv> c"
    21.9 -
   21.10 -lemma K_record_apply [simp]: "K_record c x = c"
   21.11 -  by (simp add: K_record_def)
   21.12 +definition
   21.13 +  K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
   21.14 +where
   21.15 +  K_record_apply [simp]: "K_record c x = c"
   21.16  
   21.17  lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
   21.18    by (rule ext) (simp add: K_record_apply comp_def)
    22.1 --- a/src/HOL/Set.thy	Fri Apr 20 11:21:41 2007 +0200
    22.2 +++ b/src/HOL/Set.thy	Fri Apr 20 11:21:42 2007 +0200
    22.3 @@ -145,8 +145,10 @@
    22.4    subscripts in Proof General. *}
    22.5  
    22.6  instance set :: (type) ord
    22.7 -  subset_def:   "A <= B         == \<forall>x\<in>A. x \<in> B"
    22.8 -  psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B" ..
    22.9 +  subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
   22.10 +  psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
   22.11 +
   22.12 +lemmas [code nofunc] = subset_def psubset_def
   22.13  
   22.14  abbreviation
   22.15    subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   22.16 @@ -344,6 +346,8 @@
   22.17    Compl_def:    "- A            == {x. ~x:A}"
   22.18    set_diff_def: "A - B          == {x. x:A & ~x:B}" ..
   22.19  
   22.20 +lemmas [code nofunc] = Compl_def set_diff_def
   22.21 +
   22.22  defs
   22.23    Un_def:       "A Un B         == {x. x:A | x:B}"
   22.24    Int_def:      "A Int B        == {x. x:A & x:B}"
   22.25 @@ -2126,6 +2130,8 @@
   22.26    sup_set_eq: "sup A B \<equiv> A \<union> B"
   22.27    by intro_classes (auto simp add: inf_set_eq sup_set_eq)
   22.28  
   22.29 +lemmas [code nofunc] = inf_set_eq sup_set_eq
   22.30 +
   22.31  
   22.32  subsection {* Basic ML bindings *}
   22.33  
    23.1 --- a/src/Pure/Isar/ROOT.ML	Fri Apr 20 11:21:41 2007 +0200
    23.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Apr 20 11:21:42 2007 +0200
    23.3 @@ -11,6 +11,7 @@
    23.4  use "auto_bind.ML";
    23.5  use "local_syntax.ML";
    23.6  use "proof_context.ML";
    23.7 +use "../axclass.ML";
    23.8  use "local_defs.ML";
    23.9  
   23.10  (*outer syntax*)
   23.11 @@ -41,13 +42,17 @@
   23.12  use "net_rules.ML";
   23.13  use "induct_attrib.ML";
   23.14  
   23.15 +(*code generator base*)
   23.16 +use "../Tools/codegen_consts.ML";
   23.17 +use "../Tools/codegen_func.ML";
   23.18 +use "../Tools/codegen_data.ML";
   23.19 +
   23.20  (*derived theory and proof elements*)
   23.21  use "local_theory.ML";
   23.22  use "calculation.ML";
   23.23  use "obtain.ML";
   23.24  use "locale.ML";
   23.25  use "spec_parse.ML";
   23.26 -use "../axclass.ML";
   23.27  use "../Tools/class_package.ML";
   23.28  use "theory_target.ML";
   23.29  use "specification.ML";
    24.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 20 11:21:41 2007 +0200
    24.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 20 11:21:42 2007 +0200
    24.3 @@ -89,7 +89,7 @@
    24.4      (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    24.5          P.!!! (P.list1 P.xname)) []
    24.6          -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    24.7 -      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
    24.8 +      >> (fn (x, y) => Toplevel.theory (snd o ClassPackage.axclass_cmd x y)));
    24.9  
   24.10  
   24.11  (* types *)
   24.12 @@ -432,11 +432,6 @@
   24.13             >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
   24.14      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   24.15  
   24.16 -val print_classesP =
   24.17 -  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
   24.18 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
   24.19 -      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
   24.20 -
   24.21  end;
   24.22  
   24.23  
   24.24 @@ -710,6 +705,16 @@
   24.25  
   24.26  
   24.27  
   24.28 +(** code generation **)
   24.29 +
   24.30 +val code_datatypeP =
   24.31 +  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl (
   24.32 +    Scan.repeat1 P.term
   24.33 +    >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd)
   24.34 +  );
   24.35 +
   24.36 +
   24.37 +
   24.38  (** diagnostic commands (for interactive mode only) **)
   24.39  
   24.40  val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   24.41 @@ -752,6 +757,11 @@
   24.42    OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
   24.43      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
   24.44  
   24.45 +val print_classesP =
   24.46 +  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
   24.47 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
   24.48 +      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
   24.49 +
   24.50  val print_localeP =
   24.51    OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
   24.52      (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
   24.53 @@ -860,6 +870,11 @@
   24.54    OuterSyntax.improper_command "typ" "read and print type" K.diag
   24.55      (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   24.56  
   24.57 +val print_codesetupP =
   24.58 +  OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
   24.59 +    (Scan.succeed
   24.60 +      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
   24.61 +        (CodegenData.print_codesetup o Toplevel.theory_of)));
   24.62  
   24.63  
   24.64  (** system commands (for interactive mode only) **)
   24.65 @@ -994,6 +1009,8 @@
   24.66    apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   24.67    cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   24.68    interpretP,
   24.69 +  (*code generation*)
   24.70 +  code_datatypeP,
   24.71    (*diagnostic commands*)
   24.72    pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
   24.73    print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
   24.74 @@ -1003,7 +1020,7 @@
   24.75    print_methodsP, print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
   24.76    find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   24.77    print_thmsP, print_prfsP, print_full_prfsP, print_propP,
   24.78 -  print_termP, print_typeP,
   24.79 +  print_termP, print_typeP, print_codesetupP,
   24.80    (*system commands*)
   24.81    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   24.82    touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
    25.1 --- a/src/Pure/Isar/specification.ML	Fri Apr 20 11:21:41 2007 +0200
    25.2 +++ b/src/Pure/Isar/specification.ML	Fri Apr 20 11:21:42 2007 +0200
    25.3 @@ -130,7 +130,8 @@
    25.4  (*    |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
    25.5        |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
    25.6      val ((b, [th']), lthy3) = lthy2
    25.7 -      |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]);
    25.8 +      |> LocalTheory.note Thm.definitionK
    25.9 +          ((name, CodegenData.add_func_attr false :: atts), [prove lthy2 th]);
   25.10  
   25.11      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
   25.12      val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
    26.1 --- a/src/Pure/Tools/ROOT.ML	Fri Apr 20 11:21:41 2007 +0200
    26.2 +++ b/src/Pure/Tools/ROOT.ML	Fri Apr 20 11:21:42 2007 +0200
    26.3 @@ -15,9 +15,6 @@
    26.4  use "../codegen.ML";
    26.5  
    26.6  (*code generator, 2nd generation*)
    26.7 -use "codegen_consts.ML";
    26.8 -use "codegen_func.ML";
    26.9 -use "codegen_data.ML";
   26.10  use "codegen_names.ML";
   26.11  use "codegen_funcgr.ML";
   26.12  use "codegen_thingol.ML";
    27.1 --- a/src/Pure/Tools/codegen_data.ML	Fri Apr 20 11:21:41 2007 +0200
    27.2 +++ b/src/Pure/Tools/codegen_data.ML	Fri Apr 20 11:21:42 2007 +0200
    27.3 @@ -14,6 +14,7 @@
    27.4    val add_func: bool -> thm -> theory -> theory
    27.5    val del_func: thm -> theory -> theory
    27.6    val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
    27.7 +  val add_func_attr: bool -> Attrib.src
    27.8    val add_inline: thm -> theory -> theory
    27.9    val del_inline: thm -> theory -> theory
   27.10    val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
   27.11 @@ -23,6 +24,7 @@
   27.12    val add_datatype: string * ((string * sort) list * (string * typ list) list)
   27.13      -> theory -> theory
   27.14    val add_datatype_consts: CodegenConsts.const list -> theory -> theory
   27.15 +  val add_datatype_consts_cmd: string list -> theory -> theory
   27.16  
   27.17    val coregular_algebra: theory -> Sorts.algebra
   27.18    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
   27.19 @@ -33,6 +35,8 @@
   27.20  
   27.21    val preprocess_cterm: cterm -> thm
   27.22  
   27.23 +  val print_codesetup: theory -> unit
   27.24 +
   27.25    val trace: bool ref
   27.26  end;
   27.27  
   27.28 @@ -91,7 +95,7 @@
   27.29    then (false, xs)
   27.30    else (true, AList.merge eq_key eq xys);
   27.31  
   27.32 -val merge_thms = merge' Thm.eq_thm;
   27.33 +val merge_thms = merge' Thm.eq_thm_prop;
   27.34  
   27.35  fun merge_lthms (r1, r2) =
   27.36    if Susp.same (r1, r2)
   27.37 @@ -122,7 +126,7 @@
   27.38      fun drop thm' = not (matches args (args_of thm'))
   27.39        orelse (warning ("Dropping redundant defining equation\n" ^ string_of_thm thm'); false);
   27.40      val (keeps, drops) = List.partition drop sels;
   27.41 -  in (thm :: keeps, dels |> fold (insert Thm.eq_thm) drops |> remove Thm.eq_thm thm) end;
   27.42 +  in (thm :: keeps, dels |> fold (insert Thm.eq_thm_prop) drops |> remove Thm.eq_thm_prop thm) end;
   27.43  
   27.44  fun add_thm thm (sels, dels) =
   27.45    apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
   27.46 @@ -135,7 +139,7 @@
   27.47        fold add_thm (Susp.force lthms) (sels, dels);
   27.48  
   27.49  fun del_thm thm (sels, dels) =
   27.50 -  (Susp.value (remove Thm.eq_thm thm (Susp.force sels)), thm :: dels);
   27.51 +  (Susp.value (remove Thm.eq_thm_prop thm (Susp.force sels)), thm :: dels);
   27.52  
   27.53  fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
   27.54  
   27.55 @@ -144,8 +148,8 @@
   27.56      val (dels_t, dels) = merge_thms (dels1, dels2);
   27.57    in if dels_t
   27.58      then let
   27.59 -      val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm dels1 (Susp.force sels2))
   27.60 -      val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm (Susp.force sels1) dels2)
   27.61 +      val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm_prop dels1 (Susp.force sels2))
   27.62 +      val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm_prop (Susp.force sels1) dels2)
   27.63      in (true, ((lazy_thms o K) sels, dels)) end
   27.64      else let
   27.65        val (sels_t, sels) = merge_lthms (sels1, sels2)
   27.66 @@ -377,6 +381,8 @@
   27.67      end;
   27.68  end);
   27.69  
   27.70 +val print_codesetup = CodeData.print;
   27.71 +
   27.72  fun init k = CodeData.map
   27.73    (fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
   27.74  
   27.75 @@ -402,16 +408,16 @@
   27.76  
   27.77  fun common_typ_funcs [] = []
   27.78    | common_typ_funcs [thm] = [thm]
   27.79 -  | common_typ_funcs thms =
   27.80 +  | common_typ_funcs (thms as thm :: _) =
   27.81        let
   27.82 -        val thy = Thm.theory_of_thm (hd thms)
   27.83 +        val thy = Thm.theory_of_thm thm;
   27.84          fun incr_thm thm max =
   27.85            let
   27.86              val thm' = incr_indexes max thm;
   27.87              val max' = Thm.maxidx_of thm' + 1;
   27.88            in (thm', max') end;
   27.89          val (thms', maxidx) = fold_map incr_thm thms 0;
   27.90 -        val (ty1::tys) = map CodegenFunc.typ_func thms';
   27.91 +        val ty1 :: tys = map (snd o CodegenFunc.head_func) thms';
   27.92          fun unify ty env = Sign.typ_unify thy (ty1, ty) env
   27.93            handle Type.TUNIFY =>
   27.94              error ("Type unificaton failed, while unifying defining equations\n"
   27.95 @@ -423,12 +429,12 @@
   27.96            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
   27.97        in map (Thm.instantiate (instT, [])) thms' end;
   27.98  
   27.99 -fun certify_const thy c c_thms =
  27.100 +fun certify_const thy const thms =
  27.101    let
  27.102 -    fun cert (c', thm) = if CodegenConsts.eq_const (c, c')
  27.103 +    fun cert thm = if CodegenConsts.eq_const (const, fst (CodegenFunc.head_func thm))
  27.104        then thm else error ("Wrong head of defining equation,\nexpected constant "
  27.105 -        ^ CodegenConsts.string_of_const thy c ^ "\n" ^ string_of_thm thm)
  27.106 -  in map cert c_thms end;
  27.107 +        ^ CodegenConsts.string_of_const thy const ^ "\n" ^ string_of_thm thm)
  27.108 +  in map cert thms end;
  27.109  
  27.110  
  27.111  
  27.112 @@ -459,7 +465,7 @@
  27.113        |> maps these
  27.114        |> map (Thm.transfer thy);
  27.115      val sorts = map (map (snd o dest_TVar) o snd o dest_Type o the_single
  27.116 -      o Sign.const_typargs thy o fst o CodegenFunc.dest_func) funcs;
  27.117 +      o Sign.const_typargs thy o (fn ((c, _), ty) => (c, ty)) o CodegenFunc.head_func) funcs;
  27.118    in sorts end;
  27.119  
  27.120  fun weakest_constraints thy (class, tyco) =
  27.121 @@ -512,51 +518,49 @@
  27.122  val classop_weakest_typ = gen_classop_typ weakest_constraints;
  27.123  val classop_strongest_typ = gen_classop_typ strongest_constraints;
  27.124  
  27.125 -fun gen_mk_func_typ strict thm =
  27.126 +fun assert_func_typ thm =
  27.127    let
  27.128      val thy = Thm.theory_of_thm thm;
  27.129 -    val raw_funcs = CodegenFunc.mk_func strict thm;
  27.130 -    val error_warning = if strict then error else warning #> K NONE;
  27.131      fun check_typ_classop class (const as (c, SOME tyco), thm) =
  27.132            let
  27.133 -            val ((_, ty), _) = CodegenFunc.dest_func thm;
  27.134 +            val (_, ty) = CodegenFunc.head_func thm;
  27.135              val ty_decl = classop_weakest_typ thy class (c, tyco);
  27.136              val ty_strongest = classop_strongest_typ thy class (c, tyco);
  27.137              fun constrain thm = 
  27.138                let
  27.139                  val max = Thm.maxidx_of thm + 1;
  27.140                  val ty_decl' = Logic.incr_tvar max ty_decl;
  27.141 -                val ((_, ty'), _) = CodegenFunc.dest_func thm;
  27.142 +                val (_, ty') = CodegenFunc.head_func thm;
  27.143                  val (env, _) = Sign.typ_unify thy (ty_decl', ty') (Vartab.empty, max);
  27.144                  val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
  27.145                    cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
  27.146                in Thm.instantiate (instT, []) thm end;
  27.147            in if Sign.typ_instance thy (ty_strongest, ty)
  27.148              then if Sign.typ_instance thy (ty, ty_decl)
  27.149 -            then SOME (const, thm)
  27.150 +            then thm
  27.151              else (warning ("Constraining type\n" ^ CodegenConsts.string_of_typ thy ty
  27.152                ^ "\nof defining equation\n"
  27.153                ^ string_of_thm thm
  27.154                ^ "\nto permitted most general type\n"
  27.155                ^ CodegenConsts.string_of_typ thy ty_decl);
  27.156 -              SOME (const, constrain thm))
  27.157 -            else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty
  27.158 +              constrain thm)
  27.159 +            else CodegenFunc.bad_thm ("Type\n" ^ CodegenConsts.string_of_typ thy ty
  27.160                ^ "\nof defining equation\n"
  27.161                ^ string_of_thm thm
  27.162                ^ "\nis incompatible with permitted least general type\n"
  27.163                ^ CodegenConsts.string_of_typ thy ty_strongest)
  27.164            end
  27.165        | check_typ_classop class ((c, NONE), thm) =
  27.166 -          error_warning ("Illegal type for class operation " ^ quote c
  27.167 +          CodegenFunc.bad_thm ("Illegal type for class operation " ^ quote c
  27.168             ^ "\nin defining equation\n"
  27.169             ^ string_of_thm thm);
  27.170      fun check_typ_fun (const as (c, _), thm) =
  27.171        let
  27.172 -        val ((_, ty), _) = CodegenFunc.dest_func thm;
  27.173 +        val (_, ty) = CodegenFunc.head_func thm;
  27.174          val ty_decl = Sign.the_const_type thy c;
  27.175        in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
  27.176 -        then SOME (const, thm)
  27.177 -        else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty
  27.178 +        then thm
  27.179 +        else CodegenFunc.bad_thm ("Type\n" ^ CodegenConsts.string_of_typ thy ty
  27.180             ^ "\nof defining equation\n"
  27.181             ^ string_of_thm thm
  27.182             ^ "\nis incompatible declared function type\n"
  27.183 @@ -566,23 +570,34 @@
  27.184        case AxClass.class_of_param thy c
  27.185         of SOME class => check_typ_classop class (const, thm)
  27.186          | NONE => check_typ_fun (const, thm);
  27.187 -    val funcs = map_filter check_typ raw_funcs;
  27.188 -  in funcs end;
  27.189 +  in check_typ (fst (CodegenFunc.head_func thm), thm) end;
  27.190 +
  27.191 +val mk_func = CodegenFunc.error_thm
  27.192 +  (assert_func_typ o CodegenFunc.mk_func);
  27.193 +val mk_func_liberal = CodegenFunc.warning_thm
  27.194 +  (assert_func_typ o CodegenFunc.mk_func);
  27.195  
  27.196  end;
  27.197  
  27.198 -
  27.199  (** interfaces **)
  27.200  
  27.201 -fun add_func strict thm thy =
  27.202 -  let
  27.203 -    val funcs = gen_mk_func_typ strict thm;
  27.204 -    val cs = map fst funcs;
  27.205 -  in
  27.206 -    map_exec_purge (SOME cs) (map_funcs 
  27.207 -     (fold (fn (c, thm) => Consttab.map_default
  27.208 -       (c, (Susp.value [], [])) (add_thm thm)) funcs)) thy
  27.209 -  end;
  27.210 +fun add_func true thm thy =
  27.211 +      let
  27.212 +        val func = mk_func thm;
  27.213 +        val (const, _) = CodegenFunc.head_func func;
  27.214 +      in map_exec_purge (SOME [const]) (map_funcs
  27.215 +        (Consttab.map_default
  27.216 +          (const, (Susp.value [], [])) (add_thm func))) thy
  27.217 +      end
  27.218 +  | add_func false thm thy =
  27.219 +      case mk_func_liberal thm
  27.220 +       of SOME func => let
  27.221 +              val (const, _) = CodegenFunc.head_func func
  27.222 +            in map_exec_purge (SOME [const]) (map_funcs
  27.223 +              (Consttab.map_default
  27.224 +                (const, (Susp.value [], [])) (add_thm func))) thy
  27.225 +            end
  27.226 +        | NONE => thy;
  27.227  
  27.228  fun delete_force msg key xs =
  27.229    if AList.defined (op =) xs key then AList.delete (op =) key xs
  27.230 @@ -590,23 +605,26 @@
  27.231  
  27.232  fun del_func thm thy =
  27.233    let
  27.234 -    val funcs = gen_mk_func_typ false thm;
  27.235 -    val cs = map fst funcs;
  27.236 -  in
  27.237 -    map_exec_purge (SOME cs) (map_funcs
  27.238 -     (fold (fn (c, thm) => Consttab.map_entry c
  27.239 -       (del_thm thm)) funcs)) thy
  27.240 +    val func = mk_func thm;
  27.241 +    val (const, _) = CodegenFunc.head_func func;
  27.242 +  in map_exec_purge (SOME [const]) (map_funcs
  27.243 +    (Consttab.map_entry
  27.244 +      const (del_thm func))) thy
  27.245    end;
  27.246  
  27.247  fun add_funcl (const, lthms) thy =
  27.248    let
  27.249 -    val lthms' = certificate thy (fn thy => certify_const thy const
  27.250 -      o maps (CodegenFunc.mk_func true)) lthms;
  27.251 +    val lthms' = certificate thy (fn thy => certify_const thy const) lthms;
  27.252 +      (*FIXME must check compatibility with sort algebra;
  27.253 +        alas, naive checking results in non-termination!*)
  27.254    in
  27.255      map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
  27.256        (add_lthms lthms'))) thy
  27.257    end;
  27.258  
  27.259 +fun add_func_attr strict = Attrib.internal (fn _ => Thm.declaration_attribute
  27.260 +  (fn thm => Context.mapping (add_func strict thm) I));
  27.261 +
  27.262  local
  27.263  
  27.264  fun del_datatype tyco thy =
  27.265 @@ -637,12 +655,12 @@
  27.266  
  27.267  fun add_inline thm thy =
  27.268    (map_exec_purge NONE o map_preproc o apfst o apfst)
  27.269 -    (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
  27.270 +    (insert Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
  27.271          (*fully applied in order to get right context for mk_rew!*)
  27.272  
  27.273  fun del_inline thm thy =
  27.274    (map_exec_purge NONE o map_preproc o apfst o apfst)
  27.275 -    (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
  27.276 +    (remove Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
  27.277          (*fully applied in order to get right context for mk_rew!*)
  27.278  
  27.279  fun add_inline_proc (name, f) =
  27.280 @@ -680,12 +698,9 @@
  27.281  fun apply_preproc thy f [] = []
  27.282    | apply_preproc thy f (thms as (thm :: _)) =
  27.283        let
  27.284 +        val (const, _) = CodegenFunc.head_func thm;
  27.285          val thms' = f thy thms;
  27.286 -        val thms'' as ((const, _) :: _) = map CodegenFunc.mk_head thms'
  27.287 -      in (certify_const thy const o map CodegenFunc.mk_head) thms' end;
  27.288 -
  27.289 -fun cmp_thms thy =
  27.290 -  make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (CodegenFunc.typ_func thm1, CodegenFunc.typ_func thm2)));
  27.291 +      in certify_const thy const thms' end;
  27.292  
  27.293  fun rhs_conv conv thm =
  27.294    let
  27.295 @@ -700,7 +715,6 @@
  27.296    |> map (CodegenFunc.rewrite_func ((#inlines o the_preproc o get_exec) thy))
  27.297    |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
  27.298  (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
  27.299 -  |> sort (cmp_thms thy)
  27.300    |> common_typ_funcs;
  27.301  
  27.302  fun preprocess_cterm ct =
  27.303 @@ -757,38 +771,14 @@
  27.304    |> these
  27.305    |> map (Thm.transfer thy);
  27.306  
  27.307 -fun find_def thy (const as (c, _)) =
  27.308 -  let
  27.309 -    val specs = Defs.specifications_of (Theory.defs_of thy) c;
  27.310 -    val ty = case try (default_typ_proto thy) const
  27.311 -     of NONE => NONE
  27.312 -      | SOME ty => ty;
  27.313 -    val tys = Sign.const_typargs thy (c, ty |> the_default (Sign.the_const_type thy c));
  27.314 -    fun get_def (_, { is_def, name, lhs, rhs, thyname }) =
  27.315 -      if is_def andalso forall (Sign.typ_instance thy) (tys ~~ lhs) then
  27.316 -        try (Thm.get_axiom_i thy) name
  27.317 -      else NONE
  27.318 -  in get_first get_def specs end;
  27.319 -
  27.320  in
  27.321  
  27.322  fun these_funcs thy const =
  27.323    let
  27.324 -    fun get_prim_def_funcs (const as (c, tys)) =
  27.325 -      case find_def thy const
  27.326 -       of SOME thm =>
  27.327 -            thm
  27.328 -            |> Thm.transfer thy
  27.329 -            |> gen_mk_func_typ false
  27.330 -            |> map (CodegenFunc.expand_eta ~1 o snd)
  27.331 -        | NONE => []
  27.332      fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
  27.333        o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
  27.334 -    val funcs = case get_funcs thy const
  27.335 -     of [] => get_prim_def_funcs const
  27.336 -    | funcs => funcs
  27.337    in
  27.338 -    funcs
  27.339 +    get_funcs thy const
  27.340      |> preprocess thy
  27.341      |> drop_refl thy
  27.342    end;
  27.343 @@ -796,61 +786,14 @@
  27.344  fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
  27.345   of SOME ty => ty
  27.346    | NONE => (case get_funcs thy const
  27.347 -     of thm :: _ => CodegenFunc.typ_func thm
  27.348 +     of thm :: _ => snd (CodegenFunc.head_func thm)
  27.349        | [] => Sign.the_const_type thy c);
  27.350  
  27.351  end; (*local*)
  27.352  
  27.353 -
  27.354 -(** code attributes **)
  27.355 -
  27.356 -local
  27.357 -  fun add_simple_attribute (name, f) =
  27.358 -    (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
  27.359 -      (fn th => Context.mapping (f th) I);
  27.360 -in
  27.361 -  val _ = map (Context.add_setup o add_simple_attribute) [
  27.362 -    ("func", add_func true),
  27.363 -    ("nofunc", del_func),
  27.364 -    ("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)),
  27.365 -    ("inline", add_inline),
  27.366 -    ("noinline", del_inline)
  27.367 -  ]
  27.368 -end; (*local*)
  27.369 -
  27.370 -
  27.371 -(** Isar setup **)
  27.372 -
  27.373 -local
  27.374 -
  27.375 -structure P = OuterParse
  27.376 -and K = OuterKeyword
  27.377 -
  27.378 -val print_codesetupK = "print_codesetup";
  27.379 -val code_datatypeK = "code_datatype";
  27.380 -
  27.381 -in
  27.382 -
  27.383 -val print_codesetupP =
  27.384 -  OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" K.diag
  27.385 -    (Scan.succeed
  27.386 -      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (CodeData.print o Toplevel.theory_of)));
  27.387 -
  27.388 -val code_datatypeP =
  27.389 -  OuterSyntax.command code_datatypeK "define set of code datatype constructors" K.thy_decl (
  27.390 -    Scan.repeat1 P.term
  27.391 -    >> (Toplevel.theory o add_datatype_consts_cmd)
  27.392 -  );
  27.393 -
  27.394 -
  27.395 -val _ = OuterSyntax.add_parsers [print_codesetupP, code_datatypeP];
  27.396 -
  27.397 -end; (*local*)
  27.398 -
  27.399  end; (*struct*)
  27.400  
  27.401  
  27.402 -
  27.403  (** type-safe interfaces for data depedent on executable content **)
  27.404  
  27.405  signature CODE_DATA_ARGS =