skip_proof feature 'sorry' (for quick_and_dirty mode only);
authorwenzelm
Fri Jul 02 19:04:32 1999 +0200 (1999-07-02 ago)
changeset 6888d0c68ebdabc5
parent 6887 12b5fb35a688
child 6889 adcf91ad5add
skip_proof feature 'sorry' (for quick_and_dirty mode only);
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/skip_proof.ML
src/Pure/pure.ML
     1.1 --- a/src/Pure/IsaMakefile	Fri Jul 02 15:05:16 1999 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Fri Jul 02 19:04:32 1999 +0200
     1.3 @@ -34,19 +34,19 @@
     1.4    Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
     1.5    Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
     1.6    Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
     1.7 -  Isar/session.ML Isar/toplevel.ML ML-Systems/mlworks.ML \
     1.8 -  ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML \
     1.9 -  ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
    1.10 -  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \
    1.11 -  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \
    1.12 -  Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
    1.13 -  Thy/browser_info.ML Thy/html.ML Thy/present.ML Thy/thm_database.ML \
    1.14 -  Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML \
    1.15 -  Thy/thy_syn.ML axclass.ML basis.ML context.ML deriv.ML display.ML \
    1.16 -  drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
    1.17 -  logic.ML net.ML pattern.ML pure.ML pure_thy.ML search.ML sign.ML \
    1.18 -  sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML \
    1.19 -  thm.ML type.ML type_infer.ML unify.ML
    1.20 +  Isar/session.ML Isar/skip_proof.ML Isar/toplevel.ML \
    1.21 +  ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \
    1.22 +  ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \
    1.23 +  Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
    1.24 +  Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
    1.25 +  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
    1.26 +  Thy/ROOT.ML Thy/browser_info.ML Thy/html.ML Thy/present.ML \
    1.27 +  Thy/thm_database.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML \
    1.28 +  Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML context.ML \
    1.29 +  deriv.ML display.ML drule.ML envir.ML goals.ML install_pp.ML \
    1.30 +  library.ML locale.ML logic.ML net.ML pattern.ML pure.ML pure_thy.ML \
    1.31 +  search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \
    1.32 +  theory_data.ML thm.ML type.ML type_infer.ML unify.ML
    1.33  	@./mk
    1.34  
    1.35  
     2.1 --- a/src/Pure/Isar/ROOT.ML	Fri Jul 02 15:05:16 1999 +0200
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Jul 02 19:04:32 1999 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
     2.5  *)
     2.6  
     2.7 -(*proof engine*)
     2.8 +(*basic proof engine*)
     2.9  use "auto_bind.ML";
    2.10  use "proof_context.ML";
    2.11  use "proof.ML";
    2.12 @@ -14,7 +14,10 @@
    2.13  use "args.ML";
    2.14  use "attrib.ML";
    2.15  use "method.ML";
    2.16 +
    2.17 +(*derived proof elements*)
    2.18  use "calculation.ML";
    2.19 +use "skip_proof.ML";
    2.20  
    2.21  (*outer syntax*)
    2.22  use "comment.ML";
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jul 02 15:05:16 1999 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jul 02 19:04:32 1999 +0200
     3.3 @@ -355,6 +355,10 @@
     3.4    OuterSyntax.command ".." "default proof" K.qed
     3.5      (Scan.succeed IsarThy.default_proof);
     3.6  
     3.7 +val skip_proofP =
     3.8 +  OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
     3.9 +    (Scan.succeed IsarThy.skip_proof);
    3.10 +
    3.11  
    3.12  (* proof steps *)
    3.13  
    3.14 @@ -560,9 +564,9 @@
    3.15    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
    3.16    fixP, letP, thenP, fromP, withP, noteP, beginP, endP, nextP,
    3.17    qed_withP, qedP, terminal_proofP, immediate_proofP, default_proofP,
    3.18 -  applyP, then_applyP, proofP, alsoP, finallyP, backP, prevP, upP,
    3.19 -  topP, cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP,
    3.20 -  undoP,
    3.21 +  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
    3.22 +  prevP, upP, topP, cannot_undoP, clear_undoP, redoP, undos_proofP,
    3.23 +  kill_proofP, undoP,
    3.24    (*diagnostic commands*)
    3.25    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    3.26    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
     4.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jul 02 15:05:16 1999 +0200
     4.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Jul 02 19:04:32 1999 +0200
     4.3 @@ -121,6 +121,7 @@
     4.4    val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
     4.5    val immediate_proof: Toplevel.transition -> Toplevel.transition
     4.6    val default_proof: Toplevel.transition -> Toplevel.transition
     4.7 +  val skip_proof: Toplevel.transition -> Toplevel.transition
     4.8    val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
     4.9      -> Toplevel.transition -> Toplevel.transition
    4.10    val also_i: (thm list * Comment.interest) option * Comment.text
    4.11 @@ -331,6 +332,7 @@
    4.12  
    4.13  val local_immediate_proof = proof'' (ProofHistory.applys_close o Method.local_immediate_proof);
    4.14  val local_default_proof = proof'' (ProofHistory.applys_close o Method.local_default_proof);
    4.15 +val local_skip_proof = proof'' (ProofHistory.applys_close o SkipProof.local_skip_proof);
    4.16  
    4.17  
    4.18  (* global endings *)
    4.19 @@ -357,6 +359,7 @@
    4.20  val global_terminal_proof = global_result o Method.global_terminal_proof o Comment.ignore_interest;
    4.21  val global_immediate_proof = global_result Method.global_immediate_proof;
    4.22  val global_default_proof = global_result Method.global_default_proof;
    4.23 +val global_skip_proof = global_result SkipProof.global_skip_proof;
    4.24  
    4.25  
    4.26  (* common endings *)
    4.27 @@ -365,6 +368,7 @@
    4.28  fun terminal_proof meth = local_terminal_proof meth o global_terminal_proof meth;
    4.29  val immediate_proof = local_immediate_proof o global_immediate_proof;
    4.30  val default_proof = local_default_proof o global_default_proof;
    4.31 +val skip_proof = local_skip_proof o global_skip_proof;
    4.32  
    4.33  
    4.34  (* calculational proof commands *)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/Isar/skip_proof.ML	Fri Jul 02 19:04:32 1999 +0200
     5.3 @@ -0,0 +1,53 @@
     5.4 +(*  Title:      Pure/Isar/skip_proof.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Markus Wenzel, TU Muenchen
     5.7 +
     5.8 +Skip subproofs (for quick_and_dirty mode only).
     5.9 +*)
    5.10 +
    5.11 +signature SKIP_PROOF =
    5.12 +sig
    5.13 +  val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit)
    5.14 +    -> Proof.state -> Proof.state Seq.seq
    5.15 +  val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    5.16 +  val setup: (theory -> theory) list
    5.17 +end;
    5.18 +
    5.19 +structure SkipProof: SKIP_PROOF =
    5.20 +struct
    5.21 +
    5.22 +
    5.23 +(* oracle *)
    5.24 +
    5.25 +val skip_proofN = "skip_proof";
    5.26 +
    5.27 +exception SkipProof;
    5.28 +val any_prop = Var (("A", 0), propT);
    5.29 +
    5.30 +fun any_thm (_, SkipProof) =
    5.31 +  if ! quick_and_dirty then any_prop
    5.32 +  else error "Proofs may be skipped in quick_and_dirty mode only!";
    5.33 +
    5.34 +
    5.35 +(* proof command *)
    5.36 +
    5.37 +fun cheat_meth ctxt =
    5.38 +  let
    5.39 +    val thy = ProofContext.theory_of ctxt;
    5.40 +    (*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
    5.41 +    val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof);
    5.42 +  in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end;
    5.43 +
    5.44 +val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth);
    5.45 +val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth);
    5.46 +
    5.47 +
    5.48 +(* proof command *)
    5.49 +
    5.50 +
    5.51 +(* theory setup *)
    5.52 +
    5.53 +val setup = [Theory.add_oracle (skip_proofN, any_thm)];
    5.54 +
    5.55 +
    5.56 +end;
     6.1 --- a/src/Pure/pure.ML	Fri Jul 02 15:05:16 1999 +0200
     6.2 +++ b/src/Pure/pure.ML	Fri Jul 02 19:04:32 1999 +0200
     6.3 @@ -13,6 +13,7 @@
     6.4      Attrib.setup @
     6.5      Method.setup @
     6.6      Calculation.setup @
     6.7 +    SkipProof.setup @
     6.8      AxClass.setup @
     6.9      BrowserInfo.setup @
    6.10      Isamode.setup @