clasohm@1477
|
1 |
(* Title: FOLP/IFOLP.thy
|
clasohm@1477
|
2 |
Author: Martin D Coen, Cambridge University Computer Laboratory
|
lcp@1142
|
3 |
Copyright 1992 University of Cambridge
|
lcp@1142
|
4 |
*)
|
lcp@1142
|
5 |
|
wenzelm@17480
|
6 |
header {* Intuitionistic First-Order Logic with Proofs *}
|
wenzelm@17480
|
7 |
|
wenzelm@17480
|
8 |
theory IFOLP
|
wenzelm@17480
|
9 |
imports Pure
|
wenzelm@17480
|
10 |
begin
|
clasohm@0
|
11 |
|
wenzelm@49906
|
12 |
ML_file "~~/src/Tools/misc_legacy.ML"
|
wenzelm@49906
|
13 |
|
wenzelm@39814
|
14 |
setup Pure_Thy.old_appl_syntax_setup
|
wenzelm@26956
|
15 |
|
wenzelm@17480
|
16 |
classes "term"
|
wenzelm@36452
|
17 |
default_sort "term"
|
clasohm@0
|
18 |
|
wenzelm@17480
|
19 |
typedecl p
|
wenzelm@17480
|
20 |
typedecl o
|
clasohm@0
|
21 |
|
wenzelm@17480
|
22 |
consts
|
clasohm@0
|
23 |
(*** Judgements ***)
|
clasohm@1477
|
24 |
Proof :: "[o,p]=>prop"
|
clasohm@0
|
25 |
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)
|
wenzelm@17480
|
26 |
|
clasohm@0
|
27 |
(*** Logical Connectives -- Type Formers ***)
|
wenzelm@41558
|
28 |
eq :: "['a,'a] => o" (infixl "=" 50)
|
wenzelm@17480
|
29 |
True :: "o"
|
wenzelm@17480
|
30 |
False :: "o"
|
paulson@2714
|
31 |
Not :: "o => o" ("~ _" [40] 40)
|
wenzelm@41558
|
32 |
conj :: "[o,o] => o" (infixr "&" 35)
|
wenzelm@41558
|
33 |
disj :: "[o,o] => o" (infixr "|" 30)
|
wenzelm@41558
|
34 |
imp :: "[o,o] => o" (infixr "-->" 25)
|
wenzelm@41558
|
35 |
iff :: "[o,o] => o" (infixr "<->" 25)
|
clasohm@0
|
36 |
(*Quantifiers*)
|
clasohm@1477
|
37 |
All :: "('a => o) => o" (binder "ALL " 10)
|
clasohm@1477
|
38 |
Ex :: "('a => o) => o" (binder "EX " 10)
|
clasohm@1477
|
39 |
Ex1 :: "('a => o) => o" (binder "EX! " 10)
|
clasohm@0
|
40 |
(*Rewriting gadgets*)
|
clasohm@1477
|
41 |
NORM :: "o => o"
|
clasohm@1477
|
42 |
norm :: "'a => 'a"
|
clasohm@0
|
43 |
|
lcp@648
|
44 |
(*** Proof Term Formers: precedence must exceed 50 ***)
|
clasohm@1477
|
45 |
tt :: "p"
|
clasohm@1477
|
46 |
contr :: "p=>p"
|
wenzelm@17480
|
47 |
fst :: "p=>p"
|
wenzelm@17480
|
48 |
snd :: "p=>p"
|
clasohm@1477
|
49 |
pair :: "[p,p]=>p" ("(1<_,/_>)")
|
clasohm@1477
|
50 |
split :: "[p, [p,p]=>p] =>p"
|
wenzelm@17480
|
51 |
inl :: "p=>p"
|
wenzelm@17480
|
52 |
inr :: "p=>p"
|
clasohm@1477
|
53 |
when :: "[p, p=>p, p=>p]=>p"
|
clasohm@1477
|
54 |
lambda :: "(p => p) => p" (binder "lam " 55)
|
wenzelm@41558
|
55 |
App :: "[p,p]=>p" (infixl "`" 60)
|
lcp@648
|
56 |
alll :: "['a=>p]=>p" (binder "all " 55)
|
wenzelm@41558
|
57 |
app :: "[p,'a]=>p" (infixl "^" 55)
|
clasohm@1477
|
58 |
exists :: "['a,p]=>p" ("(1[_,/_])")
|
clasohm@0
|
59 |
xsplit :: "[p,['a,p]=>p]=>p"
|
clasohm@0
|
60 |
ideq :: "'a=>p"
|
clasohm@0
|
61 |
idpeel :: "[p,'a=>p]=>p"
|
wenzelm@17480
|
62 |
nrm :: p
|
wenzelm@17480
|
63 |
NRM :: p
|
clasohm@0
|
64 |
|
wenzelm@35116
|
65 |
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5)
|
wenzelm@35116
|
66 |
|
wenzelm@39067
|
67 |
parse_translation {*
|
wenzelm@39067
|
68 |
let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p
|
wenzelm@39067
|
69 |
in [(@{syntax_const "_Proof"}, proof_tr)] end
|
wenzelm@17480
|
70 |
*}
|
wenzelm@17480
|
71 |
|
wenzelm@39067
|
72 |
(*show_proofs = true displays the proof terms -- they are ENORMOUS*)
|
wenzelm@43487
|
73 |
ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
|
wenzelm@39067
|
74 |
|
wenzelm@39067
|
75 |
print_translation (advanced) {*
|
wenzelm@39067
|
76 |
let
|
wenzelm@39067
|
77 |
fun proof_tr' ctxt [P, p] =
|
wenzelm@39067
|
78 |
if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
|
wenzelm@39067
|
79 |
else P
|
wenzelm@39067
|
80 |
in [(@{const_syntax Proof}, proof_tr')] end
|
wenzelm@39067
|
81 |
*}
|
wenzelm@17480
|
82 |
|
clasohm@0
|
83 |
|
clasohm@0
|
84 |
(**** Propositional logic ****)
|
clasohm@0
|
85 |
|
clasohm@0
|
86 |
(*Equality*)
|
clasohm@0
|
87 |
(* Like Intensional Equality in MLTT - but proofs distinct from terms *)
|
clasohm@0
|
88 |
|
wenzelm@52443
|
89 |
axiomatization where
|
wenzelm@52443
|
90 |
ieqI: "ideq(a) : a=a" and
|
wenzelm@17480
|
91 |
ieqE: "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
|
clasohm@0
|
92 |
|
clasohm@0
|
93 |
(* Truth and Falsity *)
|
clasohm@0
|
94 |
|
wenzelm@52443
|
95 |
axiomatization where
|
wenzelm@52443
|
96 |
TrueI: "tt : True" and
|
wenzelm@17480
|
97 |
FalseE: "a:False ==> contr(a):P"
|
clasohm@0
|
98 |
|
clasohm@0
|
99 |
(* Conjunction *)
|
clasohm@0
|
100 |
|
wenzelm@52443
|
101 |
axiomatization where
|
wenzelm@52443
|
102 |
conjI: "[| a:P; b:Q |] ==> <a,b> : P&Q" and
|
wenzelm@52443
|
103 |
conjunct1: "p:P&Q ==> fst(p):P" and
|
wenzelm@17480
|
104 |
conjunct2: "p:P&Q ==> snd(p):Q"
|
clasohm@0
|
105 |
|
clasohm@0
|
106 |
(* Disjunction *)
|
clasohm@0
|
107 |
|
wenzelm@52443
|
108 |
axiomatization where
|
wenzelm@52443
|
109 |
disjI1: "a:P ==> inl(a):P|Q" and
|
wenzelm@52443
|
110 |
disjI2: "b:Q ==> inr(b):P|Q" and
|
wenzelm@17480
|
111 |
disjE: "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R
|
wenzelm@17480
|
112 |
|] ==> when(a,f,g):R"
|
clasohm@0
|
113 |
|
clasohm@0
|
114 |
(* Implication *)
|
clasohm@0
|
115 |
|
wenzelm@52443
|
116 |
axiomatization where
|
wenzelm@52443
|
117 |
impI: "\<And>P Q f. (!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q" and
|
wenzelm@52443
|
118 |
mp: "\<And>P Q f. [| f:P-->Q; a:P |] ==> f`a:Q"
|
clasohm@0
|
119 |
|
clasohm@0
|
120 |
(*Quantifiers*)
|
clasohm@0
|
121 |
|
wenzelm@52443
|
122 |
axiomatization where
|
wenzelm@52443
|
123 |
allI: "\<And>P. (!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" and
|
wenzelm@52443
|
124 |
spec: "\<And>P f. (f:ALL x. P(x)) ==> f^x : P(x)"
|
clasohm@0
|
125 |
|
wenzelm@52443
|
126 |
axiomatization where
|
wenzelm@52443
|
127 |
exI: "p : P(x) ==> [x,p] : EX x. P(x)" and
|
wenzelm@17480
|
128 |
exE: "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
|
clasohm@0
|
129 |
|
clasohm@0
|
130 |
(**** Equality between proofs ****)
|
clasohm@0
|
131 |
|
wenzelm@52443
|
132 |
axiomatization where
|
wenzelm@52443
|
133 |
prefl: "a : P ==> a = a : P" and
|
wenzelm@52443
|
134 |
psym: "a = b : P ==> b = a : P" and
|
wenzelm@17480
|
135 |
ptrans: "[| a = b : P; b = c : P |] ==> a = c : P"
|
clasohm@0
|
136 |
|
wenzelm@52443
|
137 |
axiomatization where
|
wenzelm@17480
|
138 |
idpeelB: "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
|
clasohm@0
|
139 |
|
wenzelm@52443
|
140 |
axiomatization where
|
wenzelm@52443
|
141 |
fstB: "a:P ==> fst(<a,b>) = a : P" and
|
wenzelm@52443
|
142 |
sndB: "b:Q ==> snd(<a,b>) = b : Q" and
|
wenzelm@17480
|
143 |
pairEC: "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
|
clasohm@0
|
144 |
|
wenzelm@52443
|
145 |
axiomatization where
|
wenzelm@52443
|
146 |
whenBinl: "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" and
|
wenzelm@52443
|
147 |
whenBinr: "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" and
|
wenzelm@17480
|
148 |
plusEC: "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
|
clasohm@0
|
149 |
|
wenzelm@52443
|
150 |
axiomatization where
|
wenzelm@52443
|
151 |
applyB: "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" and
|
wenzelm@17480
|
152 |
funEC: "f:P ==> f = lam x. f`x : P"
|
clasohm@0
|
153 |
|
wenzelm@52443
|
154 |
axiomatization where
|
wenzelm@17480
|
155 |
specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
|
clasohm@0
|
156 |
|
clasohm@0
|
157 |
|
clasohm@0
|
158 |
(**** Definitions ****)
|
clasohm@0
|
159 |
|
wenzelm@52443
|
160 |
defs
|
wenzelm@17480
|
161 |
not_def: "~P == P-->False"
|
wenzelm@17480
|
162 |
iff_def: "P<->Q == (P-->Q) & (Q-->P)"
|
clasohm@0
|
163 |
|
clasohm@0
|
164 |
(*Unique existence*)
|
wenzelm@17480
|
165 |
ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
|
clasohm@0
|
166 |
|
clasohm@0
|
167 |
(*Rewriting -- special constants to flag normalized terms and formulae*)
|
wenzelm@52443
|
168 |
axiomatization where
|
wenzelm@52443
|
169 |
norm_eq: "nrm : norm(x) = x" and
|
wenzelm@17480
|
170 |
NORM_iff: "NRM : NORM(P) <-> P"
|
wenzelm@17480
|
171 |
|
wenzelm@26322
|
172 |
(*** Sequent-style elimination rules for & --> and ALL ***)
|
wenzelm@26322
|
173 |
|
wenzelm@36319
|
174 |
schematic_lemma conjE:
|
wenzelm@26322
|
175 |
assumes "p:P&Q"
|
wenzelm@26322
|
176 |
and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
|
wenzelm@26322
|
177 |
shows "?a:R"
|
wenzelm@26322
|
178 |
apply (rule assms(2))
|
wenzelm@26322
|
179 |
apply (rule conjunct1 [OF assms(1)])
|
wenzelm@26322
|
180 |
apply (rule conjunct2 [OF assms(1)])
|
wenzelm@26322
|
181 |
done
|
wenzelm@26322
|
182 |
|
wenzelm@36319
|
183 |
schematic_lemma impE:
|
wenzelm@26322
|
184 |
assumes "p:P-->Q"
|
wenzelm@26322
|
185 |
and "q:P"
|
wenzelm@26322
|
186 |
and "!!x. x:Q ==> r(x):R"
|
wenzelm@26322
|
187 |
shows "?p:R"
|
wenzelm@26322
|
188 |
apply (rule assms mp)+
|
wenzelm@26322
|
189 |
done
|
wenzelm@26322
|
190 |
|
wenzelm@36319
|
191 |
schematic_lemma allE:
|
wenzelm@26322
|
192 |
assumes "p:ALL x. P(x)"
|
wenzelm@26322
|
193 |
and "!!y. y:P(x) ==> q(y):R"
|
wenzelm@26322
|
194 |
shows "?p:R"
|
wenzelm@26322
|
195 |
apply (rule assms spec)+
|
wenzelm@26322
|
196 |
done
|
wenzelm@26322
|
197 |
|
wenzelm@26322
|
198 |
(*Duplicates the quantifier; for use with eresolve_tac*)
|
wenzelm@36319
|
199 |
schematic_lemma all_dupE:
|
wenzelm@26322
|
200 |
assumes "p:ALL x. P(x)"
|
wenzelm@26322
|
201 |
and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
|
wenzelm@26322
|
202 |
shows "?p:R"
|
wenzelm@26322
|
203 |
apply (rule assms spec)+
|
wenzelm@26322
|
204 |
done
|
wenzelm@26322
|
205 |
|
wenzelm@26322
|
206 |
|
wenzelm@26322
|
207 |
(*** Negation rules, which translate between ~P and P-->False ***)
|
wenzelm@26322
|
208 |
|
wenzelm@36319
|
209 |
schematic_lemma notI:
|
wenzelm@26322
|
210 |
assumes "!!x. x:P ==> q(x):False"
|
wenzelm@26322
|
211 |
shows "?p:~P"
|
wenzelm@26322
|
212 |
unfolding not_def
|
wenzelm@26322
|
213 |
apply (assumption | rule assms impI)+
|
wenzelm@26322
|
214 |
done
|
wenzelm@26322
|
215 |
|
wenzelm@36319
|
216 |
schematic_lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
|
wenzelm@26322
|
217 |
unfolding not_def
|
wenzelm@26322
|
218 |
apply (drule (1) mp)
|
wenzelm@26322
|
219 |
apply (erule FalseE)
|
wenzelm@26322
|
220 |
done
|
wenzelm@26322
|
221 |
|
wenzelm@26322
|
222 |
(*This is useful with the special implication rules for each kind of P. *)
|
wenzelm@36319
|
223 |
schematic_lemma not_to_imp:
|
wenzelm@26322
|
224 |
assumes "p:~P"
|
wenzelm@26322
|
225 |
and "!!x. x:(P-->False) ==> q(x):Q"
|
wenzelm@26322
|
226 |
shows "?p:Q"
|
wenzelm@26322
|
227 |
apply (assumption | rule assms impI notE)+
|
wenzelm@26322
|
228 |
done
|
wenzelm@26322
|
229 |
|
wenzelm@26322
|
230 |
(* For substitution int an assumption P, reduce Q to P-->Q, substitute into
|
wenzelm@27150
|
231 |
this implication, then apply impI to move P back into the assumptions.*)
|
wenzelm@36319
|
232 |
schematic_lemma rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q"
|
wenzelm@26322
|
233 |
apply (assumption | rule mp)+
|
wenzelm@26322
|
234 |
done
|
wenzelm@26322
|
235 |
|
wenzelm@26322
|
236 |
|
wenzelm@26322
|
237 |
(*Contrapositive of an inference rule*)
|
wenzelm@36319
|
238 |
schematic_lemma contrapos:
|
wenzelm@26322
|
239 |
assumes major: "p:~Q"
|
wenzelm@26322
|
240 |
and minor: "!!y. y:P==>q(y):Q"
|
wenzelm@26322
|
241 |
shows "?a:~P"
|
wenzelm@26322
|
242 |
apply (rule major [THEN notE, THEN notI])
|
wenzelm@26322
|
243 |
apply (erule minor)
|
wenzelm@26322
|
244 |
done
|
wenzelm@26322
|
245 |
|
wenzelm@26322
|
246 |
(** Unique assumption tactic.
|
wenzelm@26322
|
247 |
Ignores proof objects.
|
wenzelm@26322
|
248 |
Fails unless one assumption is equal and exactly one is unifiable
|
wenzelm@26322
|
249 |
**)
|
wenzelm@26322
|
250 |
|
wenzelm@26322
|
251 |
ML {*
|
wenzelm@26322
|
252 |
local
|
wenzelm@26322
|
253 |
fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P;
|
wenzelm@26322
|
254 |
in
|
wenzelm@26322
|
255 |
val uniq_assume_tac =
|
wenzelm@26322
|
256 |
SUBGOAL
|
wenzelm@26322
|
257 |
(fn (prem,i) =>
|
wenzelm@26322
|
258 |
let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
|
wenzelm@26322
|
259 |
and concl = discard_proof (Logic.strip_assums_concl prem)
|
wenzelm@26322
|
260 |
in
|
wenzelm@26322
|
261 |
if exists (fn hyp => hyp aconv concl) hyps
|
wenzelm@29269
|
262 |
then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
|
wenzelm@26322
|
263 |
[_] => assume_tac i
|
wenzelm@26322
|
264 |
| _ => no_tac
|
wenzelm@26322
|
265 |
else no_tac
|
wenzelm@26322
|
266 |
end);
|
wenzelm@26322
|
267 |
end;
|
wenzelm@26322
|
268 |
*}
|
wenzelm@26322
|
269 |
|
wenzelm@26322
|
270 |
|
wenzelm@26322
|
271 |
(*** Modus Ponens Tactics ***)
|
wenzelm@26322
|
272 |
|
wenzelm@26322
|
273 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
|
wenzelm@26322
|
274 |
ML {*
|
wenzelm@26322
|
275 |
fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac i
|
wenzelm@26322
|
276 |
*}
|
wenzelm@26322
|
277 |
|
wenzelm@26322
|
278 |
(*Like mp_tac but instantiates no variables*)
|
wenzelm@26322
|
279 |
ML {*
|
wenzelm@26322
|
280 |
fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac i
|
wenzelm@26322
|
281 |
*}
|
wenzelm@26322
|
282 |
|
wenzelm@26322
|
283 |
|
wenzelm@26322
|
284 |
(*** If-and-only-if ***)
|
wenzelm@26322
|
285 |
|
wenzelm@36319
|
286 |
schematic_lemma iffI:
|
wenzelm@26322
|
287 |
assumes "!!x. x:P ==> q(x):Q"
|
wenzelm@26322
|
288 |
and "!!x. x:Q ==> r(x):P"
|
wenzelm@26322
|
289 |
shows "?p:P<->Q"
|
wenzelm@26322
|
290 |
unfolding iff_def
|
wenzelm@26322
|
291 |
apply (assumption | rule assms conjI impI)+
|
wenzelm@26322
|
292 |
done
|
wenzelm@26322
|
293 |
|
wenzelm@26322
|
294 |
|
wenzelm@26322
|
295 |
(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
|
wenzelm@26322
|
296 |
|
wenzelm@36319
|
297 |
schematic_lemma iffE:
|
wenzelm@26322
|
298 |
assumes "p:P <-> Q"
|
wenzelm@26322
|
299 |
and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
|
wenzelm@26322
|
300 |
shows "?p:R"
|
wenzelm@26322
|
301 |
apply (rule conjE)
|
wenzelm@26322
|
302 |
apply (rule assms(1) [unfolded iff_def])
|
wenzelm@26322
|
303 |
apply (rule assms(2))
|
wenzelm@26322
|
304 |
apply assumption+
|
wenzelm@26322
|
305 |
done
|
wenzelm@26322
|
306 |
|
wenzelm@26322
|
307 |
(* Destruct rules for <-> similar to Modus Ponens *)
|
wenzelm@26322
|
308 |
|
wenzelm@36319
|
309 |
schematic_lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
|
wenzelm@26322
|
310 |
unfolding iff_def
|
wenzelm@26322
|
311 |
apply (rule conjunct1 [THEN mp], assumption+)
|
wenzelm@26322
|
312 |
done
|
wenzelm@26322
|
313 |
|
wenzelm@36319
|
314 |
schematic_lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
|
wenzelm@26322
|
315 |
unfolding iff_def
|
wenzelm@26322
|
316 |
apply (rule conjunct2 [THEN mp], assumption+)
|
wenzelm@26322
|
317 |
done
|
wenzelm@26322
|
318 |
|
wenzelm@36319
|
319 |
schematic_lemma iff_refl: "?p:P <-> P"
|
wenzelm@26322
|
320 |
apply (rule iffI)
|
wenzelm@26322
|
321 |
apply assumption+
|
wenzelm@26322
|
322 |
done
|
wenzelm@26322
|
323 |
|
wenzelm@36319
|
324 |
schematic_lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
|
wenzelm@26322
|
325 |
apply (erule iffE)
|
wenzelm@26322
|
326 |
apply (rule iffI)
|
wenzelm@26322
|
327 |
apply (erule (1) mp)+
|
wenzelm@26322
|
328 |
done
|
wenzelm@26322
|
329 |
|
wenzelm@36319
|
330 |
schematic_lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
|
wenzelm@26322
|
331 |
apply (rule iffI)
|
wenzelm@26322
|
332 |
apply (assumption | erule iffE | erule (1) impE)+
|
wenzelm@26322
|
333 |
done
|
wenzelm@26322
|
334 |
|
wenzelm@26322
|
335 |
(*** Unique existence. NOTE THAT the following 2 quantifications
|
wenzelm@26322
|
336 |
EX!x such that [EX!y such that P(x,y)] (sequential)
|
wenzelm@26322
|
337 |
EX!x,y such that P(x,y) (simultaneous)
|
wenzelm@26322
|
338 |
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
|
wenzelm@26322
|
339 |
***)
|
wenzelm@26322
|
340 |
|
wenzelm@36319
|
341 |
schematic_lemma ex1I:
|
wenzelm@26322
|
342 |
assumes "p:P(a)"
|
wenzelm@26322
|
343 |
and "!!x u. u:P(x) ==> f(u) : x=a"
|
wenzelm@26322
|
344 |
shows "?p:EX! x. P(x)"
|
wenzelm@26322
|
345 |
unfolding ex1_def
|
wenzelm@26322
|
346 |
apply (assumption | rule assms exI conjI allI impI)+
|
wenzelm@26322
|
347 |
done
|
wenzelm@26322
|
348 |
|
wenzelm@36319
|
349 |
schematic_lemma ex1E:
|
wenzelm@26322
|
350 |
assumes "p:EX! x. P(x)"
|
wenzelm@26322
|
351 |
and "!!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
|
wenzelm@26322
|
352 |
shows "?a : R"
|
wenzelm@26322
|
353 |
apply (insert assms(1) [unfolded ex1_def])
|
wenzelm@26322
|
354 |
apply (erule exE conjE | assumption | rule assms(1))+
|
wenzelm@29305
|
355 |
apply (erule assms(2), assumption)
|
wenzelm@26322
|
356 |
done
|
wenzelm@26322
|
357 |
|
wenzelm@26322
|
358 |
|
wenzelm@26322
|
359 |
(*** <-> congruence rules for simplification ***)
|
wenzelm@26322
|
360 |
|
wenzelm@26322
|
361 |
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*)
|
wenzelm@26322
|
362 |
ML {*
|
wenzelm@26322
|
363 |
fun iff_tac prems i =
|
wenzelm@26322
|
364 |
resolve_tac (prems RL [@{thm iffE}]) i THEN
|
wenzelm@26322
|
365 |
REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
|
wenzelm@26322
|
366 |
*}
|
wenzelm@26322
|
367 |
|
wenzelm@36319
|
368 |
schematic_lemma conj_cong:
|
wenzelm@26322
|
369 |
assumes "p:P <-> P'"
|
wenzelm@26322
|
370 |
and "!!x. x:P' ==> q(x):Q <-> Q'"
|
wenzelm@26322
|
371 |
shows "?p:(P&Q) <-> (P'&Q')"
|
wenzelm@26322
|
372 |
apply (insert assms(1))
|
wenzelm@26322
|
373 |
apply (assumption | rule iffI conjI |
|
wenzelm@26322
|
374 |
erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
|
wenzelm@26322
|
375 |
done
|
wenzelm@26322
|
376 |
|
wenzelm@36319
|
377 |
schematic_lemma disj_cong:
|
wenzelm@26322
|
378 |
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
|
wenzelm@26322
|
379 |
apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
|
wenzelm@26322
|
380 |
done
|
wenzelm@26322
|
381 |
|
wenzelm@36319
|
382 |
schematic_lemma imp_cong:
|
wenzelm@26322
|
383 |
assumes "p:P <-> P'"
|
wenzelm@26322
|
384 |
and "!!x. x:P' ==> q(x):Q <-> Q'"
|
wenzelm@26322
|
385 |
shows "?p:(P-->Q) <-> (P'-->Q')"
|
wenzelm@26322
|
386 |
apply (insert assms(1))
|
wenzelm@26322
|
387 |
apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} |
|
wenzelm@26322
|
388 |
tactic {* iff_tac @{thms assms} 1 *})+
|
wenzelm@26322
|
389 |
done
|
wenzelm@26322
|
390 |
|
wenzelm@36319
|
391 |
schematic_lemma iff_cong:
|
wenzelm@26322
|
392 |
"[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
|
wenzelm@26322
|
393 |
apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
|
wenzelm@26322
|
394 |
done
|
wenzelm@26322
|
395 |
|
wenzelm@36319
|
396 |
schematic_lemma not_cong:
|
wenzelm@26322
|
397 |
"p:P <-> P' ==> ?p:~P <-> ~P'"
|
wenzelm@26322
|
398 |
apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
|
wenzelm@26322
|
399 |
done
|
wenzelm@26322
|
400 |
|
wenzelm@36319
|
401 |
schematic_lemma all_cong:
|
wenzelm@26322
|
402 |
assumes "!!x. f(x):P(x) <-> Q(x)"
|
wenzelm@26322
|
403 |
shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
|
wenzelm@26322
|
404 |
apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
|
wenzelm@26322
|
405 |
tactic {* iff_tac @{thms assms} 1 *})+
|
wenzelm@26322
|
406 |
done
|
wenzelm@26322
|
407 |
|
wenzelm@36319
|
408 |
schematic_lemma ex_cong:
|
wenzelm@26322
|
409 |
assumes "!!x. f(x):P(x) <-> Q(x)"
|
wenzelm@26322
|
410 |
shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
|
wenzelm@26322
|
411 |
apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
|
wenzelm@26322
|
412 |
tactic {* iff_tac @{thms assms} 1 *})+
|
wenzelm@26322
|
413 |
done
|
wenzelm@26322
|
414 |
|
wenzelm@26322
|
415 |
(*NOT PROVED
|
wenzelm@26322
|
416 |
bind_thm ("ex1_cong", prove_goal (the_context ())
|
wenzelm@26322
|
417 |
"(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
|
wenzelm@26322
|
418 |
(fn prems =>
|
wenzelm@26322
|
419 |
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
|
wenzelm@26322
|
420 |
ORELSE mp_tac 1
|
wenzelm@26322
|
421 |
ORELSE iff_tac prems 1)) ]))
|
wenzelm@26322
|
422 |
*)
|
wenzelm@26322
|
423 |
|
wenzelm@26322
|
424 |
(*** Equality rules ***)
|
wenzelm@26322
|
425 |
|
wenzelm@26322
|
426 |
lemmas refl = ieqI
|
wenzelm@26322
|
427 |
|
wenzelm@36319
|
428 |
schematic_lemma subst:
|
wenzelm@26322
|
429 |
assumes prem1: "p:a=b"
|
wenzelm@26322
|
430 |
and prem2: "q:P(a)"
|
wenzelm@26322
|
431 |
shows "?p : P(b)"
|
wenzelm@26322
|
432 |
apply (rule prem2 [THEN rev_mp])
|
wenzelm@26322
|
433 |
apply (rule prem1 [THEN ieqE])
|
wenzelm@26322
|
434 |
apply (rule impI)
|
wenzelm@26322
|
435 |
apply assumption
|
wenzelm@26322
|
436 |
done
|
wenzelm@26322
|
437 |
|
wenzelm@36319
|
438 |
schematic_lemma sym: "q:a=b ==> ?c:b=a"
|
wenzelm@26322
|
439 |
apply (erule subst)
|
wenzelm@26322
|
440 |
apply (rule refl)
|
wenzelm@26322
|
441 |
done
|
wenzelm@26322
|
442 |
|
wenzelm@36319
|
443 |
schematic_lemma trans: "[| p:a=b; q:b=c |] ==> ?d:a=c"
|
wenzelm@26322
|
444 |
apply (erule (1) subst)
|
wenzelm@26322
|
445 |
done
|
wenzelm@26322
|
446 |
|
wenzelm@26322
|
447 |
(** ~ b=a ==> ~ a=b **)
|
wenzelm@36319
|
448 |
schematic_lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
|
wenzelm@26322
|
449 |
apply (erule contrapos)
|
wenzelm@26322
|
450 |
apply (erule sym)
|
wenzelm@26322
|
451 |
done
|
wenzelm@26322
|
452 |
|
wenzelm@46465
|
453 |
schematic_lemma ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)"
|
wenzelm@46465
|
454 |
apply (drule sym)
|
wenzelm@46465
|
455 |
apply (erule subst)
|
wenzelm@46465
|
456 |
apply assumption
|
wenzelm@46465
|
457 |
done
|
wenzelm@26322
|
458 |
|
wenzelm@26322
|
459 |
(*A special case of ex1E that would otherwise need quantifier expansion*)
|
wenzelm@36319
|
460 |
schematic_lemma ex1_equalsE: "[| p:EX! x. P(x); q:P(a); r:P(b) |] ==> ?d:a=b"
|
wenzelm@26322
|
461 |
apply (erule ex1E)
|
wenzelm@26322
|
462 |
apply (rule trans)
|
wenzelm@26322
|
463 |
apply (rule_tac [2] sym)
|
wenzelm@26322
|
464 |
apply (assumption | erule spec [THEN mp])+
|
wenzelm@26322
|
465 |
done
|
wenzelm@26322
|
466 |
|
wenzelm@26322
|
467 |
(** Polymorphic congruence rules **)
|
wenzelm@26322
|
468 |
|
wenzelm@36319
|
469 |
schematic_lemma subst_context: "[| p:a=b |] ==> ?d:t(a)=t(b)"
|
wenzelm@26322
|
470 |
apply (erule ssubst)
|
wenzelm@26322
|
471 |
apply (rule refl)
|
wenzelm@26322
|
472 |
done
|
wenzelm@26322
|
473 |
|
wenzelm@36319
|
474 |
schematic_lemma subst_context2: "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)"
|
wenzelm@26322
|
475 |
apply (erule ssubst)+
|
wenzelm@26322
|
476 |
apply (rule refl)
|
wenzelm@26322
|
477 |
done
|
wenzelm@26322
|
478 |
|
wenzelm@36319
|
479 |
schematic_lemma subst_context3: "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)"
|
wenzelm@26322
|
480 |
apply (erule ssubst)+
|
wenzelm@26322
|
481 |
apply (rule refl)
|
wenzelm@26322
|
482 |
done
|
wenzelm@26322
|
483 |
|
wenzelm@26322
|
484 |
(*Useful with eresolve_tac for proving equalties from known equalities.
|
wenzelm@26322
|
485 |
a = b
|
wenzelm@26322
|
486 |
| |
|
wenzelm@26322
|
487 |
c = d *)
|
wenzelm@36319
|
488 |
schematic_lemma box_equals: "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d"
|
wenzelm@26322
|
489 |
apply (rule trans)
|
wenzelm@26322
|
490 |
apply (rule trans)
|
wenzelm@26322
|
491 |
apply (rule sym)
|
wenzelm@26322
|
492 |
apply assumption+
|
wenzelm@26322
|
493 |
done
|
wenzelm@26322
|
494 |
|
wenzelm@26322
|
495 |
(*Dual of box_equals: for proving equalities backwards*)
|
wenzelm@36319
|
496 |
schematic_lemma simp_equals: "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b"
|
wenzelm@26322
|
497 |
apply (rule trans)
|
wenzelm@26322
|
498 |
apply (rule trans)
|
wenzelm@26322
|
499 |
apply (assumption | rule sym)+
|
wenzelm@26322
|
500 |
done
|
wenzelm@26322
|
501 |
|
wenzelm@26322
|
502 |
(** Congruence rules for predicate letters **)
|
wenzelm@26322
|
503 |
|
wenzelm@36319
|
504 |
schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
|
wenzelm@26322
|
505 |
apply (rule iffI)
|
wenzelm@26322
|
506 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
|
wenzelm@26322
|
507 |
done
|
wenzelm@26322
|
508 |
|
wenzelm@36319
|
509 |
schematic_lemma pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
|
wenzelm@26322
|
510 |
apply (rule iffI)
|
wenzelm@26322
|
511 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
|
wenzelm@26322
|
512 |
done
|
wenzelm@26322
|
513 |
|
wenzelm@36319
|
514 |
schematic_lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
|
wenzelm@26322
|
515 |
apply (rule iffI)
|
wenzelm@26322
|
516 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
|
wenzelm@26322
|
517 |
done
|
wenzelm@26322
|
518 |
|
wenzelm@27152
|
519 |
lemmas pred_congs = pred1_cong pred2_cong pred3_cong
|
wenzelm@26322
|
520 |
|
wenzelm@26322
|
521 |
(*special case for the equality predicate!*)
|
wenzelm@46473
|
522 |
lemmas eq_cong = pred2_cong [where P = "op ="]
|
wenzelm@26322
|
523 |
|
wenzelm@26322
|
524 |
|
wenzelm@26322
|
525 |
(*** Simplifications of assumed implications.
|
wenzelm@26322
|
526 |
Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
|
wenzelm@26322
|
527 |
used with mp_tac (restricted to atomic formulae) is COMPLETE for
|
wenzelm@26322
|
528 |
intuitionistic propositional logic. See
|
wenzelm@26322
|
529 |
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
|
wenzelm@26322
|
530 |
(preprint, University of St Andrews, 1991) ***)
|
wenzelm@26322
|
531 |
|
wenzelm@36319
|
532 |
schematic_lemma conj_impE:
|
wenzelm@26322
|
533 |
assumes major: "p:(P&Q)-->S"
|
wenzelm@26322
|
534 |
and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
|
wenzelm@26322
|
535 |
shows "?p:R"
|
wenzelm@26322
|
536 |
apply (assumption | rule conjI impI major [THEN mp] minor)+
|
wenzelm@26322
|
537 |
done
|
wenzelm@26322
|
538 |
|
wenzelm@36319
|
539 |
schematic_lemma disj_impE:
|
wenzelm@26322
|
540 |
assumes major: "p:(P|Q)-->S"
|
wenzelm@26322
|
541 |
and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
|
wenzelm@26322
|
542 |
shows "?p:R"
|
wenzelm@26322
|
543 |
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
|
wenzelm@26322
|
544 |
resolve_tac [@{thm disjI1}, @{thm disjI2}, @{thm impI},
|
wenzelm@26322
|
545 |
@{thm major} RS @{thm mp}, @{thm minor}] 1) *})
|
wenzelm@26322
|
546 |
done
|
wenzelm@26322
|
547 |
|
wenzelm@26322
|
548 |
(*Simplifies the implication. Classical version is stronger.
|
wenzelm@26322
|
549 |
Still UNSAFE since Q must be provable -- backtracking needed. *)
|
wenzelm@36319
|
550 |
schematic_lemma imp_impE:
|
wenzelm@26322
|
551 |
assumes major: "p:(P-->Q)-->S"
|
wenzelm@26322
|
552 |
and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
|
wenzelm@26322
|
553 |
and r2: "!!x. x:S ==> r(x):R"
|
wenzelm@26322
|
554 |
shows "?p:R"
|
wenzelm@26322
|
555 |
apply (assumption | rule impI major [THEN mp] r1 r2)+
|
wenzelm@26322
|
556 |
done
|
wenzelm@26322
|
557 |
|
wenzelm@26322
|
558 |
(*Simplifies the implication. Classical version is stronger.
|
wenzelm@26322
|
559 |
Still UNSAFE since ~P must be provable -- backtracking needed. *)
|
wenzelm@36319
|
560 |
schematic_lemma not_impE:
|
wenzelm@26322
|
561 |
assumes major: "p:~P --> S"
|
wenzelm@26322
|
562 |
and r1: "!!y. y:P ==> q(y):False"
|
wenzelm@26322
|
563 |
and r2: "!!y. y:S ==> r(y):R"
|
wenzelm@26322
|
564 |
shows "?p:R"
|
wenzelm@26322
|
565 |
apply (assumption | rule notI impI major [THEN mp] r1 r2)+
|
wenzelm@26322
|
566 |
done
|
wenzelm@26322
|
567 |
|
wenzelm@26322
|
568 |
(*Simplifies the implication. UNSAFE. *)
|
wenzelm@36319
|
569 |
schematic_lemma iff_impE:
|
wenzelm@26322
|
570 |
assumes major: "p:(P<->Q)-->S"
|
wenzelm@26322
|
571 |
and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
|
wenzelm@26322
|
572 |
and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
|
wenzelm@26322
|
573 |
and r3: "!!x. x:S ==> s(x):R"
|
wenzelm@26322
|
574 |
shows "?p:R"
|
wenzelm@26322
|
575 |
apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
|
wenzelm@26322
|
576 |
done
|
wenzelm@26322
|
577 |
|
wenzelm@26322
|
578 |
(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
|
wenzelm@36319
|
579 |
schematic_lemma all_impE:
|
wenzelm@26322
|
580 |
assumes major: "p:(ALL x. P(x))-->S"
|
wenzelm@26322
|
581 |
and r1: "!!x. q:P(x)"
|
wenzelm@26322
|
582 |
and r2: "!!y. y:S ==> r(y):R"
|
wenzelm@26322
|
583 |
shows "?p:R"
|
wenzelm@26322
|
584 |
apply (assumption | rule allI impI major [THEN mp] r1 r2)+
|
wenzelm@26322
|
585 |
done
|
wenzelm@26322
|
586 |
|
wenzelm@26322
|
587 |
(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *)
|
wenzelm@36319
|
588 |
schematic_lemma ex_impE:
|
wenzelm@26322
|
589 |
assumes major: "p:(EX x. P(x))-->S"
|
wenzelm@26322
|
590 |
and r: "!!y. y:P(a)-->S ==> q(y):R"
|
wenzelm@26322
|
591 |
shows "?p:R"
|
wenzelm@26322
|
592 |
apply (assumption | rule exI impI major [THEN mp] r)+
|
wenzelm@26322
|
593 |
done
|
wenzelm@26322
|
594 |
|
wenzelm@26322
|
595 |
|
wenzelm@36319
|
596 |
schematic_lemma rev_cut_eq:
|
wenzelm@26322
|
597 |
assumes "p:a=b"
|
wenzelm@26322
|
598 |
and "!!x. x:a=b ==> f(x):R"
|
wenzelm@26322
|
599 |
shows "?p:R"
|
wenzelm@26322
|
600 |
apply (rule assms)+
|
wenzelm@26322
|
601 |
done
|
wenzelm@26322
|
602 |
|
wenzelm@26322
|
603 |
lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
|
wenzelm@26322
|
604 |
|
wenzelm@49906
|
605 |
ML_file "hypsubst.ML"
|
wenzelm@26322
|
606 |
|
wenzelm@26322
|
607 |
ML {*
|
wenzelm@43671
|
608 |
structure Hypsubst = Hypsubst
|
wenzelm@43671
|
609 |
(
|
wenzelm@26322
|
610 |
(*Take apart an equality judgement; otherwise raise Match!*)
|
wenzelm@26322
|
611 |
fun dest_eq (Const (@{const_name Proof}, _) $
|
wenzelm@41558
|
612 |
(Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u);
|
wenzelm@26322
|
613 |
|
wenzelm@26322
|
614 |
val imp_intr = @{thm impI}
|
wenzelm@26322
|
615 |
|
wenzelm@26322
|
616 |
(*etac rev_cut_eq moves an equality to be the last premise. *)
|
wenzelm@26322
|
617 |
val rev_cut_eq = @{thm rev_cut_eq}
|
wenzelm@26322
|
618 |
|
wenzelm@26322
|
619 |
val rev_mp = @{thm rev_mp}
|
wenzelm@26322
|
620 |
val subst = @{thm subst}
|
wenzelm@26322
|
621 |
val sym = @{thm sym}
|
wenzelm@26322
|
622 |
val thin_refl = @{thm thin_refl}
|
wenzelm@43671
|
623 |
);
|
wenzelm@26322
|
624 |
open Hypsubst;
|
wenzelm@26322
|
625 |
*}
|
wenzelm@26322
|
626 |
|
wenzelm@49906
|
627 |
ML_file "intprover.ML"
|
wenzelm@26322
|
628 |
|
wenzelm@26322
|
629 |
|
wenzelm@26322
|
630 |
(*** Rewrite rules ***)
|
wenzelm@26322
|
631 |
|
wenzelm@36319
|
632 |
schematic_lemma conj_rews:
|
wenzelm@26322
|
633 |
"?p1 : P & True <-> P"
|
wenzelm@26322
|
634 |
"?p2 : True & P <-> P"
|
wenzelm@26322
|
635 |
"?p3 : P & False <-> False"
|
wenzelm@26322
|
636 |
"?p4 : False & P <-> False"
|
wenzelm@26322
|
637 |
"?p5 : P & P <-> P"
|
wenzelm@26322
|
638 |
"?p6 : P & ~P <-> False"
|
wenzelm@26322
|
639 |
"?p7 : ~P & P <-> False"
|
wenzelm@26322
|
640 |
"?p8 : (P & Q) & R <-> P & (Q & R)"
|
wenzelm@26322
|
641 |
apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
|
wenzelm@26322
|
642 |
done
|
wenzelm@26322
|
643 |
|
wenzelm@36319
|
644 |
schematic_lemma disj_rews:
|
wenzelm@26322
|
645 |
"?p1 : P | True <-> True"
|
wenzelm@26322
|
646 |
"?p2 : True | P <-> True"
|
wenzelm@26322
|
647 |
"?p3 : P | False <-> P"
|
wenzelm@26322
|
648 |
"?p4 : False | P <-> P"
|
wenzelm@26322
|
649 |
"?p5 : P | P <-> P"
|
wenzelm@26322
|
650 |
"?p6 : (P | Q) | R <-> P | (Q | R)"
|
wenzelm@26322
|
651 |
apply (tactic {* IntPr.fast_tac 1 *})+
|
wenzelm@26322
|
652 |
done
|
wenzelm@26322
|
653 |
|
wenzelm@36319
|
654 |
schematic_lemma not_rews:
|
wenzelm@26322
|
655 |
"?p1 : ~ False <-> True"
|
wenzelm@26322
|
656 |
"?p2 : ~ True <-> False"
|
wenzelm@26322
|
657 |
apply (tactic {* IntPr.fast_tac 1 *})+
|
wenzelm@26322
|
658 |
done
|
wenzelm@26322
|
659 |
|
wenzelm@36319
|
660 |
schematic_lemma imp_rews:
|
wenzelm@26322
|
661 |
"?p1 : (P --> False) <-> ~P"
|
wenzelm@26322
|
662 |
"?p2 : (P --> True) <-> True"
|
wenzelm@26322
|
663 |
"?p3 : (False --> P) <-> True"
|
wenzelm@26322
|
664 |
"?p4 : (True --> P) <-> P"
|
wenzelm@26322
|
665 |
"?p5 : (P --> P) <-> True"
|
wenzelm@26322
|
666 |
"?p6 : (P --> ~P) <-> ~P"
|
wenzelm@26322
|
667 |
apply (tactic {* IntPr.fast_tac 1 *})+
|
wenzelm@26322
|
668 |
done
|
wenzelm@26322
|
669 |
|
wenzelm@36319
|
670 |
schematic_lemma iff_rews:
|
wenzelm@26322
|
671 |
"?p1 : (True <-> P) <-> P"
|
wenzelm@26322
|
672 |
"?p2 : (P <-> True) <-> P"
|
wenzelm@26322
|
673 |
"?p3 : (P <-> P) <-> True"
|
wenzelm@26322
|
674 |
"?p4 : (False <-> P) <-> ~P"
|
wenzelm@26322
|
675 |
"?p5 : (P <-> False) <-> ~P"
|
wenzelm@26322
|
676 |
apply (tactic {* IntPr.fast_tac 1 *})+
|
wenzelm@26322
|
677 |
done
|
wenzelm@26322
|
678 |
|
wenzelm@36319
|
679 |
schematic_lemma quant_rews:
|
wenzelm@26322
|
680 |
"?p1 : (ALL x. P) <-> P"
|
wenzelm@26322
|
681 |
"?p2 : (EX x. P) <-> P"
|
wenzelm@26322
|
682 |
apply (tactic {* IntPr.fast_tac 1 *})+
|
wenzelm@26322
|
683 |
done
|
wenzelm@26322
|
684 |
|
wenzelm@26322
|
685 |
(*These are NOT supplied by default!*)
|
wenzelm@36319
|
686 |
schematic_lemma distrib_rews1:
|
wenzelm@26322
|
687 |
"?p1 : ~(P|Q) <-> ~P & ~Q"
|
wenzelm@26322
|
688 |
"?p2 : P & (Q | R) <-> P&Q | P&R"
|
wenzelm@26322
|
689 |
"?p3 : (Q | R) & P <-> Q&P | R&P"
|
wenzelm@26322
|
690 |
"?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)"
|
wenzelm@26322
|
691 |
apply (tactic {* IntPr.fast_tac 1 *})+
|
wenzelm@26322
|
692 |
done
|
wenzelm@26322
|
693 |
|
wenzelm@36319
|
694 |
schematic_lemma distrib_rews2:
|
wenzelm@26322
|
695 |
"?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
|
wenzelm@26322
|
696 |
"?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
|
wenzelm@26322
|
697 |
"?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
|
wenzelm@26322
|
698 |
"?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"
|
wenzelm@26322
|
699 |
apply (tactic {* IntPr.fast_tac 1 *})+
|
wenzelm@26322
|
700 |
done
|
wenzelm@26322
|
701 |
|
wenzelm@26322
|
702 |
lemmas distrib_rews = distrib_rews1 distrib_rews2
|
wenzelm@26322
|
703 |
|
wenzelm@36319
|
704 |
schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
|
wenzelm@26322
|
705 |
apply (tactic {* IntPr.fast_tac 1 *})
|
wenzelm@26322
|
706 |
done
|
wenzelm@26322
|
707 |
|
wenzelm@36319
|
708 |
schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
|
wenzelm@26322
|
709 |
apply (tactic {* IntPr.fast_tac 1 *})
|
wenzelm@26322
|
710 |
done
|
clasohm@0
|
711 |
|
clasohm@0
|
712 |
end
|