proper merge of interpretation equations
authorhaftmann
Thu Oct 01 17:11:48 2009 +0200 (2009-10-01)
changeset 32850d95a7fd00bd4
parent 32806 06561afcadaa
child 32851 d6956d589f96
proper merge of interpretation equations
src/HOL/Relation.thy
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
     1.1 --- a/src/HOL/Relation.thy	Thu Oct 01 09:09:56 2009 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Oct 01 17:11:48 2009 +0200
     1.3 @@ -6,8 +6,7 @@
     1.4  header {* Relations *}
     1.5  
     1.6  theory Relation
     1.7 -imports Finite_Set Datatype
     1.8 -  (*FIXME order is important, otherwise merge problem for canonical interpretation of class monoid_mult wrt. power!*)
     1.9 +imports Datatype Finite_Set
    1.10  begin
    1.11  
    1.12  subsection {* Definitions *}
     2.1 --- a/src/Pure/Isar/class.ML	Thu Oct 01 09:09:56 2009 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 01 17:11:48 2009 +0200
     2.3 @@ -289,7 +289,7 @@
     2.4         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     2.5      #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
     2.6         Locale.add_registration_eqs (class, base_morph) eqs export_morph
     2.7 -    #> register class sups params base_sort base_morph axiom assm_intro of_class))
     2.8 +    #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     2.9      |> TheoryTarget.init (SOME class)
    2.10      |> pair class
    2.11    end;
     3.1 --- a/src/Pure/Isar/class_target.ML	Thu Oct 01 09:09:56 2009 +0200
     3.2 +++ b/src/Pure/Isar/class_target.ML	Thu Oct 01 17:11:48 2009 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  sig
     3.5    (*classes*)
     3.6    val register: class -> class list -> ((string * typ) * (string * typ)) list
     3.7 -    -> sort -> morphism -> thm option -> thm option -> thm
     3.8 +    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
     3.9      -> theory -> theory
    3.10  
    3.11    val is_class: theory -> class -> bool
    3.12 @@ -78,6 +78,7 @@
    3.13    base_sort: sort,
    3.14    base_morph: morphism
    3.15      (*static part of canonical morphism*),
    3.16 +  export_morph: morphism,
    3.17    assm_intro: thm option,
    3.18    of_class: thm,
    3.19    axiom: thm option,
    3.20 @@ -88,21 +89,21 @@
    3.21  
    3.22  };
    3.23  
    3.24 -fun make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    3.25 +fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    3.26      (defs, operations)) =
    3.27    ClassData { consts = consts, base_sort = base_sort,
    3.28 -    base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    3.29 -    defs = defs, operations = operations };
    3.30 -fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
    3.31 +    base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
    3.32 +    of_class = of_class, axiom = axiom, defs = defs, operations = operations };
    3.33 +fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
    3.34      of_class, axiom, defs, operations }) =
    3.35 -  make_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    3.36 +  make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    3.37      (defs, operations)));
    3.38  fun merge_class_data _ (ClassData { consts = consts,
    3.39 -    base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
    3.40 +    base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
    3.41      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    3.42 -  ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
    3.43 +  ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
    3.44      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    3.45 -  make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    3.46 +  make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    3.47      (Thm.merge_thms (defs1, defs2),
    3.48        AList.merge (op =) (K true) (operations1, operations2)));
    3.49  
    3.50 @@ -159,6 +160,7 @@
    3.51  val base_morphism = #base_morph oo the_class_data;
    3.52  fun morphism thy class = base_morphism thy class
    3.53    $> Element.eq_morphism thy (these_defs thy [class]);
    3.54 +val export_morphism = #export_morph oo the_class_data;
    3.55  
    3.56  fun print_classes thy =
    3.57    let
    3.58 @@ -196,22 +198,22 @@
    3.59  
    3.60  (* updaters *)
    3.61  
    3.62 -fun register class sups params base_sort morph
    3.63 +fun register class sups params base_sort base_morph export_morph
    3.64      axiom assm_intro of_class thy =
    3.65    let
    3.66      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    3.67        (c, (class, (ty, Free v_ty)))) params;
    3.68      val add_class = Graph.new_node (class,
    3.69          make_class_data (((map o pairself) fst params, base_sort,
    3.70 -          morph, assm_intro, of_class, axiom), ([], operations)))
    3.71 +          base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
    3.72        #> fold (curry Graph.add_edge class) sups;
    3.73    in ClassData.map add_class thy end;
    3.74  
    3.75  fun activate_defs class thms thy =
    3.76    let
    3.77      val eq_morph = Element.eq_morphism thy thms;
    3.78 -    fun amend cls thy = Locale.amend_registration_legacy eq_morph
    3.79 -      (cls, morphism thy cls) thy;
    3.80 +    fun amend cls thy = Locale.amend_registration (cls, base_morphism thy cls)
    3.81 +      (eq_morph, true) (export_morphism thy cls) thy;
    3.82    in fold amend (heritage thy [class]) thy end;
    3.83  
    3.84  fun register_operation class (c, (t, some_def)) thy =