added prove_goalw_cterm;
authorwenzelm
Mon Mar 20 18:48:12 2000 +0100 (2000-03-20 ago)
changeset 85393cbe48a112f7
parent 8538 e8ab6cd2e908
child 8540 3a45bc1ff175
added prove_goalw_cterm;
quick_and_dirty moved here;
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Mon Mar 20 18:47:47 2000 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon Mar 20 18:48:12 2000 +0100
     1.3 @@ -2,14 +2,16 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Skip subproofs (for quick_and_dirty mode only).
     1.8 +Skipping proofs -- quick_and_dirty mode.
     1.9  *)
    1.10  
    1.11  signature SKIP_PROOF =
    1.12  sig
    1.13 +  val quick_and_dirty: bool ref
    1.14    val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.15      -> Proof.state -> Proof.state Seq.seq
    1.16    val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.17 +  val prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm
    1.18    val setup: (theory -> theory) list
    1.19  end;
    1.20  
    1.21 @@ -17,7 +19,13 @@
    1.22  struct
    1.23  
    1.24  
    1.25 -(* oracle *)
    1.26 +(* quick_and_dirty *)
    1.27 +
    1.28 +(*if true then some packages will OMIT SOME PROOFS*)
    1.29 +val quick_and_dirty = ref false;
    1.30 +
    1.31 +
    1.32 +(* cheat_tac *)
    1.33  
    1.34  val skip_proofN = "skip_proof";
    1.35  
    1.36 @@ -29,20 +37,24 @@
    1.37    else error "Proofs may be skipped in quick_and_dirty mode only!";
    1.38  
    1.39  
    1.40 -(* proof command *)
    1.41 -
    1.42 -fun cheat_meth ctxt =
    1.43 -  let
    1.44 -    val thy = ProofContext.theory_of ctxt;
    1.45 -    (*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
    1.46 -    val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof);
    1.47 -  in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end;
    1.48 -
    1.49 -val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth, None);
    1.50 -val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth, None);
    1.51 +(*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
    1.52 +fun cheat_tac thy st =
    1.53 +  ALLGOALS (Tactic.rtac (Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof))) st;
    1.54  
    1.55  
    1.56 -(* proof command *)
    1.57 +(* "sorry" proof command *)
    1.58 +
    1.59 +fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt)));
    1.60 +
    1.61 +val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None);
    1.62 +val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None);
    1.63 +
    1.64 +
    1.65 +(* conditional prove_goalw_cterm *)
    1.66 +
    1.67 +fun prove_goalw_cterm thy rews ct tacs =
    1.68 +  Goals.prove_goalw_cterm rews ct
    1.69 +    (if ! quick_and_dirty then (K [cheat_tac thy]) else tacs);
    1.70  
    1.71  
    1.72  (* theory setup *)
    1.73 @@ -51,3 +63,6 @@
    1.74  
    1.75  
    1.76  end;
    1.77 +
    1.78 +
    1.79 +val quick_and_dirty = SkipProof.quick_and_dirty;