author  wenzelm 
Wed, 28 Nov 2001 23:31:47 +0100  
changeset 12318  72348ff7d4a0 
parent 12244  179f142ffb03 
child 14981  e73f8140af78 
permissions  rwrr 
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  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  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  11 
val quick_and_dirty: bool ref 
11892  12 
val make_thm: theory > term > thm 
13 
val cheat_tac: theory > tactic 

11972  14 
val prove: theory > string list > term list > term > (thm list > tactic) > thm 
12148  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  26 
(* quick_and_dirty *) 
27 

28 
(*if true then some packages will OMIT SOME PROOFS*) 

29 
val quick_and_dirty = ref false; 

30 

31 

11892  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  36 
exception SkipProof of term; 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

37 

11892  38 
fun skip_proof (_, SkipProof t) = 
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  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  44 

11972  45 
(* basic cheating *) 
11892  46 

47 
fun make_thm thy t = 

48 
(*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*) 

49 
Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof t); 

50 

8539  51 
fun cheat_tac thy st = 
11892  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  54 
fun prove thy xs asms prop tac = 
55 
Tactic.prove (Theory.sign_of thy) xs asms prop 

56 
(if ! quick_and_dirty then (K (cheat_tac thy)) else tac); 

57 

6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

58 

8539  59 
(* "sorry" proof command *) 
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  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  66 

6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

67 
end; 
8539  68 

69 

70 
val quick_and_dirty = SkipProof.quick_and_dirty; 