author  wenzelm 
Sat, 27 Oct 2001 23:19:55 +0200  
changeset 11972  15da572c3c27 
parent 11892  4a8834757140 
child 12055  a9c44895cc8c 
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 
6984  15 
val local_skip_proof: ({kind: string, name: string, thm: thm} > unit) * (thm > unit) 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

16 
> Proof.state > Proof.state Seq.seq 
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

17 
val global_skip_proof: Proof.state > theory * {kind: string, name: string, thm: thm} 
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

18 
val setup: (theory > theory) list 
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

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

20 

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

21 
structure SkipProof: SKIP_PROOF = 
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

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

23 

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

24 

8539  25 
(* quick_and_dirty *) 
26 

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

28 
val quick_and_dirty = ref false; 

29 

30 

11892  31 
(* oracle setup *) 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

32 

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

33 
val skip_proofN = "skip_proof"; 
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

34 

11892  35 
exception SkipProof of term; 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

36 

11892  37 
fun skip_proof (_, SkipProof t) = 
38 
if ! quick_and_dirty then t 

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

39 
else error "Proofs may be skipped in quick_and_dirty mode only!"; 
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff
changeset

40 

11892  41 
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

42 

11892  43 

11972  44 
(* basic cheating *) 
11892  45 

46 
fun make_thm thy t = 

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

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

49 

8539  50 
fun cheat_tac thy st = 
11892  51 
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

52 

11972  53 
fun prove thy xs asms prop tac = 
54 
Tactic.prove (Theory.sign_of thy) xs asms prop 

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

56 

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

57 

8539  58 
(* "sorry" proof command *) 
59 

60 
fun cheating ctxt = Method.METHOD (K (cheat_tac (ProofContext.theory_of ctxt))); 

61 

62 
val local_skip_proof = Method.local_terminal_proof (Method.Basic cheating, None); 

63 
val global_skip_proof = Method.global_terminal_proof (Method.Basic cheating, None); 

64 

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

65 
end; 
8539  66 

67 

68 
val quick_and_dirty = SkipProof.quick_and_dirty; 