5 |
5 |
6 Some miscellaneous and add-hoc set theory concepts. |
6 Some miscellaneous and add-hoc set theory concepts. |
7 |
7 |
8 *) |
8 *) |
9 |
9 |
10 Goalw [measure_def, less_than_def] |
|
11 "less_than(A) = {<x,y>:A*A. x<y}"; |
|
12 by Auto_tac; |
|
13 qed "less_than_equals"; |
|
14 |
|
15 Goalw [less_than_def] "wf(less_than(A))"; |
|
16 by (rtac wf_measure 1); |
|
17 qed "wf_less_than"; |
|
18 |
|
19 Goalw [less_than_def, measure_def] |
|
20 "less_than(A)<= A*A"; |
|
21 by Auto_tac; |
|
22 qed "less_than_subset"; |
|
23 |
|
24 Goalw [less_than_def, measure_def] |
|
25 "<x,y>:less_than(A) <-> (x:A & y:A & x<y)"; |
|
26 by Auto_tac; |
|
27 qed "less_than_iff"; |
|
28 |
|
29 Goalw [lessThan_def] |
|
30 "i:lessThan(k,A) <-> i:A & i<k"; |
|
31 by Auto_tac; |
|
32 qed "lessThan_iff"; |
|
33 |
|
34 Goalw [greaterThan_def] |
10 Goalw [greaterThan_def] |
35 "i:greaterThan(k,A) <-> i:A & k<i"; |
11 "i:greaterThan(k,A) <-> i:A & k<i"; |
36 by Auto_tac; |
12 by Auto_tac; |
37 qed "greaterThan_iff"; |
13 qed "greaterThan_iff"; |
38 |
|
39 |
|
40 (** Needed for WF reasoning in WFair.ML **) |
|
41 |
|
42 Goal "k:A ==>less_than(A)``{k} = greaterThan(k, A)"; |
|
43 by (rtac equalityI 1); |
|
44 by (auto_tac (claset(), simpset() addsimps |
|
45 [less_than_iff,greaterThan_iff])); |
|
46 qed "Image_less_than"; |
|
47 |
|
48 Goal "k:A ==> less_than(A)-`` {k} = lessThan(k, A)"; |
|
49 by (rtac equalityI 1); |
|
50 by (auto_tac (claset(), simpset() addsimps |
|
51 [less_than_iff,lessThan_iff])); |
|
52 qed "Image_inverse_less_than"; |
|
53 |
|
54 Addsimps [Image_less_than, Image_inverse_less_than]; |
|
55 |
|
56 |
14 |
57 (** Ad-hoc set-theory rules **) |
15 (** Ad-hoc set-theory rules **) |
58 |
16 |
59 Goal "Union(B) Int A = (UN b:B. b Int A)"; |
17 Goal "Union(B) Int A = (UN b:B. b Int A)"; |
60 by Auto_tac; |
18 by Auto_tac; |
79 by (assume_tac 1); |
37 by (assume_tac 1); |
80 qed "list_nat_into_univ"; |
38 qed "list_nat_into_univ"; |
81 |
39 |
82 (** To be moved to Update theory **) |
40 (** To be moved to Update theory **) |
83 |
41 |
84 Goalw [update_def] |
|
85 "[| f:Pi(A,B); x:A; y:B(x) |] ==> f(x:=y):Pi(A, B)"; |
|
86 by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb, |
|
87 apply_funtype, lam_type]) 1); |
|
88 qed "update_type2"; |
|
89 |
|
90 (** Simplication rules for Collect; To be moved elsewhere **) |
42 (** Simplication rules for Collect; To be moved elsewhere **) |
91 Goal "{x:A. P(x)} Int A = {x:A. P(x)}"; |
43 Goal "{x:A. P(x)} Int A = {x:A. P(x)}"; |
92 by Auto_tac; |
44 by Auto_tac; |
93 qed "Collect_Int2"; |
45 qed "Collect_Int2"; |
94 |
46 |
105 |
57 |
106 Goal "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"; |
58 Goal "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"; |
107 by Auto_tac; |
59 by Auto_tac; |
108 qed "Collect_conj_eq"; |
60 qed "Collect_conj_eq"; |
109 |
61 |
|
62 Goal "Union(B) Int A = (UN C:B. C Int A)"; |
|
63 by (Blast_tac 1); |
|
64 qed "Int_Union2"; |
110 |
65 |
|
66 Goal "A Int cons(a, B) = (if a : A then cons(a, A Int B) else A Int B)"; |
|
67 by Auto_tac; |
|
68 qed "Int_cons_right"; |
111 |
69 |
|
70 Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)"; |
|
71 by Auto_tac; |
|
72 qed "Int_succ_right"; |