tuned
authorhaftmann
Fri Apr 20 11:21:35 2007 +0200 (2007-04-20)
changeset 22737d87ccbcc2702
parent 22736 4948e2bd67e5
child 22738 4899f06effc6
tuned
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Lattices.thy
src/HOL/Relation_Power.thy
src/HOL/ex/Records.thy
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_consts.ML
src/Pure/Tools/codegen_func.ML
src/Pure/Tools/codegen_funcgr.ML
src/Pure/Tools/codegen_package.ML
     1.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Fri Apr 20 11:21:34 2007 +0200
     1.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Fri Apr 20 11:21:35 2007 +0200
     1.3 @@ -5,7 +5,9 @@
     1.4  
     1.5  header {* The pigeonhole principle *}
     1.6  
     1.7 -theory Pigeonhole imports EfficientNat begin
     1.8 +theory Pigeonhole
     1.9 +imports EfficientNat
    1.10 +begin
    1.11  
    1.12  text {*
    1.13  We formalize two proofs of the pigeonhole principle, which lead
     2.1 --- a/src/HOL/Lattices.thy	Fri Apr 20 11:21:34 2007 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Fri Apr 20 11:21:35 2007 +0200
     2.3 @@ -13,18 +13,20 @@
     2.4  
     2.5  text{*
     2.6    This theory of lattices only defines binary sup and inf
     2.7 -  operations. The extension to (finite) sets is done in theories @{text FixedPoint}
     2.8 -  and @{text Finite_Set}.
     2.9 +  operations. The extension to (finite) sets is done in theories
    2.10 +  @{text FixedPoint} and @{text Finite_Set}.
    2.11  *}
    2.12  
    2.13  class lower_semilattice = order +
    2.14    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    2.15 -  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    2.16 +  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    2.17 +  and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    2.18    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    2.19  
    2.20  class upper_semilattice = order +
    2.21    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    2.22 -  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    2.23 +  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    2.24 +  and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    2.25    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    2.26  
    2.27  class lattice = lower_semilattice + upper_semilattice
    2.28 @@ -251,28 +253,28 @@
    2.29  
    2.30  subsection {* Uniqueness of inf and sup *}
    2.31  
    2.32 -lemma inf_unique:
    2.33 +lemma (in lower_semilattice) inf_unique:
    2.34    fixes f (infixl "\<triangle>" 70)
    2.35 -  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
    2.36 -  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
    2.37 -  shows "inf x y = f x y"
    2.38 +  assumes le1: "\<And>x y. x \<triangle> y \<^loc>\<le> x" and le2: "\<And>x y. x \<triangle> y \<^loc>\<le> y"
    2.39 +  and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
    2.40 +  shows "x \<sqinter> y = x \<triangle> y"
    2.41  proof (rule antisym)
    2.42 -  show "x \<triangle> y \<le> inf x y" by (rule le_infI) (rule le1 le2)
    2.43 +  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1 le2)
    2.44  next
    2.45 -  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
    2.46 -  show "inf x y \<le> x \<triangle> y" by (rule leI) simp_all
    2.47 +  have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
    2.48 +  show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
    2.49  qed
    2.50  
    2.51 -lemma sup_unique:
    2.52 +lemma (in upper_semilattice) sup_unique:
    2.53    fixes f (infixl "\<nabla>" 70)
    2.54 -  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
    2.55 -  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
    2.56 -  shows "sup x y = f x y"
    2.57 +  assumes ge1 [simp]: "\<And>x y. x \<^loc>\<le> x \<nabla> y" and ge2: "\<And>x y. y \<^loc>\<le> x \<nabla> y"
    2.58 +  and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
    2.59 +  shows "x \<squnion> y = x \<nabla> y"
    2.60  proof (rule antisym)
    2.61 -  show "sup x y \<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
    2.62 +  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
    2.63  next
    2.64 -  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
    2.65 -  show "x \<nabla> y \<le> sup x y" by (rule leI) simp_all
    2.66 +  have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
    2.67 +  show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
    2.68  qed
    2.69    
    2.70  
     3.1 --- a/src/HOL/Relation_Power.thy	Fri Apr 20 11:21:34 2007 +0200
     3.2 +++ b/src/HOL/Relation_Power.thy	Fri Apr 20 11:21:35 2007 +0200
     3.3 @@ -40,7 +40,8 @@
     3.4  *}
     3.5  
     3.6  definition
     3.7 -  funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
     3.8 +  funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
     3.9 +where
    3.10    funpow_def: "funpow n f = f ^ n"
    3.11  
    3.12  lemmas [code inline] = funpow_def [symmetric]
     4.1 --- a/src/HOL/ex/Records.thy	Fri Apr 20 11:21:34 2007 +0200
     4.2 +++ b/src/HOL/ex/Records.thy	Fri Apr 20 11:21:35 2007 +0200
     4.3 @@ -35,17 +35,21 @@
     4.4    'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
     4.5  *}
     4.6  
     4.7 -consts foo1 :: point
     4.8  consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
     4.9 -consts foo3 :: "'a => 'a point_scheme"
    4.10  consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
    4.11  
    4.12  
    4.13  subsubsection {* Introducing concrete records and record schemes *}
    4.14  
    4.15 -defs
    4.16 -  foo1_def: "foo1 == (| xpos = 1, ypos = 0 |)"
    4.17 -  foo3_def: "foo3 ext == (| xpos = 1, ypos = 0, ... = ext |)"
    4.18 +definition
    4.19 +  foo1 :: point
    4.20 +where
    4.21 +  foo1_def: "foo1 = (| xpos = 1, ypos = 0 |)"
    4.22 +
    4.23 +definition
    4.24 +  foo3 :: "'a => 'a point_scheme"
    4.25 +where
    4.26 +  foo3_def: "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)"
    4.27  
    4.28  
    4.29  subsubsection {* Record selection and record update *}
     5.1 --- a/src/Pure/Tools/class_package.ML	Fri Apr 20 11:21:34 2007 +0200
     5.2 +++ b/src/Pure/Tools/class_package.ML	Fri Apr 20 11:21:35 2007 +0200
     5.3 @@ -9,6 +9,8 @@
     5.4  sig
     5.5    val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
     5.6  
     5.7 +  val axclass_cmd: bstring * xstring list
     5.8 +    -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
     5.9    val class: bstring -> class list -> Element.context_i Locale.element list
    5.10      -> string list -> theory -> string * Proof.context
    5.11    val class_cmd: bstring -> string list -> Element.context Locale.element list
    5.12 @@ -45,10 +47,21 @@
    5.13  fun fork_mixfix is_loc some_class mx =
    5.14    let
    5.15      val mx' = Syntax.unlocalize_mixfix mx;
    5.16 -    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') then NoSyn else mx';
    5.17 +    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx')
    5.18 +      then NoSyn else mx';
    5.19      val mx_local = if is_loc then mx else NoSyn;
    5.20    in (mx_global, mx_local) end;
    5.21  
    5.22 +fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    5.23 +  let
    5.24 +    val ctxt = ProofContext.init thy;
    5.25 +    val superclasses = map (Sign.read_class thy) raw_superclasses;
    5.26 +    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs;
    5.27 +    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    5.28 +      |> snd
    5.29 +      |> (map o map) fst;
    5.30 +  in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end;
    5.31 +
    5.32  
    5.33  (** AxClasses with implicit parameter handling **)
    5.34  
    5.35 @@ -95,7 +108,7 @@
    5.36      thy
    5.37      |> fold_map add_const consts
    5.38      |-> (fn cs => mk_axioms cs
    5.39 -    #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs @ other_consts) axioms_prop
    5.40 +    #-> (fn axioms_prop => AxClass.define_class (name, superclasses) (map fst cs @ other_consts) axioms_prop
    5.41      #-> (fn class => `(fn thy => AxClass.get_definition thy class)
    5.42      #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
    5.43      #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
    5.44 @@ -177,14 +190,15 @@
    5.45        thy
    5.46        |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs)
    5.47        |-> (fn thms => pair (map fst defs ~~ thms));
    5.48 -    fun after_qed cs thy =
    5.49 +    fun after_qed cs defs thy =
    5.50        thy
    5.51 -      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs);
    5.52 +      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
    5.53 +      |> fold (CodegenData.add_func false o snd) defs;
    5.54    in
    5.55      theory
    5.56      |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
    5.57      ||>> add_defs defs
    5.58 -    |-> (fn (cs, _) => do_proof (after_qed cs) arities)
    5.59 +    |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
    5.60    end;
    5.61  
    5.62  fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
    5.63 @@ -343,20 +357,6 @@
    5.64  
    5.65  (* tactics and methods *)
    5.66  
    5.67 -(*FIXME adjust these when minimal intro rules are at hand*)
    5.68 -fun intro_classes_tac' facts st =
    5.69 -  let
    5.70 -    val thy = Thm.theory_of_thm st;
    5.71 -    val ctxt = ProofContext.init thy;
    5.72 -    val intro_classes_tac = ALLGOALS
    5.73 -      (Method.insert_tac facts THEN' REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros thy)))
    5.74 -        THEN Tactic.distinct_subgoals_tac;
    5.75 -    val intro_locales_tac = SOMEGOAL (SELECT_GOAL (Locale.intro_locales_tac true ctxt facts))
    5.76 -      THEN Tactic.distinct_subgoals_tac;
    5.77 -  in
    5.78 -    (intro_classes_tac THEN REPEAT (intro_locales_tac ORELSE intro_locales_tac)) st
    5.79 -  end;
    5.80 -
    5.81  fun intro_classes_tac facts st =
    5.82    let
    5.83      val thy = Thm.theory_of_thm st;
    5.84 @@ -381,9 +381,7 @@
    5.85      default_intro_classes_tac facts;
    5.86  
    5.87  val _ = Context.add_setup (Method.add_methods
    5.88 - [("intro_classes2", Method.no_args (Method.METHOD intro_classes_tac'),
    5.89 -    "back-chain introduction rules of classes"),
    5.90 -  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    5.91 + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    5.92      "back-chain introduction rules of classes"),
    5.93    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
    5.94      "apply some intro/elim rule")]);
    5.95 @@ -481,6 +479,14 @@
    5.96  
    5.97  local
    5.98  
    5.99 +fun read_param thy raw_t =
   5.100 +  let
   5.101 +    val t = Sign.read_term thy raw_t
   5.102 +  in case try dest_Const t
   5.103 +   of SOME (c, _) => c
   5.104 +    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   5.105 +  end;
   5.106 +
   5.107  fun gen_class add_locale prep_class prep_param bname
   5.108      raw_supclasses raw_elems raw_other_consts thy =
   5.109    let
   5.110 @@ -573,7 +579,7 @@
   5.111  
   5.112  in
   5.113  
   5.114 -val class_cmd = gen_class Locale.add_locale Sign.intern_class AxClass.read_param;
   5.115 +val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;
   5.116  val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
   5.117  
   5.118  end; (*local*)
   5.119 @@ -643,7 +649,7 @@
   5.120        thy
   5.121        |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)]
   5.122        |>> the_single;
   5.123 -    val _ = warning "------ DEF ------";
   5.124 +    (*val _ = warning "------ DEF ------";
   5.125      val _ = warning c;
   5.126      val _ = warning name;
   5.127      val _ = (warning o Sign.string_of_term thy) rhs';
   5.128 @@ -658,14 +664,14 @@
   5.129      val _ = map print_witness witness;
   5.130      val _ = (warning o string_of_thm) eq';
   5.131      val eq'' = Element.satisfy_thm witness eq';
   5.132 -    val _ = (warning o string_of_thm) eq'';
   5.133 +    val _ = (warning o string_of_thm) eq'';*)
   5.134    in
   5.135      thy
   5.136 -    |> Sign.add_path prfx
   5.137 +    (* |> Sign.add_path prfx
   5.138      |> add_const (c, ty, syn')
   5.139      |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs')))
   5.140      |-> (fn global_def_thm => tap (fn _ => (warning o string_of_thm) global_def_thm))
   5.141 -    |> Sign.restore_naming thy
   5.142 +    |> Sign.restore_naming thy *)
   5.143    end;
   5.144  
   5.145  end;
     6.1 --- a/src/Pure/Tools/codegen_consts.ML	Fri Apr 20 11:21:34 2007 +0200
     6.2 +++ b/src/Pure/Tools/codegen_consts.ML	Fri Apr 20 11:21:35 2007 +0200
     6.3 @@ -16,6 +16,8 @@
     6.4    val string_of_typ: theory -> typ -> string
     6.5    val string_of_const: theory -> const -> string
     6.6    val read_const: theory -> string -> const
     6.7 +  val read_const_exprs: theory -> (const list -> const list)
     6.8 +    -> string list -> const list
     6.9  
    6.10    val co_of_const: theory -> const
    6.11      -> string * ((string * sort) list * (string * typ list))
    6.12 @@ -68,7 +70,7 @@
    6.13        ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);
    6.14  
    6.15  
    6.16 -(* reading constants as terms *)
    6.17 +(* reading constants as terms and wildcards pattern *)
    6.18  
    6.19  fun read_const thy raw_t =
    6.20    let
    6.21 @@ -78,6 +80,47 @@
    6.22      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    6.23    end;
    6.24  
    6.25 +local
    6.26 +
    6.27 +fun consts_of thy some_thyname =
    6.28 +  let
    6.29 +    val this_thy = Option.map theory some_thyname |> the_default thy;
    6.30 +    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    6.31 +      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
    6.32 +    fun classop c = case AxClass.class_of_param thy c
    6.33 +     of NONE => [(c, NONE)]
    6.34 +      | SOME class => Symtab.fold
    6.35 +          (fn (tyco, classes) => if AList.defined (op =) classes class
    6.36 +            then cons (c, SOME tyco) else I)
    6.37 +          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
    6.38 +          [(c, NONE)];
    6.39 +    val consts = maps classop cs;
    6.40 +    fun test_instance thy (class, tyco) =
    6.41 +      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
    6.42 +    fun belongs_here thyname (c, NONE) =
    6.43 +          not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
    6.44 +      | belongs_here thyname (c, SOME tyco) =
    6.45 +          let
    6.46 +            val SOME class = AxClass.class_of_param thy c
    6.47 +          in not (exists (fn thy' => test_instance thy' (class, tyco))
    6.48 +            (Theory.parents_of this_thy))
    6.49 +          end;
    6.50 +  in case some_thyname
    6.51 +   of NONE => consts
    6.52 +    | SOME thyname => filter (belongs_here thyname) consts
    6.53 +  end;
    6.54 +
    6.55 +fun read_const_expr thy "*" = ([], consts_of thy NONE)
    6.56 +  | read_const_expr thy s = if String.isSuffix ".*" s
    6.57 +      then ([], consts_of thy (SOME (unsuffix ".*" s)))
    6.58 +      else ([read_const thy s], []);
    6.59 +
    6.60 +in
    6.61 +
    6.62 +fun read_const_exprs thy select =
    6.63 +  (op @) o apsnd select o pairself flat o split_list o map (read_const_expr thy);
    6.64 +
    6.65 +end; (*local*)
    6.66  
    6.67  (* conversion between constants, constant expressions and datatype constructors *)
    6.68  
     7.1 --- a/src/Pure/Tools/codegen_func.ML	Fri Apr 20 11:21:34 2007 +0200
     7.2 +++ b/src/Pure/Tools/codegen_func.ML	Fri Apr 20 11:21:35 2007 +0200
     7.3 @@ -8,12 +8,12 @@
     7.4  signature CODEGEN_FUNC =
     7.5  sig
     7.6    val assert_rew: thm -> thm
     7.7 -  val mk_rew: thm -> thm list
     7.8 -  val assert_func: bool -> thm -> thm option
     7.9 -  val mk_func: bool -> thm -> (CodegenConsts.const * thm) list
    7.10 -  val mk_head: thm -> CodegenConsts.const * thm
    7.11 -  val dest_func: thm -> (string * typ) * term list
    7.12 -  val typ_func: thm -> typ
    7.13 +  val mk_rew: thm -> thm
    7.14 +  val mk_func: thm -> thm
    7.15 +  val head_func: thm -> CodegenConsts.const * typ
    7.16 +  val bad_thm: string -> 'a
    7.17 +  val error_thm: (thm -> thm) -> thm -> thm
    7.18 +  val warning_thm: (thm -> thm) -> thm -> thm option
    7.19  
    7.20    val inst_thm: sort Vartab.table -> thm -> thm
    7.21    val expand_eta: int -> thm -> thm
    7.22 @@ -25,10 +25,14 @@
    7.23  structure CodegenFunc : CODEGEN_FUNC =
    7.24  struct
    7.25  
    7.26 -fun lift_thm_thy f thm = f (Thm.theory_of_thm thm) thm;
    7.27 +
    7.28 +(* auxiliary *)
    7.29  
    7.30 -fun bad_thm msg thm =
    7.31 -  error (msg ^ ": " ^ string_of_thm thm);
    7.32 +exception BAD_THM of string;
    7.33 +fun bad_thm msg = raise BAD_THM msg;
    7.34 +fun error_thm f thm = f thm handle BAD_THM msg => error msg;
    7.35 +fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
    7.36 +  => (warning msg; NONE);
    7.37  
    7.38  
    7.39  (* making rewrite theorems *)
    7.40 @@ -36,85 +40,82 @@
    7.41  fun assert_rew thm =
    7.42    let
    7.43      val thy = Thm.theory_of_thm thm;
    7.44 -    val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm;
    7.45 +    val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm
    7.46 +      handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
    7.47      fun vars_of t = fold_aterms
    7.48       (fn Var (v, _) => insert (op =) v
    7.49 -       | Free _ => bad_thm "Illegal free variable in rewrite theorem" thm
    7.50 +       | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
    7.51 +           ^ Display.string_of_thm thm)
    7.52         | _ => I) t [];
    7.53      fun tvars_of t = fold_term_types
    7.54       (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
    7.55 -                          | TFree _ => bad_thm "Illegal free type variable in rewrite theorem" thm)) t [];
    7.56 +                          | TFree _ => bad_thm 
    7.57 +      ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
    7.58      val lhs_vs = vars_of lhs;
    7.59      val rhs_vs = vars_of rhs;
    7.60      val lhs_tvs = tvars_of lhs;
    7.61      val rhs_tvs = tvars_of lhs;
    7.62      val _ = if null (subtract (op =) lhs_vs rhs_vs)
    7.63        then ()
    7.64 -      else bad_thm "Free variables on right hand side of rewrite theorems" thm
    7.65 +      else bad_thm ("Free variables on right hand side of rewrite theorem\n"
    7.66 +        ^ Display.string_of_thm thm);
    7.67      val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
    7.68        then ()
    7.69 -      else bad_thm "Free type variables on right hand side of rewrite theorems" thm
    7.70 +      else bad_thm ("Free type variables on right hand side of rewrite theorem\n"
    7.71 +        ^ Display.string_of_thm thm)
    7.72    in thm end;
    7.73  
    7.74  fun mk_rew thm =
    7.75    let
    7.76      val thy = Thm.theory_of_thm thm;
    7.77 -    val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm;
    7.78 +    val ctxt = ProofContext.init thy;
    7.79    in
    7.80 -    map assert_rew thms
    7.81 +    thm
    7.82 +    |> LocalDefs.meta_rewrite_rule ctxt
    7.83 +    |> assert_rew
    7.84    end;
    7.85  
    7.86  
    7.87  (* making defining equations *)
    7.88  
    7.89 -val typ_func = lift_thm_thy (fn thy => snd o dest_Const o fst o strip_comb
    7.90 -  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
    7.91 -
    7.92 -val dest_func = lift_thm_thy (fn thy => apfst dest_Const o strip_comb
    7.93 -  o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Thm.plain_prop_of
    7.94 -  o Drule.fconv_rule Drule.beta_eta_conversion);
    7.95 -
    7.96 -val mk_head = lift_thm_thy (fn thy => fn thm =>
    7.97 -  ((CodegenConsts.const_of_cexpr thy o fst o dest_func) thm, thm));
    7.98 -
    7.99 -local
   7.100 -
   7.101 -exception BAD of string;
   7.102 -
   7.103 -fun handle_bad strict thm msg =
   7.104 -  if strict then error (msg ^ ": " ^ string_of_thm thm)
   7.105 -    else (warning (msg ^ ": " ^ string_of_thm thm); NONE);
   7.106 -
   7.107 -in
   7.108 +fun assert_func thm =
   7.109 +  let
   7.110 +    val thy = Thm.theory_of_thm thm;
   7.111 +    val args = (snd o strip_comb o fst o Logic.dest_equals
   7.112 +      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
   7.113 +    val _ =
   7.114 +      if has_duplicates (op =)
   7.115 +        ((fold o fold_aterms) (fn Var (v, _) => cons v
   7.116 +          | _ => I
   7.117 +        ) args [])
   7.118 +      then bad_thm ("Duplicated variables on left hand side of equation\n"
   7.119 +        ^ Display.string_of_thm thm)
   7.120 +      else ()
   7.121 +    fun check _ (Abs _) = bad_thm
   7.122 +          ("Abstraction on left hand side of equation\n"
   7.123 +            ^ Display.string_of_thm thm)
   7.124 +      | check 0 (Var _) = ()
   7.125 +      | check _ (Var _) = bad_thm
   7.126 +          ("Variable with application on left hand side of defining equation\n"
   7.127 +            ^ Display.string_of_thm thm)
   7.128 +      | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   7.129 +      | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
   7.130 +          then bad_thm
   7.131 +            ("Partially applied constant on left hand side of equation"
   7.132 +               ^ Display.string_of_thm thm)
   7.133 +          else ();
   7.134 +    val _ = map (check 0) args;
   7.135 +  in thm end;
   7.136  
   7.137 -fun assert_func strict thm = case try dest_func thm
   7.138 - of SOME (c_ty as (c, ty), args) => (
   7.139 -      let
   7.140 -        val thy = Thm.theory_of_thm thm;
   7.141 -        val _ =
   7.142 -          if has_duplicates (op =)
   7.143 -            ((fold o fold_aterms) (fn Var (v, _) => cons v
   7.144 -              | _ => I
   7.145 -            ) args [])
   7.146 -          then raise BAD "Repeated variables on left hand side of defining equation"
   7.147 -          else ()
   7.148 -        fun check _ (Abs _) = raise BAD
   7.149 -              "Abstraction on left hand side of defining equation"
   7.150 -          | check 0 (Var _) = ()
   7.151 -          | check _ (Var _) = raise BAD
   7.152 -              "Variable with application on left hand side of defining equation"
   7.153 -          | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   7.154 -          | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
   7.155 -              then raise BAD
   7.156 -                ("Partially applied constant on left hand side of defining equation")
   7.157 -              else ();
   7.158 -        val _ = map (check 0) args;
   7.159 -      in SOME thm end handle BAD msg => handle_bad strict thm msg)
   7.160 -  | NONE => handle_bad strict thm "Not a defining equation";
   7.161 +val mk_func = assert_func o Drule.fconv_rule Drule.beta_eta_conversion o mk_rew;
   7.162  
   7.163 -end;
   7.164 -
   7.165 -fun mk_func strict = map_filter (Option.map mk_head o assert_func strict) o mk_rew;
   7.166 +fun head_func thm =
   7.167 +  let
   7.168 +    val thy = Thm.theory_of_thm thm;
   7.169 +    val (Const (c_ty as (_, ty))) = (fst o strip_comb o fst o Logic.dest_equals
   7.170 +      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
   7.171 +    val const = CodegenConsts.const_of_cexpr thy c_ty;
   7.172 +  in (const, ty) end;
   7.173  
   7.174  
   7.175  (* utilities *)
     8.1 --- a/src/Pure/Tools/codegen_funcgr.ML	Fri Apr 20 11:21:34 2007 +0200
     8.2 +++ b/src/Pure/Tools/codegen_funcgr.ML	Fri Apr 20 11:21:35 2007 +0200
     8.3 @@ -157,9 +157,9 @@
     8.4      fun resort_rec tap_typ (const, []) = (true, (const, []))
     8.5        | resort_rec tap_typ (const, thms as thm :: _) =
     8.6            let
     8.7 -            val ty = CodegenFunc.typ_func thm;
     8.8 +            val (_, ty) = CodegenFunc.head_func thm;
     8.9              val thms' as thm' :: _ = resort_thms algebra tap_typ thms
    8.10 -            val ty' = CodegenFunc.typ_func thm';
    8.11 +            val (_, ty') = CodegenFunc.head_func thm';
    8.12            in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
    8.13      fun resort_recs funcss =
    8.14        let
    8.15 @@ -167,7 +167,7 @@
    8.16           of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const
    8.17                |> these
    8.18                |> try hd
    8.19 -              |> Option.map CodegenFunc.typ_func
    8.20 +              |> Option.map (snd o CodegenFunc.head_func)
    8.21            | NONE => NONE;
    8.22          val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss);
    8.23          val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
    8.24 @@ -241,10 +241,10 @@
    8.25        |> resort_funcss thy algebra funcgr
    8.26        |> filter_out (can (Constgraph.get_node funcgr) o fst);
    8.27      fun typ_func const [] = CodegenData.default_typ thy const
    8.28 -      | typ_func (_, NONE) (thm :: _) = CodegenFunc.typ_func thm
    8.29 +      | typ_func (_, NONE) (thm :: _) = (snd o CodegenFunc.head_func) thm
    8.30        | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
    8.31            let
    8.32 -            val ty = CodegenFunc.typ_func thm;
    8.33 +            val (_, ty) = CodegenFunc.head_func thm;
    8.34              val SOME class = AxClass.class_of_param thy c;
    8.35              val sorts_decl = Sorts.mg_domain algebra tyco [class];
    8.36              val tys = CodegenConsts.typargs thy (c, ty);
     9.1 --- a/src/Pure/Tools/codegen_package.ML	Fri Apr 20 11:21:34 2007 +0200
     9.2 +++ b/src/Pure/Tools/codegen_package.ML	Fri Apr 20 11:21:35 2007 +0200
     9.3 @@ -71,12 +71,22 @@
     9.4    fun rewrites thy = [];
     9.5  );
     9.6  
     9.7 -fun print_codethms thy =
     9.8 -  Pretty.writeln o CodegenFuncgr.pretty thy o Funcgr.make thy;
     9.9 +fun code_depgr thy [] = Funcgr.make thy []
    9.10 +  | code_depgr thy consts =
    9.11 +      let
    9.12 +        val gr = Funcgr.make thy consts;
    9.13 +        val select = CodegenFuncgr.Constgraph.all_succs gr consts;
    9.14 +      in
    9.15 +        CodegenFuncgr.Constgraph.subgraph
    9.16 +          (member CodegenConsts.eq_const select) gr
    9.17 +      end;
    9.18 +
    9.19 +fun code_thms thy =
    9.20 +  Pretty.writeln o CodegenFuncgr.pretty thy o code_depgr thy;
    9.21  
    9.22  fun code_deps thy consts =
    9.23    let
    9.24 -    val gr = Funcgr.make thy consts;
    9.25 +    val gr = code_depgr thy consts;
    9.26      fun mk_entry (const, (_, (_, parents))) =
    9.27        let
    9.28          val name = CodegenConsts.string_of_const thy const;
    9.29 @@ -113,7 +123,7 @@
    9.30  
    9.31  fun prep_eqs thy (thms as thm :: _) =
    9.32    let
    9.33 -    val ty = (Logic.unvarifyT o CodegenFunc.typ_func) thm;
    9.34 +    val ty = (Logic.unvarifyT o snd o CodegenFunc.head_func) thm;
    9.35      val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
    9.36        then thms
    9.37        else map (CodegenFunc.expand_eta 1) thms;
    9.38 @@ -600,34 +610,6 @@
    9.39  fun satisfies thy t witnesses = raw_eval_term thy
    9.40    (("CodegenPackage.satisfies_ref", satisfies_ref), t) witnesses;
    9.41  
    9.42 -
    9.43 -(* constant specifications with wildcards *)
    9.44 -
    9.45 -fun consts_of thy thyname =
    9.46 -  let
    9.47 -    val this_thy = Option.map theory thyname |> the_default thy;
    9.48 -    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    9.49 -      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
    9.50 -    fun classop c = case AxClass.class_of_param thy c
    9.51 -     of NONE => [(c, NONE)]
    9.52 -      | SOME class => Symtab.fold
    9.53 -          (fn (tyco, classes) => if AList.defined (op =) classes class
    9.54 -            then cons (c, SOME tyco) else I)
    9.55 -          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
    9.56 -          [(c, NONE)];
    9.57 -    val consts = maps classop cs;
    9.58 -    fun test_instance thy (class, tyco) =
    9.59 -      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
    9.60 -    fun belongs_here thyname (c, NONE) =
    9.61 -          not (exists (fn thy => Sign.declared_const thy c) (Theory.parents_of this_thy))
    9.62 -      | belongs_here thyname (c, SOME tyco) =
    9.63 -          not (exists (fn thy => test_instance thy ((the o AxClass.class_of_param thy) c, tyco))
    9.64 -            (Theory.parents_of this_thy))
    9.65 -  in case thyname
    9.66 -   of NONE => consts
    9.67 -    | SOME thyname => filter (belongs_here thyname) consts
    9.68 -  end;
    9.69 -
    9.70  fun filter_generatable thy targets consts =
    9.71    let
    9.72      val (consts', funcgr) = Funcgr.make_consts thy consts;
    9.73 @@ -636,11 +618,6 @@
    9.74        (consts' ~~ consts'');
    9.75    in consts''' end;
    9.76  
    9.77 -fun read_constspec thy targets "*" = filter_generatable thy targets (consts_of thy NONE)
    9.78 -  | read_constspec thy targets s = if String.isSuffix ".*" s
    9.79 -      then filter_generatable thy targets (consts_of thy (SOME (unsuffix ".*" s)))
    9.80 -      else [CodegenConsts.read_const thy s];
    9.81 -
    9.82  
    9.83  (** toplevel interface and setup **)
    9.84  
    9.85 @@ -655,7 +632,8 @@
    9.86            (target, SOME (CodegenSerializer.get_serializer thy target args CodegenNames.labelled_name))
    9.87        | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris;
    9.88      val targets = case map fst seris' of [] => NONE | xs => SOME xs;
    9.89 -    val cs = maps (read_constspec thy targets) raw_cs;
    9.90 +    val cs = CodegenConsts.read_const_exprs thy
    9.91 +      (filter_generatable thy targets) raw_cs;
    9.92      fun generate' thy = case cs
    9.93       of [] => []
    9.94        | _ =>
    9.95 @@ -671,11 +649,11 @@
    9.96      (map (serialize' cs code) (map_filter snd seris'); ())
    9.97    end;
    9.98  
    9.99 -fun print_codethms_cmd thy =
   9.100 -  print_codethms thy o map (CodegenConsts.read_const thy);
   9.101 +fun code_thms_cmd thy =
   9.102 +  code_thms thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
   9.103  
   9.104  fun code_deps_cmd thy =
   9.105 -  code_deps thy o map (CodegenConsts.read_const thy);
   9.106 +  code_deps thy o CodegenConsts.read_const_exprs thy (fst o Funcgr.make_consts thy);
   9.107  
   9.108  val code_exprP = (
   9.109      (Scan.repeat P.term
   9.110 @@ -713,13 +691,13 @@
   9.111    );
   9.112  
   9.113  val code_thmsP =
   9.114 -  OuterSyntax.improper_command code_thmsK "print cached defining equations" OuterKeyword.diag
   9.115 +  OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
   9.116      (Scan.repeat P.term
   9.117        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   9.118 -        o Toplevel.keep ((fn thy => print_codethms_cmd thy cs) o Toplevel.theory_of)));
   9.119 +        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
   9.120  
   9.121  val code_depsP =
   9.122 -  OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations" OuterKeyword.diag
   9.123 +  OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
   9.124      (Scan.repeat P.term
   9.125        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   9.126          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));