src/Pure/Isar/theory_target.ML
changeset 24935 a033971c63a0
parent 24914 95cda5dd58d5
child 24939 6dd60d1191bf
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Oct 09 17:10:48 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Oct 09 17:10:49 2007 +0200
     1.3 @@ -2,15 +2,15 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Common theory/locale targets.
     1.8 +Common theory/locale/class targets.
     1.9  *)
    1.10  
    1.11  signature THEORY_TARGET =
    1.12  sig
    1.13    val peek: local_theory -> string option
    1.14 -  val begin: bstring -> Proof.context -> local_theory
    1.15 -  val init: xstring option -> theory -> local_theory
    1.16 -  val init_i: string option -> theory -> local_theory
    1.17 +  val begin: string -> Proof.context -> local_theory
    1.18 +  val init: string option -> theory -> local_theory
    1.19 +  val init_cmd: xstring option -> theory -> local_theory
    1.20  end;
    1.21  
    1.22  structure TheoryTarget: THEORY_TARGET =
    1.23 @@ -53,13 +53,9 @@
    1.24  
    1.25  (* target declarations *)
    1.26  
    1.27 -fun target_morphism loc lthy =
    1.28 -  ProofContext.export_morphism lthy (LocalTheory.target_of lthy) $>
    1.29 -  Morphism.thm_morphism Goal.norm_result;
    1.30 -
    1.31  fun target_decl add loc d lthy =
    1.32    let
    1.33 -    val d' = Morphism.transform (target_morphism loc lthy) d;
    1.34 +    val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
    1.35      val d0 = Morphism.form d';
    1.36    in
    1.37      if loc = "" then
    1.38 @@ -228,31 +224,30 @@
    1.39  
    1.40  in
    1.41  
    1.42 -fun defs kind args lthy0 =
    1.43 +fun local_def kind ((c, mx), ((name, atts), rhs)) lthy1 =
    1.44    let
    1.45 -    fun def ((c, mx), ((name, atts), rhs)) lthy1 =
    1.46 -      let
    1.47 -        val (rhs', rhs_conv) = expand_term lthy0 rhs;
    1.48 -        val xs = Variable.add_fixed (LocalTheory.target_of lthy0) rhs' [];
    1.49 -        val T = Term.fastype_of rhs;
    1.50 +    val (rhs', rhs_conv) = expand_term lthy1 rhs;
    1.51 +    val xs = Variable.add_fixed (LocalTheory.target_of lthy1) rhs' [];
    1.52 +    val T = Term.fastype_of rhs;
    1.53  
    1.54 -        val ([(lhs, lhs_def)], lthy2) = lthy1
    1.55 -          |> LocalTheory.consts (member (op =) xs) [((c, T), mx)];
    1.56 -        val lhs' = #2 (Logic.dest_equals (Thm.prop_of lhs_def));
    1.57 +    (*consts*)
    1.58 +    val ([(lhs, lhs_def)], lthy2) = lthy1
    1.59 +      |> LocalTheory.consts (member (op =) xs) [((c, T), mx)];
    1.60 +    val (_, lhs') = Logic.dest_equals (Thm.prop_of lhs_def);
    1.61  
    1.62 -        val name' = Thm.def_name_optional c name;
    1.63 -        val (def, lthy3) = lthy2
    1.64 -          |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
    1.65 -        val eq = LocalDefs.trans_terms lthy3
    1.66 -          [(*c == loc.c xs*) lhs_def,
    1.67 -           (*lhs' == rhs'*)  def,
    1.68 -           (*rhs' == rhs*)   Thm.symmetric rhs_conv];
    1.69 -      in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
    1.70 +    (*def*)
    1.71 +    val name' = Thm.def_name_optional c name;
    1.72 +    val (def, lthy3) = lthy2
    1.73 +      |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
    1.74 +    val eq = LocalDefs.trans_terms lthy3
    1.75 +      [(*c == loc.c xs*) lhs_def,
    1.76 +       (*lhs' == rhs'*)  def,
    1.77 +       (*rhs' == rhs*)   Thm.symmetric rhs_conv];
    1.78  
    1.79 -    val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
    1.80 -    val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
    1.81 -
    1.82 -  in (lhss ~~ map (apsnd the_single) res, lthy'') end;
    1.83 +    (*notes*)
    1.84 +    val ([(res_name, [res])], lthy4) = lthy3
    1.85 +      |> LocalTheory.notes kind [((name', atts), [([eq], [])])];
    1.86 +  in ((lhs, (res_name, res)), lthy4) end;
    1.87  
    1.88  end;
    1.89  
    1.90 @@ -363,11 +358,9 @@
    1.91  
    1.92      |> is_loc ? LocalTheory.target (Locale.add_thmss loc kind target_facts)
    1.93  
    1.94 -    |> ProofContext.set_stmt true
    1.95      |> ProofContext.qualified_names
    1.96      |> ProofContext.note_thmss_i kind local_facts
    1.97      ||> ProofContext.restore_naming lthy
    1.98 -    ||> ProofContext.restore_mode lthy
    1.99    end;
   1.100  
   1.101  
   1.102 @@ -381,29 +374,28 @@
   1.103    in
   1.104      ctxt
   1.105      |> Data.put (if is_loc then SOME loc else NONE)
   1.106 -    |> the_default I (Option.map Class.init some_class)
   1.107 +    |> fold Class.init (the_list some_class)
   1.108      |> LocalTheory.init (NameSpace.base loc)
   1.109       {pretty = pretty loc,
   1.110        consts = consts is_loc some_class,
   1.111        axioms = axioms,
   1.112        abbrev = abbrev is_loc some_class,
   1.113 -      defs = defs,
   1.114 +      def = local_def,
   1.115        notes = notes loc,
   1.116        type_syntax = type_syntax loc,
   1.117        term_syntax = term_syntax loc,
   1.118        declaration = declaration loc,
   1.119 -      target_morphism = target_morphism loc,
   1.120        target_naming = target_naming loc,
   1.121        reinit = fn _ =>
   1.122          (if is_loc then Locale.init loc else ProofContext.init)
   1.123          #> begin loc,
   1.124 -      exit = LocalTheory.target_of }
   1.125 +      exit = LocalTheory.target_of}
   1.126    end;
   1.127  
   1.128 -fun init_i NONE thy = begin "" (ProofContext.init thy)
   1.129 -  | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
   1.130 +fun init NONE thy = begin "" (ProofContext.init thy)
   1.131 +  | init (SOME loc) thy = begin loc (Locale.init loc thy);
   1.132  
   1.133 -fun init (SOME "-") thy = init_i NONE thy
   1.134 -  | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
   1.135 +fun init_cmd (SOME "-") thy = init NONE thy
   1.136 +  | init_cmd loc thy = init (Option.map (Locale.intern thy) loc) thy;
   1.137  
   1.138  end;