# HG changeset patch
# User wenzelm
# Date 930935072 -7200
# Node ID d0c68ebdabc54cab80a5ee05739bb4f369f1a0f0
# Parent  12b5fb35a688197c934b93bf3b93100b0739d336
skip_proof feature 'sorry' (for quick_and_dirty mode only);

diff -r 12b5fb35a688 -r d0c68ebdabc5 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Jul 02 15:05:16 1999 +0200
+++ b/src/Pure/IsaMakefile	Fri Jul 02 19:04:32 1999 +0200
@@ -34,19 +34,19 @@
   Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
   Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
   Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
-  Isar/session.ML Isar/toplevel.ML ML-Systems/mlworks.ML \
-  ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML \
-  ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
-  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \
-  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \
-  Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
-  Thy/browser_info.ML Thy/html.ML Thy/present.ML Thy/thm_database.ML \
-  Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML \
-  Thy/thy_syn.ML axclass.ML basis.ML context.ML deriv.ML display.ML \
-  drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
-  logic.ML net.ML pattern.ML pure.ML pure_thy.ML search.ML sign.ML \
-  sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML \
-  thm.ML type.ML type_infer.ML unify.ML
+  Isar/session.ML Isar/skip_proof.ML Isar/toplevel.ML \
+  ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \
+  ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \
+  Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
+  Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
+  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
+  Thy/ROOT.ML Thy/browser_info.ML Thy/html.ML Thy/present.ML \
+  Thy/thm_database.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML \
+  Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML context.ML \
+  deriv.ML display.ML drule.ML envir.ML goals.ML install_pp.ML \
+  library.ML locale.ML logic.ML net.ML pattern.ML pure.ML pure_thy.ML \
+  search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \
+  theory_data.ML thm.ML type.ML type_infer.ML unify.ML
 	@./mk
 
 
diff -r 12b5fb35a688 -r d0c68ebdabc5 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Jul 02 15:05:16 1999 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri Jul 02 19:04:32 1999 +0200
@@ -5,7 +5,7 @@
 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
 *)
 
-(*proof engine*)
+(*basic proof engine*)
 use "auto_bind.ML";
 use "proof_context.ML";
 use "proof.ML";
@@ -14,7 +14,10 @@
 use "args.ML";
 use "attrib.ML";
 use "method.ML";
+
+(*derived proof elements*)
 use "calculation.ML";
+use "skip_proof.ML";
 
 (*outer syntax*)
 use "comment.ML";
diff -r 12b5fb35a688 -r d0c68ebdabc5 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jul 02 15:05:16 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jul 02 19:04:32 1999 +0200
@@ -355,6 +355,10 @@
   OuterSyntax.command ".." "default proof" K.qed
     (Scan.succeed IsarThy.default_proof);
 
+val skip_proofP =
+  OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
+    (Scan.succeed IsarThy.skip_proof);
+
 
 (* proof steps *)
 
@@ -560,9 +564,9 @@
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
   qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
-  applyP, then_applyP, proofP, alsoP, finallyP, backP, prevP, upP,
-  topP, cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP,
-  undoP,
+  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
+  prevP, upP, topP, cannot_undoP, clear_undoP, redoP, undos_proofP,
+  kill_proofP, undoP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
diff -r 12b5fb35a688 -r d0c68ebdabc5 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Jul 02 15:05:16 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Jul 02 19:04:32 1999 +0200
@@ -121,6 +121,7 @@
   val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
   val immediate_proof: Toplevel.transition -> Toplevel.transition
   val default_proof: Toplevel.transition -> Toplevel.transition
+  val skip_proof: Toplevel.transition -> Toplevel.transition
   val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
   val also_i: (thm list * Comment.interest) option * Comment.text
@@ -331,6 +332,7 @@
 
 val local_immediate_proof = proof'' (ProofHistory.applys_close o Method.local_immediate_proof);
 val local_default_proof = proof'' (ProofHistory.applys_close o Method.local_default_proof);
+val local_skip_proof = proof'' (ProofHistory.applys_close o SkipProof.local_skip_proof);
 
 
 (* global endings *)
@@ -357,6 +359,7 @@
 val global_terminal_proof = global_result o Method.global_terminal_proof o Comment.ignore_interest;
 val global_immediate_proof = global_result Method.global_immediate_proof;
 val global_default_proof = global_result Method.global_default_proof;
+val global_skip_proof = global_result SkipProof.global_skip_proof;
 
 
 (* common endings *)
@@ -365,6 +368,7 @@
 fun terminal_proof meth = local_terminal_proof meth o global_terminal_proof meth;
 val immediate_proof = local_immediate_proof o global_immediate_proof;
 val default_proof = local_default_proof o global_default_proof;
+val skip_proof = local_skip_proof o global_skip_proof;
 
 
 (* calculational proof commands *)
diff -r 12b5fb35a688 -r d0c68ebdabc5 src/Pure/Isar/skip_proof.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/skip_proof.ML	Fri Jul 02 19:04:32 1999 +0200
@@ -0,0 +1,53 @@
+(*  Title:      Pure/Isar/skip_proof.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Skip subproofs (for quick_and_dirty mode only).
+*)
+
+signature SKIP_PROOF =
+sig
+  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val setup: (theory -> theory) list
+end;
+
+structure SkipProof: SKIP_PROOF =
+struct
+
+
+(* oracle *)
+
+val skip_proofN = "skip_proof";
+
+exception SkipProof;
+val any_prop = Var (("A", 0), propT);
+
+fun any_thm (_, SkipProof) =
+  if ! quick_and_dirty then any_prop
+  else error "Proofs may be skipped in quick_and_dirty mode only!";
+
+
+(* proof command *)
+
+fun cheat_meth ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    (*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
+    val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof);
+  in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end;
+
+val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth);
+val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth);
+
+
+(* proof command *)
+
+
+(* theory setup *)
+
+val setup = [Theory.add_oracle (skip_proofN, any_thm)];
+
+
+end;
diff -r 12b5fb35a688 -r d0c68ebdabc5 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Fri Jul 02 15:05:16 1999 +0200
+++ b/src/Pure/pure.ML	Fri Jul 02 19:04:32 1999 +0200
@@ -13,6 +13,7 @@
     Attrib.setup @
     Method.setup @
     Calculation.setup @
+    SkipProof.setup @
     AxClass.setup @
     BrowserInfo.setup @
     Isamode.setup @