moved prove_goalw_cterm to goals.ML;
authorwenzelm
Mon Oct 22 18:03:49 2001 +0200 (2001-10-22 ago)
changeset 118924a8834757140
parent 11891 99569e5f0ab5
child 11893 6b9e8820d4de
moved prove_goalw_cterm to goals.ML;
cleaned up;
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Mon Oct 22 18:03:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon Oct 22 18:03:49 2001 +0200
     1.3 @@ -9,11 +9,11 @@
     1.4  signature SKIP_PROOF =
     1.5  sig
     1.6    val quick_and_dirty: bool ref
     1.7 +  val make_thm: theory -> term -> thm
     1.8 +  val cheat_tac: theory -> tactic
     1.9    val local_skip_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.10      -> Proof.state -> Proof.state Seq.seq
    1.11    val global_skip_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.12 -  val prove_goalw_cterm: theory -> thm list -> cterm -> (thm list -> tactic list) -> thm
    1.13 -  val make_thm: theory -> term -> thm
    1.14    val setup: (theory -> theory) list
    1.15  end;
    1.16  
    1.17 @@ -27,21 +27,27 @@
    1.18  val quick_and_dirty = ref false;
    1.19  
    1.20  
    1.21 -(* cheat_tac *)
    1.22 +(* oracle setup *)
    1.23  
    1.24  val skip_proofN = "skip_proof";
    1.25  
    1.26 -exception SkipProof;
    1.27 -val any_prop = Var (("A", 0), propT);
    1.28 +exception SkipProof of term;
    1.29  
    1.30 -fun any_thm (_, SkipProof) =
    1.31 -  if ! quick_and_dirty then any_prop
    1.32 +fun skip_proof (_, SkipProof t) =
    1.33 +  if ! quick_and_dirty then t
    1.34    else error "Proofs may be skipped in quick_and_dirty mode only!";
    1.35  
    1.36 +val setup = [Theory.add_oracle (skip_proofN, skip_proof)];
    1.37  
    1.38 -(*too bad -- dynamic scoping of the oracle, cannot even qualify the name*)
    1.39 +
    1.40 +(* make_thm and cheat_tac *)
    1.41 +
    1.42 +fun make_thm thy t =
    1.43 +  (*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*)
    1.44 +  Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof t);
    1.45 +
    1.46  fun cheat_tac thy st =
    1.47 -  ALLGOALS (Tactic.rtac (Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof))) st;
    1.48 +  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    1.49  
    1.50  
    1.51  (* "sorry" proof command *)
    1.52 @@ -51,25 +57,6 @@
    1.53  val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None);
    1.54  val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None);
    1.55  
    1.56 -
    1.57 -(* conditional prove_goalw_cterm *)
    1.58 -
    1.59 -fun prove_goalw_cterm thy rews ct tacs =
    1.60 -  Goals.prove_goalw_cterm rews ct
    1.61 -    (if ! quick_and_dirty then (K [cheat_tac thy]) else tacs);
    1.62 -
    1.63 -
    1.64 -(* make_thm *)
    1.65 -
    1.66 -fun make_thm thy t =
    1.67 -  prove_goalw_cterm thy [] (Thm.cterm_of (Theory.sign_of thy) t) (K []);
    1.68 -
    1.69 -
    1.70 -(* theory setup *)
    1.71 -
    1.72 -val setup = [Theory.add_oracle (skip_proofN, any_thm)];
    1.73 -
    1.74 -
    1.75  end;
    1.76  
    1.77