src/Pure/Isar/theory_target.ML
changeset 25485 33840a854e63
parent 25462 dad0291cb76a
child 25514 4b508bb31a6c
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Nov 28 09:01:40 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Nov 28 09:01:42 2007 +0100
     1.3 @@ -190,30 +190,29 @@
     1.4               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
     1.5    end;
     1.6  
     1.7 -fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy =
     1.8 +fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
     1.9    let
    1.10      val pos = ContextPosition.properties_of lthy;
    1.11      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.12      val U = map #2 xs ---> T;
    1.13      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.14 -    val declare_const = if null instantiation
    1.15 -      then Sign.declare_const pos (c, U, mx3)
    1.16 -      else case Class.instantiation_const lthy c
    1.17 -       of SOME c' => Class.declare_overloaded (c', U, mx3)
    1.18 -        | NONE => Sign.declare_const pos (c, U, mx3);
    1.19 -    val (const, lthy') = lthy |> LocalTheory.theory_result declare_const;
    1.20 +    val declare_const = case Class.instantiation_param lthy c
    1.21 +       of SOME c' => LocalTheory.theory_result (Class.overloaded_const (c', U, mx3))
    1.22 +            ##> Class.confirm_declaration c
    1.23 +        | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
    1.24 +    val (const, lthy') = lthy |> declare_const;
    1.25      val t = Term.list_comb (const, map Free xs);
    1.26    in
    1.27      lthy'
    1.28      |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default pos ((c, mx2), t))
    1.29 -    |> is_class ? class_target ta (Class.add_logical_const target pos ((c, mx1), t))
    1.30 +    |> is_class ? class_target ta (Class.logical_const target pos ((c, mx1), t))
    1.31      |> LocalDefs.add_def ((c, NoSyn), t)
    1.32    end;
    1.33  
    1.34  
    1.35  (* abbrev *)
    1.36  
    1.37 -fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy =
    1.38 +fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
    1.39    let
    1.40      val pos = ContextPosition.properties_of lthy;
    1.41      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.42 @@ -232,7 +231,7 @@
    1.43          #-> (fn (lhs, _) =>
    1.44            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.45              term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>
    1.46 -            is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), t'))
    1.47 +            is_class ? class_target ta (Class.syntactic_const target prmode pos ((c, mx1), t'))
    1.48            end)
    1.49        else
    1.50          LocalTheory.theory
    1.51 @@ -245,7 +244,7 @@
    1.52  
    1.53  (* define *)
    1.54  
    1.55 -fun define (ta as Target {target, is_locale, is_class, instantiation})
    1.56 +fun define (ta as Target {target, is_locale, is_class, ...})
    1.57      kind ((c, mx), ((name, atts), rhs)) lthy =
    1.58    let
    1.59      val thy = ProofContext.theory_of lthy;
    1.60 @@ -262,18 +261,15 @@
    1.61      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    1.62  
    1.63      (*def*)
    1.64 -    val is_instantiation = not (null instantiation)
    1.65 -      andalso is_some (Class.instantiation_const lthy c);
    1.66 -    val define_const = if not is_instantiation
    1.67 +    val define_const = if is_none (Class.instantiation_param lthy c)
    1.68        then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
    1.69 -      else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs));
    1.70 +      else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    1.71      val (global_def, lthy3) = lthy2
    1.72        |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
    1.73 -    val def = if not is_instantiation then LocalDefs.trans_terms lthy3
    1.74 +    val def = LocalDefs.trans_terms lthy3
    1.75        [(*c == global.c xs*)     local_def,
    1.76         (*global.c xs == rhs'*)  global_def,
    1.77 -       (*rhs' == rhs*)          Thm.symmetric rhs_conv]
    1.78 -      else Thm.transitive local_def global_def;
    1.79 +       (*rhs' == rhs*)          Thm.symmetric rhs_conv];
    1.80  
    1.81      (*note*)
    1.82      val ([(res_name, [res])], lthy4) = lthy3
    1.83 @@ -294,7 +290,12 @@
    1.84      val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
    1.85  
    1.86      (*axioms*)
    1.87 -    val hyps = map Thm.term_of (Assumption.assms_of lthy');
    1.88 +    val resubst_instparams = map_aterms (fn t as Free (v, T) =>
    1.89 +      (case Class.instantiation_param lthy' v
    1.90 +       of NONE => t
    1.91 +        | SOME c => Const (c, T)) | t => t)
    1.92 +    val hyps = map Thm.term_of (Assumption.assms_of lthy')
    1.93 +      |> map resubst_instparams;
    1.94      fun axiom ((name, atts), props) thy = thy
    1.95        |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
    1.96        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.97 @@ -318,11 +319,10 @@
    1.98  fun init_instantiaton arities = make_target "" false false arities
    1.99  
   1.100  fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
   1.101 -  if null instantiation then
   1.102 -    if not is_locale then ProofContext.init
   1.103 -    else if not is_class then Locale.init target
   1.104 -    else Class.init target
   1.105 -  else Class.instantiation instantiation;
   1.106 +  if not (null instantiation) then Class.init_instantiation instantiation
   1.107 +  else if not is_locale then ProofContext.init
   1.108 +  else if not is_class then Locale.init target
   1.109 +  else Class.init target;
   1.110  
   1.111  fun init_lthy (ta as Target {target, instantiation, ...}) =
   1.112    Data.put ta #>
   1.113 @@ -336,7 +336,8 @@
   1.114      term_syntax = term_syntax ta,
   1.115      declaration = declaration ta,
   1.116      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
   1.117 -    exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation}
   1.118 +    exit = if null instantiation then LocalTheory.target_of
   1.119 +      else Class.conclude_instantiation #> LocalTheory.target_of}
   1.120  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
   1.121  
   1.122  in
   1.123 @@ -347,8 +348,8 @@
   1.124  fun context "-" thy = init NONE thy
   1.125    | context target thy = init (SOME (Locale.intern thy target)) thy;
   1.126  
   1.127 -fun instantiation raw_arities thy =
   1.128 -  init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy;
   1.129 +fun instantiation arities thy =
   1.130 +  init_lthy_ctxt (init_instantiaton arities) thy;
   1.131  
   1.132  end;
   1.133