src/Pure/Isar/isar_thy.ML
changeset 6404 2daaf2943c79
parent 6371 8469852acbc0
child 6483 3e5d450c2b31
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Mar 18 16:44:53 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Mar 19 11:24:00 1999 +0100
     1.3 @@ -61,20 +61,18 @@
     1.4    val begin_block: ProofHistory.T -> ProofHistory.T
     1.5    val next_block: ProofHistory.T -> ProofHistory.T
     1.6    val end_block: ProofHistory.T -> ProofHistory.T
     1.7 -  val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
     1.8 -  val qed_with_i: bstring option * theory attribute list option -> ProofHistory.T -> theory
     1.9 -  val qed: ProofHistory.T -> theory
    1.10 -  val kill_proof: ProofHistory.T -> theory
    1.11    val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.12 -  val tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    1.13    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
    1.14 -  val then_tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    1.15    val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
    1.16 -  val proof_i: (Proof.context -> Proof.method) option -> ProofHistory.T -> ProofHistory.T
    1.17 -  val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
    1.18 -  val terminal_proof_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T
    1.19 -  val immediate_proof: ProofHistory.T -> ProofHistory.T
    1.20 -  val default_proof: ProofHistory.T -> ProofHistory.T
    1.21 +  val kill_proof: ProofHistory.T -> theory
    1.22 +  val global_qed_with: bstring option * Args.src list option -> Method.text option
    1.23 +    -> Toplevel.transition -> Toplevel.transition
    1.24 +  val global_qed_with_i: bstring option * theory attribute list option -> Method.text option
    1.25 +    -> Toplevel.transition -> Toplevel.transition
    1.26 +  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    1.27 +  val terminal_proof: Method.text -> Toplevel.transition -> Toplevel.transition
    1.28 +  val immediate_proof: Toplevel.transition -> Toplevel.transition
    1.29 +  val default_proof: Toplevel.transition -> Toplevel.transition
    1.30    val use_mltext: string -> theory option -> theory option
    1.31    val use_mltext_theory: string -> theory -> theory
    1.32    val use_setup: string -> theory -> theory
    1.33 @@ -201,46 +199,63 @@
    1.34  val have_i = local_statement_i true Proof.have_i;
    1.35  
    1.36  
    1.37 -(* end proof *)
    1.38 -
    1.39 -fun gen_qed_with prep_att (alt_name, raw_atts) prf =
    1.40 -  let
    1.41 -    val state = ProofHistory.current prf;
    1.42 -    val thy = Proof.theory_of state;
    1.43 -    val alt_atts = apsome (map (prep_att thy)) raw_atts;
    1.44 -    val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state;
    1.45 -
    1.46 -    val prt_result = Pretty.block
    1.47 -      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
    1.48 -  in Pretty.writeln prt_result; thy end;
    1.49 -
    1.50 -val qed_with = gen_qed_with Attrib.global_attribute;
    1.51 -val qed_with_i = gen_qed_with (K I);
    1.52 -
    1.53 -val qed = qed_with (None, None);
    1.54 -
    1.55 -val kill_proof = Proof.theory_of o ProofHistory.current;
    1.56 -
    1.57 -
    1.58  (* blocks *)
    1.59  
    1.60  val begin_block = ProofHistory.apply_open Proof.begin_block;
    1.61  val next_block = ProofHistory.apply Proof.next_block;
    1.62 +val end_block = ProofHistory.apply_close Proof.end_block;
    1.63  
    1.64  
    1.65  (* backward steps *)
    1.66  
    1.67  val tac = ProofHistory.applys o Method.tac;
    1.68 -val tac_i = tac o Method.Basic;
    1.69  val then_tac = ProofHistory.applys o Method.then_tac;
    1.70 -val then_tac_i = then_tac o Method.Basic;
    1.71  val proof = ProofHistory.applys o Method.proof;
    1.72 -val proof_i = proof o apsome Method.Basic;
    1.73 -val end_block = ProofHistory.applys_close Method.end_block;
    1.74 -val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
    1.75 -val terminal_proof_i = terminal_proof o Method.Basic;
    1.76 -val immediate_proof = ProofHistory.applys_close Method.immediate_proof;
    1.77 -val default_proof = ProofHistory.applys_close Method.default_proof;
    1.78 +
    1.79 +
    1.80 +(* local endings *)
    1.81 +
    1.82 +val local_qed = Toplevel.proof o ProofHistory.applys_close o Method.local_qed;
    1.83 +val local_terminal_proof = Toplevel.proof o ProofHistory.applys_close o Method.local_terminal_proof;
    1.84 +val local_immediate_proof = Toplevel.proof (ProofHistory.applys_close Method.local_immediate_proof);
    1.85 +val local_default_proof = Toplevel.proof (ProofHistory.applys_close Method.local_default_proof);
    1.86 +
    1.87 +
    1.88 +(* global endings *)
    1.89 +
    1.90 +val kill_proof = Proof.theory_of o ProofHistory.current;
    1.91 +
    1.92 +fun global_result finish = Toplevel.proof_to_theory (fn prf =>
    1.93 +  let
    1.94 +    val state = ProofHistory.current prf;
    1.95 +    val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    1.96 +    val (thy, (kind, name, thm)) = finish state;
    1.97 +
    1.98 +    val prt_result = Pretty.block
    1.99 +      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
   1.100 +  in Pretty.writeln prt_result; thy end);
   1.101 +
   1.102 +fun gen_global_qed_with prep_att (alt_name, raw_atts) opt_text state =
   1.103 +  let
   1.104 +    val thy = Proof.theory_of state;
   1.105 +    val alt_atts = apsome (map (prep_att thy)) raw_atts;
   1.106 +  in Method.global_qed alt_name alt_atts opt_text state end;
   1.107 +
   1.108 +val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute;
   1.109 +val global_qed_with_i = global_result oo gen_global_qed_with (K I);
   1.110 +val global_qed = global_qed_with (None, None);
   1.111 +
   1.112 +val global_terminal_proof = global_result o Method.global_terminal_proof;
   1.113 +val global_immediate_proof = global_result Method.global_immediate_proof;
   1.114 +val global_default_proof = global_result Method.global_default_proof;
   1.115 +
   1.116 +
   1.117 +(* common endings *)
   1.118 +
   1.119 +fun qed opt_text = local_qed opt_text o global_qed opt_text;
   1.120 +fun terminal_proof opt_text = local_terminal_proof opt_text o global_terminal_proof opt_text;
   1.121 +val immediate_proof = local_immediate_proof o global_immediate_proof;
   1.122 +val default_proof = local_default_proof o global_default_proof;
   1.123  
   1.124  
   1.125  (* use ML text *)