eq_morphism is always optional: avoid trivial morphism for empty list of equations
authorhaftmann
Wed May 05 09:24:42 2010 +0200 (2010-05-05)
changeset 36674d95f39448121
parent 36673 6d25e8dab1e3
child 36675 806ea6e282e4
child 36692 54b64d4ad524
eq_morphism is always optional: avoid trivial morphism for empty list of equations
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed May 05 09:24:41 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed May 05 09:24:42 2010 +0200
     1.3 @@ -74,7 +74,10 @@
     1.4      fun prove_assm_intro thm =
     1.5        let
     1.6          val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
     1.7 -        val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
     1.8 +        val const_eq_morph = case eq_morph
     1.9 +         of SOME eq_morph => const_morph $> eq_morph
    1.10 +          | NONE => const_morph
    1.11 +        val thm'' = Morphism.thm const_eq_morph thm';
    1.12          val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
    1.13        in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.14      val assm_intro = Option.map prove_assm_intro
    1.15 @@ -290,7 +293,9 @@
    1.16      |-> (fn (param_map, params, assm_axiom) =>
    1.17         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
    1.18      #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
    1.19 -       Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph
    1.20 +       Locale.add_registration (class, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph)
    1.21 +         (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*)
    1.22 +         (Option.map (rpair true) eq_morph) export_morph
    1.23      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.24      |> Theory_Target.init (SOME class)
    1.25      |> pair class
     2.1 --- a/src/Pure/Isar/class_target.ML	Wed May 05 09:24:41 2010 +0200
     2.2 +++ b/src/Pure/Isar/class_target.ML	Wed May 05 09:24:42 2010 +0200
     2.3 @@ -151,8 +151,9 @@
     2.4  fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
     2.5  
     2.6  val base_morphism = #base_morph oo the_class_data;
     2.7 -fun morphism thy class = base_morphism thy class
     2.8 -  $> Element.eq_morphism thy (these_defs thy [class]);
     2.9 +fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
    2.10 + of SOME eq_morph => base_morphism thy class $> eq_morph
    2.11 +  | NONE => base_morphism thy class;
    2.12  val export_morphism = #export_morph oo the_class_data;
    2.13  
    2.14  fun print_classes thy =
    2.15 @@ -202,12 +203,11 @@
    2.16        #> fold (curry Graph.add_edge class) sups;
    2.17    in ClassData.map add_class thy end;
    2.18  
    2.19 -fun activate_defs class thms thy =
    2.20 -  let
    2.21 -    val eq_morph = Element.eq_morphism thy thms;
    2.22 -    fun amend cls thy = Locale.amend_registration (cls, base_morphism thy cls)
    2.23 -      (eq_morph, true) (export_morphism thy cls) thy;
    2.24 -  in fold amend (heritage thy [class]) thy end;
    2.25 +fun activate_defs class thms thy = case Element.eq_morphism thy thms
    2.26 + of SOME eq_morph => fold (fn cls => fn thy =>
    2.27 +      Locale.amend_registration (cls, base_morphism thy cls)
    2.28 +        (eq_morph, true) (export_morphism thy cls) thy) (heritage thy [class]) thy
    2.29 +  | NONE => thy;
    2.30  
    2.31  fun register_operation class (c, (t, some_def)) thy =
    2.32    let
    2.33 @@ -223,7 +223,7 @@
    2.34        (fn (defs, operations) =>
    2.35          (fold cons (the_list some_def) defs,
    2.36            (c, (class, (ty', t'))) :: operations))
    2.37 -    |> is_some some_def ? activate_defs class (the_list some_def)
    2.38 +    |> activate_defs class (the_list some_def)
    2.39    end;
    2.40  
    2.41  fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
     3.1 --- a/src/Pure/Isar/element.ML	Wed May 05 09:24:41 2010 +0200
     3.2 +++ b/src/Pure/Isar/element.ML	Wed May 05 09:24:42 2010 +0200
     3.3 @@ -55,7 +55,7 @@
     3.4    val satisfy_facts: witness list ->
     3.5      (Attrib.binding * (thm list * Attrib.src list) list) list ->
     3.6      (Attrib.binding * (thm list * Attrib.src list) list) list
     3.7 -  val eq_morphism: theory -> thm list -> morphism
     3.8 +  val eq_morphism: theory -> thm list -> morphism option
     3.9    val transfer_morphism: theory -> morphism
    3.10    val init: context_i -> Context.generic -> Context.generic
    3.11    val activate_i: context_i -> Proof.context -> context_i * Proof.context
    3.12 @@ -448,11 +448,11 @@
    3.13  
    3.14  (* rewriting with equalities *)
    3.15  
    3.16 -fun eq_morphism thy thms = Morphism.morphism
    3.17 +fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
    3.18   {binding = I,
    3.19    typ = I,
    3.20    term = MetaSimplifier.rewrite_term thy thms [],
    3.21 -  fact = map (MetaSimplifier.rewrite_rule thms)};
    3.22 +  fact = map (MetaSimplifier.rewrite_rule thms)});
    3.23  
    3.24  
    3.25  (* transfer to theory using closure *)
     4.1 --- a/src/Pure/Isar/expression.ML	Wed May 05 09:24:41 2010 +0200
     4.2 +++ b/src/Pure/Isar/expression.ML	Wed May 05 09:24:42 2010 +0200
     4.3 @@ -821,7 +821,7 @@
     4.4        #-> (fn eqns => fold (fn ((dep, morph), wits) =>
     4.5          fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
     4.6              (map (Element.morph_witness export') wits))
     4.7 -          (if null eqns then NONE else SOME (Element.eq_morphism thy eqns, true))
     4.8 +          (Element.eq_morphism thy eqns |> Option.map (rpair true))
     4.9            export thy) (deps ~~ witss)));
    4.10  
    4.11    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;