tuned
authorhaftmann
Wed Oct 24 07:19:52 2007 +0200 (2007-10-24)
changeset 25163f737a88a3248
parent 25162 ad4d5365d9d8
child 25164 0fcb4775cbfb
tuned
NEWS
src/Pure/Isar/class.ML
     1.1 --- a/NEWS	Tue Oct 23 23:27:23 2007 +0200
     1.2 +++ b/NEWS	Wed Oct 24 07:19:52 2007 +0200
     1.3 @@ -823,7 +823,7 @@
     1.4  package; constants add, mul, pow now curried.  Infix syntax for
     1.5  algebraic operations.
     1.6  
     1.7 -* Some steps towards more uniform lattice theory development in HOL.
     1.8 +* More uniform lattice theory development in HOL.
     1.9  
    1.10      constants "meet" and "join" now named "inf" and "sup"
    1.11      constant "Meet" now named "Inf"
    1.12 @@ -946,6 +946,9 @@
    1.13  * Classes "order" and "linorder": potential INCOMPATIBILITY due to
    1.14  changed order of proof goals instance proofs.
    1.15  
    1.16 +* Locale "partial_order" now unified with class "order" (cf. theory
    1.17 +Orderings), added parameter "less".  INCOMPATIBILITY.
    1.18 +
    1.19  * Dropped redundant lemma def_imp_eq in favor of meta_eq_to_obj_eq.
    1.20  INCOMPATIBILITY.
    1.21  
    1.22 @@ -977,10 +980,7 @@
    1.23  
    1.24  * Class "recpower" is generalized to arbitrary monoids, not just
    1.25  commutative semirings.  INCOMPATIBILITY: may need to incorporate
    1.26 -commutativity or a semiring properties additionally.
    1.27 -
    1.28 -* Unified locale "partial_order" with class definition (cf. theory
    1.29 -Orderings), added parameter "less".  INCOMPATIBILITY.
    1.30 +commutativity or semiring properties additionally.
    1.31  
    1.32  * Constant "List.list_all2" in List.thy now uses authentic syntax.
    1.33  INCOMPATIBILITY: translations containing list_all2 may go wrong,
    1.34 @@ -1005,11 +1005,12 @@
    1.35  
    1.36  See HOL/Integ/IntArith.thy for an example setup.
    1.37  
    1.38 -* New top level command 'normal_form' computes the normal form of a
    1.39 -term that may contain free variables.  For example ``normal_form
    1.40 -"rev[a,b,c]"'' produces ``[b,c,a]'' (without proof).  This command is
    1.41 -suitable for heavy-duty computations because the functions are
    1.42 -compiled to ML first.
    1.43 +* Command 'normal_form' computes the normal form of a
    1.44 +term that may contain free variables.  For example
    1.45 +``normal_form "rev [a, b, c]"'' produces ``[b, c, a]'' (without proof).
    1.46 +This command is suitable for heavy-duty computations because the functions
    1.47 +are compiled to ML first.  Correspondingly, a method ``normalization''
    1.48 +is provided.  See further HOL/ex/NormalForm.thy and Tools/nbe.ML.
    1.49  
    1.50  * Alternative iff syntax "A <-> B" for equality on bool (with priority
    1.51  25 like -->); output depends on the "iff" print_mode, the default is
     2.1 --- a/src/Pure/Isar/class.ML	Tue Oct 23 23:27:23 2007 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Wed Oct 24 07:19:52 2007 +0200
     2.3 @@ -433,16 +433,13 @@
     2.4  
     2.5  (* updaters *)
     2.6  
     2.7 -fun add_class_data ((class, superclasses), (cs, base_sort, insttab, phi, intro)) thy =
     2.8 +fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
     2.9    let
    2.10 -    val inst = map
    2.11 -      (SOME o the o Symtab.lookup insttab o fst o fst)
    2.12 -        (Locale.parameters_of_expr thy (Locale.Locale class));
    2.13      val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
    2.14        (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
    2.15      val cs = (map o pairself) fst cs;
    2.16      val add_class = Graph.new_node (class,
    2.17 -        mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
    2.18 +        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
    2.19        #> fold (curry Graph.add_edge class) superclasses;
    2.20    in
    2.21      ClassData.map add_class thy
    2.22 @@ -738,10 +735,8 @@
    2.23      val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
    2.24        prep_spec thy raw_supclasses raw_includes_elems;
    2.25      val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
    2.26 -    fun mk_inst class param_names cs =
    2.27 -      Symtab.empty
    2.28 -      |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
    2.29 -           (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
    2.30 +    fun mk_inst class cs =
    2.31 +      (map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs;
    2.32      fun fork_syntax (Element.Fixes xs) =
    2.33            fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
    2.34            #>> Element.Fixes
    2.35 @@ -785,7 +780,7 @@
    2.36        #-> (fn [(_, [class_intro])] =>
    2.37          add_class_data ((class, sups),
    2.38            (map fst params ~~ consts, base_sort,
    2.39 -            mk_inst class (map fst all_params) (map snd supconsts @ consts),
    2.40 +            mk_inst class (map snd supconsts @ consts),
    2.41                calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
    2.42        #> class_interpretation class axioms []
    2.43        )))))