theorem(_i): locale atts;
authorwenzelm
Tue Nov 06 01:20:49 2001 +0100 (2001-11-06)
changeset 120655f7f44d5e3dd
parent 12064 34c270893ecb
child 12066 31337dd5f596
theorem(_i): locale atts;
global_goal, finish_global: proper treatment of target locale;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Nov 06 01:19:07 2001 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Nov 06 01:20:49 2001 +0100
     1.3 @@ -76,10 +76,12 @@
     1.4    val def: string -> context attribute list -> string *  (string * string list) -> state -> state
     1.5    val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
     1.6    val invoke_case: string * string option list * context attribute list -> state -> state
     1.7 -  val theorem: string -> xstring option -> context attribute Locale.element list -> bstring
     1.8 -    -> theory attribute list -> string * (string list * string list) -> theory -> state
     1.9 -  val theorem_i: string -> string option -> context attribute Locale.element_i list -> bstring
    1.10 -    -> theory attribute list -> term * (term list * term list) -> theory -> state
    1.11 +  val theorem: string
    1.12 +    -> (xstring * context attribute list) option -> context attribute Locale.element list
    1.13 +    -> bstring -> theory attribute list -> string * (string list * string list) -> theory -> state
    1.14 +  val theorem_i: string
    1.15 +    -> (string * context attribute list) option -> context attribute Locale.element_i list
    1.16 +    -> bstring -> theory attribute list -> term * (term list * term list) -> theory -> state
    1.17    val chain: state -> state
    1.18    val from_facts: thm list -> state -> state
    1.19    val show: (bool -> state -> state) -> (state -> state Seq.seq) -> string
    1.20 @@ -119,12 +121,13 @@
    1.21  (* type goal *)
    1.22  
    1.23  datatype kind =
    1.24 -  Theorem of string * string option * theory attribute list |    (*theorem with kind and locale*)
    1.25 -  Show of context attribute list |               (*intermediate result, solving subgoal*)
    1.26 -  Have of context attribute list;                (*intermediate result*)
    1.27 +  Theorem of string * (string * context attribute list) option * theory attribute list |
    1.28 +    (*theorem with kind, locale target, attributes*)
    1.29 +  Show of context attribute list |  (*intermediate result, solving subgoal*)
    1.30 +  Have of context attribute list;   (*intermediate result*)
    1.31  
    1.32  fun kind_name _ (Theorem (s, None, _)) = s
    1.33 -  | kind_name sg (Theorem (s, Some loc, _)) = s ^ " (in " ^ Locale.cond_extern sg loc ^ ")"
    1.34 +  | kind_name sg (Theorem (s, Some (name, _), _)) = s ^ " (in " ^ Locale.cond_extern sg name ^ ")"
    1.35    | kind_name _ (Show _) = "show"
    1.36    | kind_name _ (Have _) = "have";
    1.37  
    1.38 @@ -610,18 +613,20 @@
    1.39    end;
    1.40  
    1.41  (*global goals*)
    1.42 -fun global_goal prepp act_locale act_elems kind locale elems name atts x thy =
    1.43 -  thy |> init_state
    1.44 -  |> open_block |> (case locale of Some loc => map_context (act_locale loc) | None => I)
    1.45 -  |> open_block |> map_context (act_elems elems)
    1.46 -  |> setup_goal I prepp (ProofContext.fix_frees o single) (Theorem (kind, locale, atts))
    1.47 -    Seq.single name x;
    1.48 +fun global_goal prepp prep_locale activate kind raw_locale elems name atts x thy =
    1.49 +  let val locale = apsome (apfst (prep_locale (Theory.sign_of thy))) raw_locale in
    1.50 +    thy
    1.51 +    |> init_state
    1.52 +    |> open_block
    1.53 +    |> (case locale of Some (name, _) => map_context (Locale.activate_locale_i name) | None => I)
    1.54 +    |> open_block
    1.55 +    |> map_context (activate elems)
    1.56 +    |> setup_goal I prepp (ProofContext.fix_frees o single) (Theorem (kind, locale, atts))
    1.57 +      Seq.single name x
    1.58 +  end;
    1.59  
    1.60 -val theorem = global_goal ProofContext.bind_propp_schematic
    1.61 -  Locale.activate_locale Locale.activate_elements;
    1.62 -
    1.63 -val theorem_i = global_goal ProofContext.bind_propp_schematic_i
    1.64 -  Locale.activate_locale_i Locale.activate_elements_i;
    1.65 +val theorem = global_goal ProofContext.bind_propp_schematic Locale.intern Locale.activate_elements;
    1.66 +val theorem_i = global_goal ProofContext.bind_propp_schematic_i (K I) Locale.activate_elements_i;
    1.67  
    1.68  
    1.69  (*local goals*)
    1.70 @@ -708,35 +713,38 @@
    1.71  
    1.72  (* global_qed *)
    1.73  
    1.74 +fun locale_store_thm _ None _ = I
    1.75 +  | locale_store_thm name (Some (loc, atts)) th = Locale.store_thm loc ((name, th), atts);
    1.76 +
    1.77  fun finish_global state =
    1.78    let
    1.79 -    val (goal_ctxt, (((kind, name, t), (_, raw_thm)), _)) = current_goal state;
    1.80 -    val full_name = if name = "" then "" else Sign.full_name (sign_of state) name;
    1.81 -    val locale_context = context_of (state |> close_block);  (* FIXME unused *)
    1.82 -    val theory_context = context_of (state |> close_block |> close_block);
    1.83 +    fun export inner outer th =
    1.84 +      (case Seq.pull (ProofContext.export false inner outer th) of
    1.85 +        Some (th', _) => th' |> Drule.local_standard
    1.86 +      | None => raise STATE ("Internal failure of theorem export", state));
    1.87  
    1.88 -    val result = prep_result state t raw_thm;
    1.89 -    val resultq =
    1.90 -      ProofContext.export false goal_ctxt theory_context result
    1.91 -      |> Seq.map Drule.local_standard;
    1.92 +    val (goal_ctxt, (((kind, name, t), (_, raw_thm)), _)) = current_goal state;
    1.93 +    val locale_ctxt = context_of (state |> close_block);
    1.94 +    val theory_ctxt = context_of (state |> close_block |> close_block);
    1.95  
    1.96 -    val (atts, opt_locale) =
    1.97 -      (case kind of Theorem (s, loc, atts) => (atts @ [Drule.kind s], loc)
    1.98 +    val locale_result = prep_result state t raw_thm |> export goal_ctxt locale_ctxt;
    1.99 +    val result = locale_result |> export locale_ctxt theory_ctxt;
   1.100 +
   1.101 +    val (kname, atts, locale) =
   1.102 +      (case kind of Theorem (s, locale, atts) => (s, atts @ [Drule.kind s], locale)
   1.103        | _ => err_malformed "finish_global" state);
   1.104 -    val thy = theory_of state;
   1.105 -  in
   1.106 -    resultq |> Seq.map (fn res =>
   1.107 -      let val (thy', res') = PureThy.store_thm ((name, res), atts) thy
   1.108 -      in (thy', {kind = kind_name (sign_of state) kind, name = name, thm = res'}) end)
   1.109 -  end;
   1.110 +    val (thy', result') =
   1.111 +      theory_of state
   1.112 +      |> PureThy.store_thm ((name, result), atts)
   1.113 +      |>> locale_store_thm name locale locale_result;
   1.114 +  in (thy', {kind = kname, name = name, thm = result'}) end;
   1.115  
   1.116  (*note: clients should inspect first result only, as backtracking may destroy theory*)
   1.117  fun global_qed finalize state =
   1.118    state
   1.119    |> end_proof true
   1.120    |> finalize
   1.121 -  |> Seq.map finish_global
   1.122 -  |> Seq.flat;
   1.123 +  |> Seq.map finish_global;
   1.124  
   1.125  
   1.126