|
1 (**** HOL examples -- process using Doc/tout HOL-eg.txt ****) |
|
2 |
|
3 Pretty.setmargin 72; (*existing macros just allow this margin*) |
|
4 print_depth 0; |
|
5 |
|
6 |
|
7 (*** Conjunction rules ***) |
|
8 |
|
9 val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q"; |
|
10 by (resolve_tac [and_def RS ssubst] 1); |
|
11 by (resolve_tac [allI] 1); |
|
12 by (resolve_tac [impI] 1); |
|
13 by (eresolve_tac [mp RS mp] 1); |
|
14 by (REPEAT (resolve_tac prems 1)); |
|
15 val conjI = result(); |
|
16 |
|
17 val prems = goal HOL_Rule.thy "[| P & Q |] ==> P"; |
|
18 prths (prems RL [and_def RS subst]); |
|
19 prths (prems RL [and_def RS subst] RL [spec] RL [mp]); |
|
20 by (resolve_tac it 1); |
|
21 by (REPEAT (ares_tac [impI] 1)); |
|
22 val conjunct1 = result(); |
|
23 |
|
24 |
|
25 (*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
|
26 |
|
27 goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; |
|
28 by (resolve_tac [notI] 1); |
|
29 by (eresolve_tac [rangeE] 1); |
|
30 by (eresolve_tac [equalityCE] 1); |
|
31 by (dresolve_tac [CollectD] 1); |
|
32 by (contr_tac 1); |
|
33 by (swap_res_tac [CollectI] 1); |
|
34 by (assume_tac 1); |
|
35 |
|
36 choplev 0; |
|
37 by (best_tac (set_cs addSEs [equalityCE]) 1); |
|
38 |
|
39 |
|
40 goal Set.thy "! f:: 'a=>'a set. ! x. ~ f(x) = ?S(f)"; |
|
41 by (REPEAT (resolve_tac [allI,notI] 1)); |
|
42 by (eresolve_tac [equalityCE] 1); |
|
43 by (dresolve_tac [CollectD] 1); |
|
44 by (contr_tac 1); |
|
45 by (swap_res_tac [CollectI] 1); |
|
46 by (assume_tac 1); |
|
47 |
|
48 choplev 0; |
|
49 by (best_tac (set_cs addSEs [equalityCE]) 1); |
|
50 |
|
51 |
|
52 goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? a. f(a) = S)"; |
|
53 by (best_tac (set_cs addSEs [equalityCE]) 1); |
|
54 |
|
55 |
|
56 |
|
57 |
|
58 > val prems = goal HOL_Rule.thy "[| P; Q |] ==> P&Q"; |
|
59 Level 0 |
|
60 P & Q |
|
61 1. P & Q |
|
62 > by (resolve_tac [and_def RS ssubst] 1); |
|
63 Level 1 |
|
64 P & Q |
|
65 1. ! R. (P --> Q --> R) --> R |
|
66 > by (resolve_tac [allI] 1); |
|
67 Level 2 |
|
68 P & Q |
|
69 1. !!R. (P --> Q --> R) --> R |
|
70 > by (resolve_tac [impI] 1); |
|
71 Level 3 |
|
72 P & Q |
|
73 1. !!R. P --> Q --> R ==> R |
|
74 > by (eresolve_tac [mp RS mp] 1); |
|
75 Level 4 |
|
76 P & Q |
|
77 1. !!R. P |
|
78 2. !!R. Q |
|
79 > by (REPEAT (resolve_tac prems 1)); |
|
80 Level 5 |
|
81 P & Q |
|
82 No subgoals! |
|
83 |
|
84 |
|
85 |
|
86 > val prems = goal HOL_Rule.thy "[| P & Q |] ==> P"; |
|
87 Level 0 |
|
88 P |
|
89 1. P |
|
90 > prths (prems RL [and_def RS subst]); |
|
91 ! R. (P --> Q --> R) --> R [P & Q] |
|
92 P & Q [P & Q] |
|
93 |
|
94 > prths (prems RL [and_def RS subst] RL [spec] RL [mp]); |
|
95 P --> Q --> ?Q ==> ?Q [P & Q] |
|
96 |
|
97 > by (resolve_tac it 1); |
|
98 Level 1 |
|
99 P |
|
100 1. P --> Q --> P |
|
101 > by (REPEAT (ares_tac [impI] 1)); |
|
102 Level 2 |
|
103 P |
|
104 No subgoals! |
|
105 |
|
106 |
|
107 |
|
108 |
|
109 > goal Set.thy "~ ?S : range(f :: 'a=>'a set)"; |
|
110 Level 0 |
|
111 ~?S : range(f) |
|
112 1. ~?S : range(f) |
|
113 > by (resolve_tac [notI] 1); |
|
114 Level 1 |
|
115 ~?S : range(f) |
|
116 1. ?S : range(f) ==> False |
|
117 > by (eresolve_tac [rangeE] 1); |
|
118 Level 2 |
|
119 ~?S : range(f) |
|
120 1. !!x. ?S = f(x) ==> False |
|
121 > by (eresolve_tac [equalityCE] 1); |
|
122 Level 3 |
|
123 ~?S : range(f) |
|
124 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False |
|
125 2. !!x. [| ~?c3(x) : ?S; ~?c3(x) : f(x) |] ==> False |
|
126 > by (dresolve_tac [CollectD] 1); |
|
127 Level 4 |
|
128 ~{x. ?P7(x)} : range(f) |
|
129 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False |
|
130 2. !!x. [| ~?c3(x) : {x. ?P7(x)}; ~?c3(x) : f(x) |] ==> False |
|
131 > by (contr_tac 1); |
|
132 Level 5 |
|
133 ~{x. ~x : f(x)} : range(f) |
|
134 1. !!x. [| ~x : {x. ~x : f(x)}; ~x : f(x) |] ==> False |
|
135 > by (swap_res_tac [CollectI] 1); |
|
136 Level 6 |
|
137 ~{x. ~x : f(x)} : range(f) |
|
138 1. !!x. [| ~x : f(x); ~False |] ==> ~x : f(x) |
|
139 > by (assume_tac 1); |
|
140 Level 7 |
|
141 ~{x. ~x : f(x)} : range(f) |
|
142 No subgoals! |
|
143 |
|
144 > choplev 0; |
|
145 Level 0 |
|
146 ~?S : range(f) |
|
147 1. ~?S : range(f) |
|
148 > by (best_tac (set_cs addSEs [equalityCE]) 1); |
|
149 Level 1 |
|
150 ~{x. ~x : f(x)} : range(f) |
|
151 No subgoals! |