src/Pure/Isar/skip_proof.ML
author wenzelm
Wed, 28 Nov 2001 23:31:47 +0100
changeset 12318 72348ff7d4a0
parent 12244 179f142ffb03
child 14981 e73f8140af78
permissions -rw-r--r--
skip_proof: do not require quick_and_dirty in interactive mode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/skip_proof.ML
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
8807
wenzelm
parents: 8539
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     5
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
     6
Skipping proofs -- quick_and_dirty mode.
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     7
*)
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     8
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     9
signature SKIP_PROOF =
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    10
sig
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    11
  val quick_and_dirty: bool ref
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    12
  val make_thm: theory -> term -> thm
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    13
  val cheat_tac: theory -> tactic
11972
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    14
  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
12148
a57873aec3bf adapted to multiple results;
wenzelm
parents: 12055
diff changeset
    15
  val local_skip_proof: (Proof.context -> string * (string * thm list) list -> unit) *
12318
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    16
    (Proof.context -> thm -> unit) -> bool -> Proof.state -> Proof.state Seq.seq
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    17
  val global_skip_proof:
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    18
    bool -> Proof.state -> theory * ((string * string) * (string * thm list) list)
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    19
  val setup: (theory -> theory) list
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    20
end;
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    21
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    22
structure SkipProof: SKIP_PROOF =
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    23
struct
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    24
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    25
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    26
(* quick_and_dirty *)
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    27
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    28
(*if true then some packages will OMIT SOME PROOFS*)
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    29
val quick_and_dirty = ref false;
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    30
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    31
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    32
(* oracle setup *)
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    33
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    34
val skip_proofN = "skip_proof";
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    35
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    36
exception SkipProof of term;
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    37
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    38
fun skip_proof (_, SkipProof t) =
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    39
  if ! quick_and_dirty then t
12318
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    40
  else error "Proof may be skipped in quick_and_dirty mode only!";
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    41
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    42
val setup = [Theory.add_oracle (skip_proofN, skip_proof)];
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    43
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    44
11972
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    45
(* basic cheating *)
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    46
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    47
fun make_thm thy t =
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    48
  (*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*)
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    49
  Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof t);
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    50
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    51
fun cheat_tac thy st =
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    52
  ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    53
11972
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    54
fun prove thy xs asms prop tac =
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    55
  Tactic.prove (Theory.sign_of thy) xs asms prop
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    56
    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    57
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    58
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    59
(* "sorry" proof command *)
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    60
12318
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    61
fun cheating int ctxt = Method.METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    62
    (cheat_tac (ProofContext.theory_of ctxt))));
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    63
12318
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    64
fun local_skip_proof x int = Method.local_terminal_proof (Method.Basic (cheating int), None) x;
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    65
fun global_skip_proof int = Method.global_terminal_proof (Method.Basic (cheating int), None);
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    66
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    67
end;
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    68
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    69
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    70
val quick_and_dirty = SkipProof.quick_and_dirty;