7 declare [[eta_contract]] |
7 declare [[eta_contract]] |
8 |
8 |
9 typedecl 'a set |
9 typedecl 'a set |
10 instance set :: ("term") "term" .. |
10 instance set :: ("term") "term" .. |
11 |
11 |
12 consts |
12 |
13 Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set" (*comprehension*) |
13 subsection \<open>Set comprehension and membership\<close> |
14 Compl :: "('a set) \<Rightarrow> 'a set" (*complement*) |
14 |
15 Int :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Int" 70) |
15 axiomatization Collect :: "['a \<Rightarrow> o] \<Rightarrow> 'a set" |
16 Un :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Un" 65) |
16 and mem :: "['a, 'a set] \<Rightarrow> o" (infixl ":" 50) |
17 Union :: "(('a set)set) \<Rightarrow> 'a set" (*...of a set*) |
17 where mem_Collect_iff: "(a : Collect(P)) \<longleftrightarrow> P(a)" |
18 Inter :: "(('a set)set) \<Rightarrow> 'a set" (*...of a set*) |
18 and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)" |
19 UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" (*general*) |
|
20 INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" (*general*) |
|
21 Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" (*bounded quants*) |
|
22 Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" (*bounded quants*) |
|
23 mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o" (*monotonicity*) |
|
24 mem :: "['a, 'a set] \<Rightarrow> o" (infixl ":" 50) (*membership*) |
|
25 subset :: "['a set, 'a set] \<Rightarrow> o" (infixl "<=" 50) |
|
26 singleton :: "'a \<Rightarrow> 'a set" ("{_}") |
|
27 empty :: "'a set" ("{}") |
|
28 |
19 |
29 syntax |
20 syntax |
30 "_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})") (*collection*) |
21 "_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})") |
31 |
|
32 (* Big Intersection / Union *) |
|
33 |
|
34 "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) |
|
35 "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) |
|
36 |
|
37 (* Bounded Quantifiers *) |
|
38 |
|
39 "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" ("(ALL _:_./ _)" [0, 0, 0] 10) |
|
40 "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" ("(EX _:_./ _)" [0, 0, 0] 10) |
|
41 |
|
42 translations |
22 translations |
43 "{x. P}" == "CONST Collect(\<lambda>x. P)" |
23 "{x. P}" == "CONST Collect(\<lambda>x. P)" |
44 "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)" |
|
45 "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)" |
|
46 "ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)" |
|
47 "EX x:A. P" == "CONST Bex(A, \<lambda>x. P)" |
|
48 |
|
49 axiomatization where |
|
50 mem_Collect_iff: "(a : {x. P(x)}) \<longleftrightarrow> P(a)" and |
|
51 set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)" |
|
52 |
|
53 defs |
|
54 Ball_def: "Ball(A, P) == ALL x. x:A \<longrightarrow> P(x)" |
|
55 Bex_def: "Bex(A, P) == EX x. x:A \<and> P(x)" |
|
56 mono_def: "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))" |
|
57 subset_def: "A <= B == ALL x:A. x:B" |
|
58 singleton_def: "{a} == {x. x=a}" |
|
59 empty_def: "{} == {x. False}" |
|
60 Un_def: "A Un B == {x. x:A | x:B}" |
|
61 Int_def: "A Int B == {x. x:A \<and> x:B}" |
|
62 Compl_def: "Compl(A) == {x. \<not>x:A}" |
|
63 INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}" |
|
64 UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}" |
|
65 Inter_def: "Inter(S) == (INT x:S. x)" |
|
66 Union_def: "Union(S) == (UN x:S. x)" |
|
67 |
|
68 |
24 |
69 lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}" |
25 lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}" |
70 apply (rule mem_Collect_iff [THEN iffD2]) |
26 apply (rule mem_Collect_iff [THEN iffD2]) |
71 apply assumption |
27 apply assumption |
72 done |
28 done |
83 done |
39 done |
84 |
40 |
85 |
41 |
86 subsection \<open>Bounded quantifiers\<close> |
42 subsection \<open>Bounded quantifiers\<close> |
87 |
43 |
|
44 definition Ball :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" |
|
45 where "Ball(A, P) == ALL x. x:A \<longrightarrow> P(x)" |
|
46 |
|
47 definition Bex :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> o" |
|
48 where "Bex(A, P) == EX x. x:A \<and> P(x)" |
|
49 |
|
50 syntax |
|
51 "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" ("(ALL _:_./ _)" [0, 0, 0] 10) |
|
52 "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" ("(EX _:_./ _)" [0, 0, 0] 10) |
|
53 translations |
|
54 "ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)" |
|
55 "EX x:A. P" == "CONST Bex(A, \<lambda>x. P)" |
|
56 |
88 lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)" |
57 lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)" |
89 by (simp add: Ball_def) |
58 by (simp add: Ball_def) |
90 |
59 |
91 lemma bspec: "\<lbrakk>ALL x:A. P(x); x:A\<rbrakk> \<Longrightarrow> P(x)" |
60 lemma bspec: "\<lbrakk>ALL x:A. P(x); x:A\<rbrakk> \<Longrightarrow> P(x)" |
92 by (simp add: Ball_def) |
61 by (simp add: Ball_def) |
105 |
74 |
106 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
75 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
107 lemma ball_rew: "(ALL x:A. True) \<longleftrightarrow> True" |
76 lemma ball_rew: "(ALL x:A. True) \<longleftrightarrow> True" |
108 by (blast intro: ballI) |
77 by (blast intro: ballI) |
109 |
78 |
110 |
79 subsubsection \<open>Congruence rules\<close> |
111 subsection \<open>Congruence rules\<close> |
|
112 |
80 |
113 lemma ball_cong: |
81 lemma ball_cong: |
114 "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow> |
82 "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow> |
115 (ALL x:A. P(x)) \<longleftrightarrow> (ALL x:A'. P'(x))" |
83 (ALL x:A. P(x)) \<longleftrightarrow> (ALL x:A'. P'(x))" |
116 by (blast intro: ballI elim: ballE) |
84 by (blast intro: ballI elim: ballE) |
117 |
85 |
118 lemma bex_cong: |
86 lemma bex_cong: |
119 "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow> |
87 "\<lbrakk>A = A'; \<And>x. x:A' \<Longrightarrow> P(x) \<longleftrightarrow> P'(x)\<rbrakk> \<Longrightarrow> |
120 (EX x:A. P(x)) \<longleftrightarrow> (EX x:A'. P'(x))" |
88 (EX x:A. P(x)) \<longleftrightarrow> (EX x:A'. P'(x))" |
121 by (blast intro: bexI elim: bexE) |
89 by (blast intro: bexI elim: bexE) |
|
90 |
|
91 |
|
92 subsection \<open>Further operations\<close> |
|
93 |
|
94 definition subset :: "['a set, 'a set] \<Rightarrow> o" (infixl "<=" 50) |
|
95 where "A <= B == ALL x:A. x:B" |
|
96 |
|
97 definition mono :: "['a set \<Rightarrow> 'b set] \<Rightarrow> o" |
|
98 where "mono(f) == (ALL A B. A <= B \<longrightarrow> f(A) <= f(B))" |
|
99 |
|
100 definition singleton :: "'a \<Rightarrow> 'a set" ("{_}") |
|
101 where "{a} == {x. x=a}" |
|
102 |
|
103 definition empty :: "'a set" ("{}") |
|
104 where "{} == {x. False}" |
|
105 |
|
106 definition Un :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Un" 65) |
|
107 where "A Un B == {x. x:A | x:B}" |
|
108 |
|
109 definition Int :: "['a set, 'a set] \<Rightarrow> 'a set" (infixl "Int" 70) |
|
110 where "A Int B == {x. x:A \<and> x:B}" |
|
111 |
|
112 definition Compl :: "('a set) \<Rightarrow> 'a set" |
|
113 where "Compl(A) == {x. \<not>x:A}" |
|
114 |
|
115 |
|
116 subsection \<open>Big Intersection / Union\<close> |
|
117 |
|
118 definition INTER :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" |
|
119 where "INTER(A, B) == {y. ALL x:A. y: B(x)}" |
|
120 |
|
121 definition UNION :: "['a set, 'a \<Rightarrow> 'b set] \<Rightarrow> 'b set" |
|
122 where "UNION(A, B) == {y. EX x:A. y: B(x)}" |
|
123 |
|
124 syntax |
|
125 "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(INT _:_./ _)" [0, 0, 0] 10) |
|
126 "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(UN _:_./ _)" [0, 0, 0] 10) |
|
127 translations |
|
128 "INT x:A. B" == "CONST INTER(A, \<lambda>x. B)" |
|
129 "UN x:A. B" == "CONST UNION(A, \<lambda>x. B)" |
|
130 |
|
131 definition Inter :: "(('a set)set) \<Rightarrow> 'a set" |
|
132 where "Inter(S) == (INT x:S. x)" |
|
133 |
|
134 definition Union :: "(('a set)set) \<Rightarrow> 'a set" |
|
135 where "Union(S) == (UN x:S. x)" |
122 |
136 |
123 |
137 |
124 subsection \<open>Rules for subsets\<close> |
138 subsection \<open>Rules for subsets\<close> |
125 |
139 |
126 lemma subsetI: "(\<And>x. x:A \<Longrightarrow> x:B) \<Longrightarrow> A <= B" |
140 lemma subsetI: "(\<And>x. x:A \<Longrightarrow> x:B) \<Longrightarrow> A <= B" |