author | paulson |
Wed, 25 Jun 2003 13:17:26 +0200 | |
changeset 14072 | f932be305381 |
parent 14071 | 373806545656 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: HOL/UNITY/UNITYMisc.ML |
2 |
ID: $Id$ |
|
3 |
Author: Sidi O Ehmety, Computer Laboratory |
|
4 |
Copyright 2001 University of Cambridge |
|
5 |
||
6 |
Some miscellaneous and add-hoc set theory concepts. |
|
7 |
||
8 |
*) |
|
9 |
||
10 |
(** Ad-hoc set-theory rules **) |
|
11 |
||
12 |
Goal "Union(B) Int A = (UN b:B. b Int A)"; |
|
13 |
by Auto_tac; |
|
14 |
qed "Int_Union_Union"; |
|
15 |
||
16 |
Goal "A Int Union(B) = (UN b:B. A Int b)"; |
|
17 |
by Auto_tac; |
|
18 |
qed "Int_Union_Union2"; |
|
19 |
||
20 |
||
21 |
(** Needed in State theory for the current definition of variables |
|
22 |
where they are indexed by lists **) |
|
23 |
||
24 |
Goal "i:list(nat) ==> i:univ(0)"; |
|
25 |
by (dres_inst_tac [("B", "0")] list_into_univ 1); |
|
26 |
by (blast_tac (claset() addIs [nat_into_univ]) 1); |
|
27 |
by (assume_tac 1); |
|
28 |
qed "list_nat_into_univ"; |
|
29 |
||
30 |
||
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
31 |
(** Simplication rules for Collect **) |
11479 | 32 |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
33 |
(*Currently unused*) |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
34 |
Goal "{x:A. P(x)} Int B = {x : A Int B. P(x)}"; |
11479 | 35 |
by Auto_tac; |
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
36 |
qed "Collect_Int_left"; |
11479 | 37 |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
38 |
(*Currently unused*) |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
39 |
Goal "A Int {x:B. P(x)} = {x : A Int B. P(x)}"; |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
40 |
by Auto_tac; |
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14071
diff
changeset
|
41 |
qed "Collect_Int_right"; |
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14046
diff
changeset
|
42 |
|
11479 | 43 |
Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"; |
44 |
by Auto_tac; |
|
45 |
qed "Collect_disj_eq"; |
|
46 |
||
47 |
Goal "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"; |
|
48 |
by Auto_tac; |
|
49 |
qed "Collect_conj_eq"; |
|
50 |
||
14046 | 51 |
Goal "Union(B) Int A = (UN C:B. C Int A)"; |
52 |
by (Blast_tac 1); |
|
53 |
qed "Int_Union2"; |
|
11479 | 54 |
|
14046 | 55 |
Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)"; |
56 |
by Auto_tac; |
|
57 |
qed "Int_succ_right"; |