src/Pure/Isar/isar_thy.ML
changeset 6937 d9e3e2b30bee
parent 6904 4125d6b6d8f9
child 6952 0f7e8d42902b
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Jul 08 18:36:57 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 08 18:37:54 1999 +0200
     1.3 @@ -67,42 +67,43 @@
     1.4    val with_facts_i: (thm * Proof.context attribute list) list * Comment.text
     1.5      -> ProofHistory.T -> ProofHistory.T
     1.6    val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.7 +  val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T
     1.8    val fix: (string * string option) list * Comment.text -> ProofHistory.T -> ProofHistory.T
     1.9    val fix_i: (string * typ) list * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.10    val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.11    val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    1.12 -  val theorem: (bstring * Args.src list * (string * string list)) * Comment.text
    1.13 -    -> bool -> theory -> ProofHistory.T
    1.14 -  val theorem_i: (bstring * theory attribute list * (term * term list)) * Comment.text
    1.15 -    -> bool -> theory -> ProofHistory.T
    1.16 -  val lemma: (bstring * Args.src list * (string * string list)) * Comment.text
    1.17 -    -> bool -> theory -> ProofHistory.T
    1.18 -  val lemma_i: (bstring * theory attribute list * (term * term list)) * Comment.text
    1.19 -    -> bool -> theory -> ProofHistory.T
    1.20 -  val assume: (string * Args.src list * (string * string list) list) * Comment.text
    1.21 -    -> ProofHistory.T -> ProofHistory.T
    1.22 -  val assume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
    1.23 -    -> ProofHistory.T -> ProofHistory.T
    1.24 -  val presume: (string * Args.src list * (string * string list) list) * Comment.text
    1.25 -    -> ProofHistory.T -> ProofHistory.T
    1.26 -  val presume_i: (string * Proof.context attribute list * (term * term list) list) * Comment.text
    1.27 -    -> ProofHistory.T -> ProofHistory.T
    1.28 -  val show: (string * Args.src list * (string * string list)) * Comment.text
    1.29 -    -> ProofHistory.T -> ProofHistory.T
    1.30 -  val show_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
    1.31 -    -> ProofHistory.T -> ProofHistory.T
    1.32 -  val have: (string * Args.src list * (string * string list)) * Comment.text
    1.33 -    -> ProofHistory.T -> ProofHistory.T
    1.34 -  val have_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
    1.35 -    -> ProofHistory.T -> ProofHistory.T
    1.36 -  val thus: (string * Args.src list * (string * string list)) * Comment.text
    1.37 -    -> ProofHistory.T -> ProofHistory.T
    1.38 -  val thus_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
    1.39 -    -> ProofHistory.T -> ProofHistory.T
    1.40 -  val hence: (string * Args.src list * (string * string list)) * Comment.text
    1.41 -    -> ProofHistory.T -> ProofHistory.T
    1.42 -  val hence_i: (string * Proof.context attribute list * (term * term list)) * Comment.text
    1.43 -    -> ProofHistory.T -> ProofHistory.T
    1.44 +  val theorem: (bstring * Args.src list * (string * (string list * string list)))
    1.45 +    * Comment.text -> bool -> theory -> ProofHistory.T
    1.46 +  val theorem_i: (bstring * theory attribute list * (term * (term list * term list)))
    1.47 +    * Comment.text -> bool -> theory -> ProofHistory.T
    1.48 +  val lemma: (bstring * Args.src list * (string * (string list * string list)))
    1.49 +    * Comment.text -> bool -> theory -> ProofHistory.T
    1.50 +  val lemma_i: (bstring * theory attribute list * (term * (term list * term list)))
    1.51 +    * Comment.text -> bool -> theory -> ProofHistory.T
    1.52 +  val assume: (string * Args.src list * (string * (string list * string list)) list)
    1.53 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.54 +  val assume_i: (string * Proof.context attribute list * (term * (term list * term list)) list)
    1.55 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.56 +  val presume: (string * Args.src list * (string * (string list * string list)) list)
    1.57 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.58 +  val presume_i: (string * Proof.context attribute list * (term * (term list * term list)) list)
    1.59 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.60 +  val show: (string * Args.src list * (string * (string list * string list)))
    1.61 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.62 +  val show_i: (string * Proof.context attribute list * (term * (term list * term list)))
    1.63 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.64 +  val have: (string * Args.src list * (string * (string list * string list)))
    1.65 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.66 +  val have_i: (string * Proof.context attribute list * (term * (term list * term list)))
    1.67 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.68 +  val thus: (string * Args.src list * (string * (string list * string list)))
    1.69 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.70 +  val thus_i: (string * Proof.context attribute list * (term * (term list * term list)))
    1.71 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.72 +  val hence: (string * Args.src list * (string * (string list * string list)))
    1.73 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.74 +  val hence_i: (string * Proof.context attribute list * (term * (term list * term list)))
    1.75 +    * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.76    val begin_block: ProofHistory.T -> ProofHistory.T
    1.77    val next_block: ProofHistory.T -> ProofHistory.T
    1.78    val end_block: ProofHistory.T -> ProofHistory.T
    1.79 @@ -118,7 +119,8 @@
    1.80      -> (Method.text * Comment.interest) option
    1.81      -> Toplevel.transition -> Toplevel.transition
    1.82    val qed: (Method.text * Comment.interest) option -> Toplevel.transition -> Toplevel.transition
    1.83 -  val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
    1.84 +  val terminal_proof: (Method.text * Comment.interest) * (Method.text * Comment.interest) option
    1.85 +    -> Toplevel.transition -> Toplevel.transition
    1.86    val immediate_proof: Toplevel.transition -> Toplevel.transition
    1.87    val default_proof: Toplevel.transition -> Toplevel.transition
    1.88    val skip_proof: Toplevel.transition -> Toplevel.transition
    1.89 @@ -252,6 +254,7 @@
    1.90  val with_facts_i = gen_from_facts (have_thmss_i add_thmss) o Comment.ignore;
    1.91  
    1.92  fun chain comment_ignore = ProofHistory.apply Proof.chain;
    1.93 +fun export_chain comment_ignore = ProofHistory.applys Proof.export_chain;
    1.94  
    1.95  
    1.96  (* context *)
    1.97 @@ -280,10 +283,10 @@
    1.98  val theorem_i = global_statement_i Proof.theorem_i o Comment.ignore;
    1.99  val lemma     = global_statement Proof.lemma o Comment.ignore;
   1.100  val lemma_i   = global_statement_i Proof.lemma_i o Comment.ignore;
   1.101 -val assume    = local_statement (Proof.assume assume_tac) I o Comment.ignore;
   1.102 -val assume_i  = local_statement_i (Proof.assume_i assume_tac) I o Comment.ignore;
   1.103 -val presume   = local_statement (Proof.assume (K all_tac)) I o Comment.ignore;
   1.104 -val presume_i = local_statement_i (Proof.assume_i (K all_tac)) I o Comment.ignore;
   1.105 +val assume    = local_statement Proof.assume I o Comment.ignore;
   1.106 +val assume_i  = local_statement_i Proof.assume_i I o Comment.ignore;
   1.107 +val presume   = local_statement Proof.presume I o Comment.ignore;
   1.108 +val presume_i = local_statement_i Proof.presume_i I o Comment.ignore;
   1.109  val show      = local_statement Proof.show I o Comment.ignore;
   1.110  val show_i    = local_statement_i Proof.show_i I o Comment.ignore;
   1.111  val have      = local_statement Proof.have I o Comment.ignore;
   1.112 @@ -298,7 +301,7 @@
   1.113  
   1.114  val begin_block = ProofHistory.apply Proof.begin_block;
   1.115  val next_block = ProofHistory.apply Proof.next_block;
   1.116 -val end_block = ProofHistory.apply Proof.end_block;
   1.117 +val end_block = ProofHistory.applys Proof.end_block;
   1.118  
   1.119  
   1.120  (* backward steps *)
   1.121 @@ -313,7 +316,7 @@
   1.122  (* print result *)
   1.123  
   1.124  fun pretty_result {kind, name, thm} =
   1.125 -  Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
   1.126 +  Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm_no_hyps thm];
   1.127  
   1.128  val print_result = Pretty.writeln o pretty_result;
   1.129  fun cond_print_result int res = if int then print_result res else ();
   1.130 @@ -326,8 +329,10 @@
   1.131  val local_qed =
   1.132    proof'' o (ProofHistory.applys oo Method.local_qed) o apsome Comment.ignore_interest;
   1.133  
   1.134 +fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y);
   1.135 +
   1.136  val local_terminal_proof =
   1.137 -  proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o Comment.ignore_interest;
   1.138 +  proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests;
   1.139  
   1.140  val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
   1.141  val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
   1.142 @@ -355,7 +360,7 @@
   1.143  val global_qed_with_i = global_result oo gen_global_qed_with (K I);
   1.144  val global_qed = global_qed_with (None, None);
   1.145  
   1.146 -val global_terminal_proof = global_result o Method.global_terminal_proof o Comment.ignore_interest;
   1.147 +val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
   1.148  val global_immediate_proof = global_result Method.global_immediate_proof;
   1.149  val global_default_proof = global_result Method.global_default_proof;
   1.150  val global_skip_proof = global_result SkipProof.global_skip_proof;
   1.151 @@ -364,7 +369,7 @@
   1.152  (* common endings *)
   1.153  
   1.154  fun qed meth = local_qed meth o global_qed meth;
   1.155 -fun terminal_proof meth = local_terminal_proof meth o global_terminal_proof meth;
   1.156 +fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
   1.157  val immediate_proof = local_immediate_proof o global_immediate_proof;
   1.158  val default_proof = local_default_proof o global_default_proof;
   1.159  val skip_proof = local_skip_proof o global_skip_proof;
   1.160 @@ -375,7 +380,7 @@
   1.161  local
   1.162  
   1.163  fun cond_print_calc int thm =
   1.164 -  if int then Pretty.writeln (Pretty.big_list "calculation:" [Display.pretty_thm thm])
   1.165 +  if int then Pretty.writeln (Pretty.big_list "calculation:" [Display.pretty_thm_no_hyps thm])
   1.166    else ();
   1.167  
   1.168  fun proof''' f = Toplevel.proof' (f o cond_print_calc);