1 (* Title: HOLCF/holcfb.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for Holcfb.thy |
|
7 *) |
|
8 |
|
9 open Holcfb; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* <::nat=>nat=>bool is well-founded *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 val well_founded_nat = prove_goal Nat.thy |
|
16 "!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))" |
|
17 (fn prems => |
|
18 [ |
|
19 (res_inst_tac [("n","x")] less_induct 1), |
|
20 (strip_tac 1), |
|
21 (res_inst_tac [("Q","? k.k<n & P(k)")] (excluded_middle RS disjE) 1), |
|
22 (etac exE 2), |
|
23 (etac conjE 2), |
|
24 (rtac mp 2), |
|
25 (etac allE 2), |
|
26 (etac impE 2), |
|
27 (atac 2), |
|
28 (etac spec 2), |
|
29 (atac 2), |
|
30 (res_inst_tac [("x","n")] exI 1), |
|
31 (rtac conjI 1), |
|
32 (atac 1), |
|
33 (strip_tac 1), |
|
34 (rtac leI 1), |
|
35 (fast_tac HOL_cs 1) |
|
36 ]); |
|
37 |
|
38 |
|
39 (* ------------------------------------------------------------------------ *) |
|
40 (* Lemmas for selecting the least element in a nonempty set *) |
|
41 (* ------------------------------------------------------------------------ *) |
|
42 |
|
43 val theleast = prove_goalw Holcfb.thy [theleast_def] |
|
44 "P(x) ==> P(theleast(P)) & (!x.P(x)--> theleast(P) <= x)" |
|
45 (fn prems => |
|
46 [ |
|
47 (cut_facts_tac prems 1), |
|
48 (rtac (well_founded_nat RS spec RS mp RS exE) 1), |
|
49 (atac 1), |
|
50 (rtac selectI 1), |
|
51 (atac 1) |
|
52 ]); |
|
53 |
|
54 val theleast1= theleast RS conjunct1; |
|
55 (* ?P1(?x1) ==> ?P1(theleast(?P1)) *) |
|
56 |
|
57 val theleast2 = prove_goal Holcfb.thy "P(x) ==> theleast(P) <= x" |
|
58 (fn prems => |
|
59 [ |
|
60 (rtac (theleast RS conjunct2 RS spec RS mp) 1), |
|
61 (resolve_tac prems 1), |
|
62 (resolve_tac prems 1) |
|
63 ]); |
|
64 |
|
65 |
|
66 (* ------------------------------------------------------------------------ *) |
|
67 (* Some lemmas in HOL.thy *) |
|
68 (* ------------------------------------------------------------------------ *) |
|
69 |
|
70 |
|
71 val de_morgan1 = prove_goal HOL.thy "(~a & ~b)=(~(a | b))" |
|
72 (fn prems => |
|
73 [ |
|
74 (rtac iffI 1), |
|
75 (fast_tac HOL_cs 1), |
|
76 (fast_tac HOL_cs 1) |
|
77 ]); |
|
78 |
|
79 val de_morgan2 = prove_goal HOL.thy "(~a | ~b)=(~(a & b))" |
|
80 (fn prems => |
|
81 [ |
|
82 (rtac iffI 1), |
|
83 (fast_tac HOL_cs 1), |
|
84 (fast_tac HOL_cs 1) |
|
85 ]); |
|
86 |
|
87 |
|
88 val notall2ex = prove_goal HOL.thy "(~ (!x.P(x))) = (? x.~P(x))" |
|
89 (fn prems => |
|
90 [ |
|
91 (rtac iffI 1), |
|
92 (fast_tac HOL_cs 1), |
|
93 (fast_tac HOL_cs 1) |
|
94 ]); |
|
95 |
|
96 val notex2all = prove_goal HOL.thy "(~ (? x.P(x))) = (!x.~P(x))" |
|
97 (fn prems => |
|
98 [ |
|
99 (rtac iffI 1), |
|
100 (fast_tac HOL_cs 1), |
|
101 (fast_tac HOL_cs 1) |
|
102 ]); |
|
103 |
|
104 |
|
105 val selectI2 = prove_goal HOL.thy "(? x. P(x)) ==> P(@ x.P(x))" |
|
106 (fn prems => |
|
107 [ |
|
108 (cut_facts_tac prems 1), |
|
109 (etac exE 1), |
|
110 (etac selectI 1) |
|
111 ]); |
|
112 |
|
113 val selectE = prove_goal HOL.thy "P(@ x.P(x)) ==> (? x. P(x))" |
|
114 (fn prems => |
|
115 [ |
|
116 (cut_facts_tac prems 1), |
|
117 (etac exI 1) |
|
118 ]); |
|
119 |
|
120 val select_eq_Ex = prove_goal HOL.thy "(P(@ x.P(x))) = (? x. P(x))" |
|
121 (fn prems => |
|
122 [ |
|
123 (rtac (iff RS mp RS mp) 1), |
|
124 (strip_tac 1), |
|
125 (etac selectE 1), |
|
126 (strip_tac 1), |
|
127 (etac selectI2 1) |
|
128 ]); |
|
129 |
|
130 |
|
131 val notnotI = prove_goal HOL.thy "P ==> ~~P" |
|
132 (fn prems => |
|
133 [ |
|
134 (cut_facts_tac prems 1), |
|
135 (fast_tac HOL_cs 1) |
|
136 ]); |
|
137 |
|
138 |
|
139 val classical2 = prove_goal HOL.thy "[|Q ==> R; ~Q ==> R|]==>R" |
|
140 (fn prems => |
|
141 [ |
|
142 (rtac disjE 1), |
|
143 (rtac excluded_middle 1), |
|
144 (eresolve_tac prems 1), |
|
145 (eresolve_tac prems 1) |
|
146 ]); |
|
147 |
|
148 |
|
149 |
|
150 val classical3 = (notE RS notI); |
|
151 (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *) |
|
152 |
|