(*  Title:      Pure/Isar/isar_thy.ML
    ID:         $Id: isar_thy.ML,v 1.170 2005/09/17 10:18:04 wenzelm Exp $
    Author:     Markus Wenzel, TU Muenchen

Derived theory and proof operations.
*)

signature ISAR_THY =
sig
  val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
  val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
  val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
  val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
  val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list
  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
  val theorems: string ->
    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    -> theory -> theory * (string * thm list) list
  val theorems_i: string ->
    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
    -> theory -> theory * (string * thm list) list
  val smart_theorems: string -> xstring option ->
    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
    theory -> theory * Proof.context
  val declare_theorems: xstring option ->
    (thmref * Attrib.src list) list -> theory -> theory * Proof.context
  val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    bool -> Proof.state -> Proof.state
  val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    bool -> Proof.state -> Proof.state
  val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    bool -> Proof.state -> Proof.state
  val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    bool -> Proof.state -> Proof.state
  val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
    theory -> Proof.state
  val theorem_i: string -> string * theory attribute list -> term * (term list * term list) ->
    theory -> Proof.state
  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
  val terminal_proof: Method.text * Method.text option ->
    Toplevel.transition -> Toplevel.transition
  val default_proof: Toplevel.transition -> Toplevel.transition
  val immediate_proof: Toplevel.transition -> Toplevel.transition
  val done_proof: Toplevel.transition -> Toplevel.transition
  val skip_proof: Toplevel.transition -> Toplevel.transition
  val forget_proof: Toplevel.transition -> Toplevel.transition
  val begin_theory: string -> string list -> (string * bool) list -> bool -> theory
  val end_theory: theory -> theory
  val kill_theory: string -> unit
  val theory: string * string list * (string * bool) list
    -> Toplevel.transition -> Toplevel.transition
  val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
  val context: string -> Toplevel.transition -> Toplevel.transition
end;

structure IsarThy: ISAR_THY =
struct

(* axioms and defs *)

fun add_axms f args thy =
  f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;

val add_axioms = add_axms (#1 oo PureThy.add_axioms);
val add_axioms_i = #1 oo PureThy.add_axioms_i;
fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) args;
fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) args;


(* theorems *)

fun present_theorems kind (thy, named_thmss) =
  conditional (kind <> "" andalso kind <> Drule.internalK) (fn () =>
    Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);

fun theorems kind args thy = thy
  |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
  |> tap (present_theorems kind);

fun theorems_i kind args =
  PureThy.note_thmss_i (Drule.kind kind) args
  #> tap (present_theorems kind);

fun apply_theorems args = apsnd (List.concat o map snd) o theorems "" [(("", []), args)];
fun apply_theorems_i args = apsnd (List.concat o map snd) o theorems_i "" [(("", []), args)];

fun smart_theorems kind NONE args thy = thy
      |> theorems kind args
      |> tap (present_theorems kind)
      |> (fn (thy, _) => (thy, ProofContext.init thy))
  | smart_theorems kind (SOME loc) args thy = thy
      |> Locale.note_thmss kind loc args
      |> tap (present_theorems kind o apfst #1)
      |> #1;

fun declare_theorems opt_loc args =
  smart_theorems "" opt_loc [(("", []), args)];


(* goals *)

local

fun local_goal opt_chain goal stmt int =
  opt_chain #> goal (K (K Seq.single)) stmt int;

fun global_goal goal kind a propp thy =
  goal kind (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy);

in

val have = local_goal I Proof.have;
val hence = local_goal Proof.chain Proof.have;
val show = local_goal I Proof.show;
val thus = local_goal Proof.chain Proof.show;
val theorem = global_goal Proof.theorem;
val theorem_i = global_goal Proof.theorem_i;

end;


(* local endings *)

fun local_qed m = Toplevel.proof (ProofHistory.applys (Proof.local_qed (m, true)));
val local_terminal_proof = Toplevel.proof o ProofHistory.applys o Proof.local_terminal_proof;
val local_default_proof = Toplevel.proof (ProofHistory.applys Proof.local_default_proof);
val local_immediate_proof = Toplevel.proof (ProofHistory.applys Proof.local_immediate_proof);
val local_done_proof = Toplevel.proof (ProofHistory.applys Proof.local_done_proof);
val local_skip_proof = Toplevel.proof' (ProofHistory.applys o Proof.local_skip_proof);

val skip_local_qed =
  Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF));


(* global endings *)

fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn prf =>
  let
    val state = ProofHistory.current prf;
    val _ = Proof.assert_bottom true state handle Proof.STATE _ => raise Toplevel.UNDEF;
  in ending int state end);

fun global_qed m = global_ending (K (Proof.global_qed (m, true)));
val global_terminal_proof = global_ending o K o Proof.global_terminal_proof;
val global_default_proof = global_ending (K Proof.global_default_proof);
val global_immediate_proof = global_ending (K Proof.global_immediate_proof);
val global_skip_proof = global_ending Proof.global_skip_proof;
val global_done_proof = global_ending (K Proof.global_done_proof);

val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1 o History.current);


(* common endings *)

fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
val default_proof = local_default_proof o global_default_proof;
val immediate_proof = local_immediate_proof o global_immediate_proof;
val done_proof = local_done_proof o global_done_proof;
val skip_proof = local_skip_proof o global_skip_proof;

val forget_proof =
  Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current) o
  Toplevel.skip_proof_to_theory (K true);


(* theory init and exit *)

fun begin_theory name imports uses =
  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);

val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory;

val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;

fun theory (name, imports, uses) =
  Toplevel.init_theory (begin_theory name imports uses)
    (fn thy => (end_theory thy; ()))
    (kill_theory o Context.theory_name);


(* context switch *)

fun fetch_context f x =
  (case Context.pass NONE f x of
    ((), NONE) => raise Toplevel.UNDEF
  | ((), SOME thy) => thy);

fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ());

val context = init_context (ThyInfo.quiet_update_thy true);

end;