author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 17480  fd19f77dcf60 
permissions  rwrr 
1464  1 
(* Title: FOLP/ex/intro.ML 
0  2 
ID: $Id$ 
1446  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Examples for the manual "Introduction to Isabelle" 

7 

8 
Derives some inference rules, illustrating the use of definitions 

9 

10 
To generate similar output to manual, execute these commands: 

11 
Pretty.setmargin 72; print_depth 0; 

12 
*) 

13 

14 

15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset

15 
(**** Some simple backward proofs ****) 
0  16 

17480  17 
goal (theory "FOLP") "?p:PP > P"; 
1446  18 
by (rtac impI 1); 
19 
by (rtac disjE 1); 

0  20 
by (assume_tac 3); 
21 
by (assume_tac 2); 

22 
by (assume_tac 1); 

23 
val mythm = result(); 

24 

17480  25 
goal (theory "FOLP") "?p:(P & Q)  R > (P  R)"; 
1446  26 
by (rtac impI 1); 
27 
by (etac disjE 1); 

28 
by (dtac conjunct1 1); 

29 
by (rtac disjI1 1); 

30 
by (rtac disjI2 2); 

0  31 
by (REPEAT (assume_tac 1)); 
32 
result(); 

33 

34 
(*Correct version, delaying use of "spec" until last*) 

17480  35 
goal (theory "FOLP") "?p:(ALL x y. P(x,y)) > (ALL z w. P(w,z))"; 
1446  36 
by (rtac impI 1); 
37 
by (rtac allI 1); 

38 
by (rtac allI 1); 

39 
by (dtac spec 1); 

40 
by (dtac spec 1); 

0  41 
by (assume_tac 1); 
42 
result(); 

43 

44 

45 
(**** Demonstration of fast_tac ****) 

46 

17480  47 
goal (theory "FOLP") "?p:(EX y. ALL x. J(y,x) <> ~J(x,x)) \ 
0  48 
\ > ~ (ALL x. EX y. ALL z. J(z,y) <> ~ J(z,x))"; 
49 
by (fast_tac FOLP_cs 1); 

50 
result(); 

51 

17480  52 
goal (theory "FOLP") "?p:ALL x. P(x,f(x)) <> \ 
0  53 
\ (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"; 
54 
by (fast_tac FOLP_cs 1); 

55 
result(); 

56 

57 

58 
(**** Derivation of conjunction elimination rule ****) 

59 

17480  60 
val [major,minor] = goal (theory "FOLP") "[ p:P&Q; !!x y.[ x:P; y:Q ] ==>f(x,y):R ] ==> ?p:R"; 
1446  61 
by (rtac minor 1); 
0  62 
by (resolve_tac [major RS conjunct1] 1); 
63 
by (resolve_tac [major RS conjunct2] 1); 

64 
prth (topthm()); 

65 
result(); 

66 

67 

68 
(**** Derived rules involving definitions ****) 

69 

70 
(** Derivation of negation introduction **) 

71 

17480  72 
val prems = goal (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P"; 
1446  73 
by (rewtac not_def); 
74 
by (rtac impI 1); 

0  75 
by (resolve_tac prems 1); 
76 
by (assume_tac 1); 

77 
result(); 

78 

17480  79 
val [major,minor] = goal (theory "FOLP") "[ p:~P; q:P ] ==> ?p:R"; 
1446  80 
by (rtac FalseE 1); 
81 
by (rtac mp 1); 

0  82 
by (resolve_tac [rewrite_rule [not_def] major] 1); 
1446  83 
by (rtac minor 1); 
0  84 
result(); 
85 

86 
(*Alternative proof of above result*) 

17480  87 
val [major,minor] = goalw (theory "FOLP") [not_def] 
0  88 
"[ p:~P; q:P ] ==> ?p:R"; 
89 
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1); 

90 
result(); 