author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 13524 | 604d0f3622d6 |
child 15408 | 6001135caa91 |
permissions | -rw-r--r-- |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/IOA/NTP/Lemmas.ML |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow & Konrad Slind |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
*) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
5 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
(* Logic *) |
4532 | 7 |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
8 |
goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
9 |
by (Fast_tac 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
qed "fork_lemma"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
11 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
by (Fast_tac 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
qed "imp_or_lem"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
16 |
goal HOL.thy "(X = (~ Y)) = ((~X) = Y)"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
17 |
by (Fast_tac 1); |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
qed "neg_flip"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
20 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
(* Sets *) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
val set_lemmas = |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
23 |
map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1])) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
24 |
["f(x) : (UN x. {f(x)})", |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
25 |
"f x y : (UN x y. {f x y})", |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
"!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})", |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
27 |
"!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"]; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
|
4377 | 30 |
(* Arithmetic *) |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
31 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10215
diff
changeset
|
32 |
goal NatArith.thy "!!x. 0<x ==> (x - 1 = y) = (x = Suc(y))"; |
5192 | 33 |
by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
qed "pred_suc"; |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
|
4377 | 37 |
Addsimps (hd_append :: set_lemmas); |