src/Pure/Isar/theory_target.ML
changeset 29006 abe0f11cfa4e
parent 28991 694227dd3e8c
child 29102 2e1011dcd577
child 29223 e09c53289830
equal deleted inserted replaced
29005:ce378dcfddab 29006:abe0f11cfa4e
   198     val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
   198     val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
   199     val arg = (b', Term.close_schematic_term rhs');
   199     val arg = (b', Term.close_schematic_term rhs');
   200     val similar_body = Type.similar_types (rhs, rhs');
   200     val similar_body = Type.similar_types (rhs, rhs');
   201     (* FIXME workaround based on educated guess *)
   201     (* FIXME workaround based on educated guess *)
   202     val (prefix', _) = Binding.dest b';
   202     val (prefix', _) = Binding.dest b';
   203     val class_global = Name.name_of b = Name.name_of b'
   203     val class_global = Binding.base_name b = Binding.base_name b'
   204       andalso not (null prefix')
   204       andalso not (null prefix')
   205       andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
   205       andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
   206   in
   206   in
   207     not (is_class andalso (similar_body orelse class_global)) ?
   207     not (is_class andalso (similar_body orelse class_global)) ?
   208       (Context.mapping_result
   208       (Context.mapping_result
   217              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   217              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   218   end;
   218   end;
   219 
   219 
   220 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   220 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   221   let
   221   let
   222     val c = Name.name_of b;
   222     val c = Binding.base_name b;
   223     val tags = LocalTheory.group_position_of lthy;
   223     val tags = LocalTheory.group_position_of lthy;
   224     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   224     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   225     val U = map #2 xs ---> T;
   225     val U = map #2 xs ---> T;
   226     val (mx1, mx2, mx3) = fork_mixfix ta mx;
   226     val (mx1, mx2, mx3) = fork_mixfix ta mx;
   227     fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   227     fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   250 
   250 
   251 (* abbrev *)
   251 (* abbrev *)
   252 
   252 
   253 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   253 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   254   let
   254   let
   255     val c = Name.name_of b;
   255     val c = Binding.base_name b;
   256     val tags = LocalTheory.group_position_of lthy;
   256     val tags = LocalTheory.group_position_of lthy;
   257     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   257     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   258     val target_ctxt = LocalTheory.target_of lthy;
   258     val target_ctxt = LocalTheory.target_of lthy;
   259 
   259 
   260     val (mx1, mx2, mx3) = fork_mixfix ta mx;
   260     val (mx1, mx2, mx3) = fork_mixfix ta mx;
   287     kind ((b, mx), ((name, atts), rhs)) lthy =
   287     kind ((b, mx), ((name, atts), rhs)) lthy =
   288   let
   288   let
   289     val thy = ProofContext.theory_of lthy;
   289     val thy = ProofContext.theory_of lthy;
   290     val thy_ctxt = ProofContext.init thy;
   290     val thy_ctxt = ProofContext.init thy;
   291 
   291 
   292     val c = Name.name_of b;
   292     val c = Binding.base_name b;
   293     val name' = Binding.map_base (Thm.def_name_optional c) name;
   293     val name' = Binding.map_base (Thm.def_name_optional c) name;
   294     val (rhs', rhs_conv) =
   294     val (rhs', rhs_conv) =
   295       LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   295       LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   296     val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
   296     val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
   297     val T = Term.fastype_of rhs;
   297     val T = Term.fastype_of rhs;
   308       | NONE =>
   308       | NONE =>
   309           if is_none (Class.instantiation_param lthy c)
   309           if is_none (Class.instantiation_param lthy c)
   310           then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
   310           then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
   311           else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
   311           else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
   312     val (global_def, lthy3) = lthy2
   312     val (global_def, lthy3) = lthy2
   313       |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
   313       |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
   314     val def = LocalDefs.trans_terms lthy3
   314     val def = LocalDefs.trans_terms lthy3
   315       [(*c == global.c xs*)     local_def,
   315       [(*c == global.c xs*)     local_def,
   316        (*global.c xs == rhs'*)  global_def,
   316        (*global.c xs == rhs'*)  global_def,
   317        (*rhs' == rhs*)          Thm.symmetric rhs_conv];
   317        (*rhs' == rhs*)          Thm.symmetric rhs_conv];
   318 
   318