src/Pure/Isar/skip_proof.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 20049 f48c4a3a34bc
permissions -rw-r--r--
simplified type attribute;
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
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     4
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
     5
Skipping proofs -- quick_and_dirty mode.
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     6
*)
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
signature SKIP_PROOF =
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     9
sig
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    10
  val make_thm: theory -> term -> thm
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    11
  val cheat_tac: theory -> tactic
11972
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    12
  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    13
end;
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    14
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    15
structure SkipProof: SKIP_PROOF =
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    16
struct
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    17
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    18
(* oracle setup *)
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    19
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    20
exception SkipProof of term;
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    21
17362
c089fa02c1e5 load before proof.ML;
wenzelm
parents: 17114
diff changeset
    22
fun skip_proof (_, SkipProof prop) =
c089fa02c1e5 load before proof.ML;
wenzelm
parents: 17114
diff changeset
    23
  if ! quick_and_dirty then prop
12318
72348ff7d4a0 skip_proof: do not require quick_and_dirty in interactive mode;
wenzelm
parents: 12244
diff changeset
    24
  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
    25
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17956
diff changeset
    26
val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    27
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    28
11972
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    29
(* basic cheating *)
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    30
17362
c089fa02c1e5 load before proof.ML;
wenzelm
parents: 17114
diff changeset
    31
fun make_thm thy prop =
c089fa02c1e5 load before proof.ML;
wenzelm
parents: 17114
diff changeset
    32
  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    33
8539
3cbe48a112f7 added prove_goalw_cterm;
wenzelm
parents: 6984
diff changeset
    34
fun cheat_tac thy st =
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    35
  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
    36
11972
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    37
fun prove thy xs asms prop tac =
17956
369e2af8ee45 Goal.prove;
wenzelm
parents: 17476
diff changeset
    38
  Goal.prove thy xs asms prop
11972
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    39
    (if ! quick_and_dirty then (K (cheat_tac thy)) else tac);
15da572c3c27 added prove;
wenzelm
parents: 11892
diff changeset
    40
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    41
end;