coherent binding policy with primitive target operations
authorhaftmann
Fri Mar 13 19:17:58 2009 +0100 (2009-03-13 ago)
changeset 30519c05c0199826f
parent 30518 07b45c1aa788
child 30520 c4728771f04f
coherent binding policy with primitive target operations
src/Pure/Isar/class_target.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/theory_target.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/Isar/class_target.ML	Fri Mar 13 19:17:57 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 19:17:58 2009 +0100
     1.3 @@ -43,8 +43,8 @@
     1.4    val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
     1.5      -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
     1.6    val conclude_instantiation: local_theory -> local_theory
     1.7 -  val instantiation_param: local_theory -> string -> string option
     1.8 -  val confirm_declaration: string -> local_theory -> local_theory
     1.9 +  val instantiation_param: local_theory -> binding -> string option
    1.10 +  val confirm_declaration: binding -> local_theory -> local_theory
    1.11    val pretty_instantiation: local_theory -> Pretty.T
    1.12    val type_name: string -> string
    1.13  
    1.14 @@ -430,8 +430,8 @@
    1.15  
    1.16  val instantiation_params = #params o get_instantiation;
    1.17  
    1.18 -fun instantiation_param lthy v = instantiation_params lthy
    1.19 -  |> find_first (fn (_, (v', _)) => v = v')
    1.20 +fun instantiation_param lthy b = instantiation_params lthy
    1.21 +  |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
    1.22    |> Option.map (fst o fst);
    1.23  
    1.24  
    1.25 @@ -530,8 +530,8 @@
    1.26      |> synchronize_inst_syntax
    1.27    end;
    1.28  
    1.29 -fun confirm_declaration c = (map_instantiation o apsnd)
    1.30 -  (filter_out (fn (_, (c', _)) => c' = c))
    1.31 +fun confirm_declaration b = (map_instantiation o apsnd)
    1.32 +  (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
    1.33    #> LocalTheory.target synchronize_inst_syntax
    1.34  
    1.35  fun gen_instantiation_instance do_proof after_qed lthy =
     2.1 --- a/src/Pure/Isar/overloading.ML	Fri Mar 13 19:17:57 2009 +0100
     2.2 +++ b/src/Pure/Isar/overloading.ML	Fri Mar 13 19:17:58 2009 +0100
     2.3 @@ -9,9 +9,9 @@
     2.4    val init: (string * (string * typ) * bool) list -> theory -> local_theory
     2.5    val conclude: local_theory -> local_theory
     2.6    val declare: string * typ -> theory -> term * theory
     2.7 -  val confirm: string -> local_theory -> local_theory
     2.8 -  val define: bool -> string -> string * term -> theory -> thm * theory
     2.9 -  val operation: Proof.context -> string -> (string * bool) option
    2.10 +  val confirm: binding -> local_theory -> local_theory
    2.11 +  val define: bool -> binding -> string * term -> theory -> thm * theory
    2.12 +  val operation: Proof.context -> binding -> (string * bool) option
    2.13    val pretty: Proof.context -> Pretty.T
    2.14    
    2.15    type improvable_syntax
    2.16 @@ -123,18 +123,19 @@
    2.17  val get_overloading = OverloadingData.get o LocalTheory.target_of;
    2.18  val map_overloading = LocalTheory.target o OverloadingData.map;
    2.19  
    2.20 -fun operation lthy v = get_overloading lthy
    2.21 -  |> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
    2.22 +fun operation lthy b = get_overloading lthy
    2.23 +  |> get_first (fn ((c, _), (v, checked)) =>
    2.24 +      if Binding.name_of b = v then SOME (c, checked) else NONE);
    2.25  
    2.26 -fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
    2.27 +fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b));
    2.28  
    2.29  
    2.30  (* overloaded declarations and definitions *)
    2.31  
    2.32  fun declare c_ty = pair (Const c_ty);
    2.33  
    2.34 -fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name,
    2.35 -  Logic.mk_equals (Const (c, Term.fastype_of t), t));
    2.36 +fun define checked b (c, t) = Thm.add_def (not checked) true
    2.37 +  (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
    2.38  
    2.39  
    2.40  (* target *)
     3.1 --- a/src/Pure/Isar/theory_target.ML	Fri Mar 13 19:17:57 2009 +0100
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Mar 13 19:17:58 2009 +0100
     3.3 @@ -188,10 +188,7 @@
     3.4    in
     3.5      not (is_class andalso (similar_body orelse class_global)) ?
     3.6        (Context.mapping_result
     3.7 -        (fn thy => thy
     3.8 -          |> Sign.no_base_names
     3.9 -          |> Sign.add_abbrev PrintMode.internal tags legacy_arg
    3.10 -          ||> Sign.restore_naming thy)
    3.11 +        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
    3.12          (ProofContext.add_abbrev PrintMode.internal tags arg)
    3.13        #-> (fn (lhs' as Const (d, _), _) =>
    3.14            similar_body ?
    3.15 @@ -203,23 +200,22 @@
    3.16  
    3.17  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
    3.18    let
    3.19 -    val c = Binding.qualified_name_of b;
    3.20      val tags = LocalTheory.group_position_of lthy;
    3.21      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    3.22      val U = map #2 xs ---> T;
    3.23      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    3.24      val declare_const =
    3.25 -      (case Class_Target.instantiation_param lthy c of
    3.26 +      (case Class_Target.instantiation_param lthy b of
    3.27          SOME c' =>
    3.28            if mx3 <> NoSyn then syntax_error c'
    3.29            else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
    3.30 -            ##> Class_Target.confirm_declaration c
    3.31 +            ##> Class_Target.confirm_declaration b
    3.32          | NONE =>
    3.33 -            (case Overloading.operation lthy c of
    3.34 +            (case Overloading.operation lthy b of
    3.35                SOME (c', _) =>
    3.36                  if mx3 <> NoSyn then syntax_error c'
    3.37                  else LocalTheory.theory_result (Overloading.declare (c', U))
    3.38 -                  ##> Overloading.confirm c
    3.39 +                  ##> Overloading.confirm b
    3.40              | NONE => LocalTheory.theory_result (Sign.declare_const tags ((b, U), mx3))));
    3.41      val (const, lthy') = lthy |> declare_const;
    3.42      val t = Term.list_comb (const, map Free xs);
    3.43 @@ -282,17 +278,14 @@
    3.44      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    3.45  
    3.46      (*def*)
    3.47 -    val c = Binding.qualified_name_of b;
    3.48 -    val define_const =
    3.49 -      (case Overloading.operation lthy c of
    3.50 -        SOME (_, checked) =>
    3.51 -          (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    3.52 -      | NONE =>
    3.53 -          if is_none (Class_Target.instantiation_param lthy c)
    3.54 -          then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
    3.55 -          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
    3.56      val (global_def, lthy3) = lthy2
    3.57 -      |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
    3.58 +      |> LocalTheory.theory_result (case Overloading.operation lthy b of
    3.59 +          SOME (_, checked) =>
    3.60 +            Overloading.define checked name' ((fst o dest_Const) lhs', rhs')
    3.61 +        | NONE =>
    3.62 +            if is_none (Class_Target.instantiation_param lthy b)
    3.63 +            then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
    3.64 +            else AxClass.define_overloaded name' ((fst o dest_Const) lhs', rhs'));
    3.65      val def = LocalDefs.trans_terms lthy3
    3.66        [(*c == global.c xs*)     local_def,
    3.67         (*global.c xs == rhs'*)  global_def,
     4.1 --- a/src/Pure/axclass.ML	Fri Mar 13 19:17:57 2009 +0100
     4.2 +++ b/src/Pure/axclass.ML	Fri Mar 13 19:17:58 2009 +0100
     4.3 @@ -27,7 +27,7 @@
     4.4    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
     4.5    val instance_name: string * class -> string
     4.6    val declare_overloaded: string * typ -> theory -> term * theory
     4.7 -  val define_overloaded: string -> string * term -> theory -> thm * theory
     4.8 +  val define_overloaded: binding -> string * term -> theory -> thm * theory
     4.9    val inst_tyco_of: theory -> string * typ -> string option
    4.10    val unoverload: theory -> thm -> thm
    4.11    val overload: theory -> thm -> thm
    4.12 @@ -383,16 +383,17 @@
    4.13        #> pair (Const (c, T))))
    4.14    end;
    4.15  
    4.16 -fun define_overloaded name (c, t) thy =
    4.17 +fun define_overloaded b (c, t) thy =
    4.18    let
    4.19      val T = Term.fastype_of t;
    4.20      val SOME tyco = inst_tyco_of thy (c, T);
    4.21      val (c', eq) = get_inst_param thy (c, tyco);
    4.22      val prop = Logic.mk_equals (Const (c', T), t);
    4.23 -    val name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name;
    4.24 +    val b' = Thm.def_binding_optional
    4.25 +      (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b;
    4.26    in
    4.27      thy
    4.28 -    |> Thm.add_def false false (Binding.name name', prop)
    4.29 +    |> Thm.add_def false false (b', prop)
    4.30      |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
    4.31    end;
    4.32