equal
deleted
inserted
replaced
|
1 (*<*) |
1 theory Sets = Main: |
2 theory Sets = Main: |
2 |
3 (*>*) |
3 section{*Sets, Functions and Relations*} |
4 section{*Sets, Functions and Relations*} |
4 |
5 |
5 subsection{*Set Notation*} |
6 subsection{*Set Notation*} |
6 |
7 |
7 term "A \<union> B" |
8 text{* |
8 term "A \<inter> B" |
9 \begin{center} |
9 term "A - B" |
10 \begin{tabular}{ccc} |
10 term "a \<in> A" |
11 @{term "A \<union> B"} & @{term "A \<inter> B"} & @{term "A - B"} \\ |
11 term "b \<notin> A" |
12 @{term "a \<in> A"} & @{term "b \<notin> A"} \\ |
12 term "{a,b}" |
13 @{term "{a,b}"} & @{text "{x. P x}"} \\ |
13 term "{x. P x}" |
14 @{term "\<Union> M"} & @{text "\<Union>a \<in> A. F a"} |
14 term "{x+y+eps |x y. x < y}" |
15 \end{tabular} |
15 term "\<Union> M" |
16 \end{center} |
16 term "\<Union>a \<in> A. F a" |
17 *} |
17 |
18 |
18 subsection{*Functions*} |
19 subsection{*Some Functions*} |
19 |
20 |
|
21 text{* |
|
22 \begin{tabular}{l} |
|
23 @{thm id_def}\\ |
|
24 @{thm o_def[no_vars]}\\ |
|
25 @{thm image_def[no_vars]}\\ |
|
26 @{thm vimage_def[no_vars]} |
|
27 \end{tabular} |
|
28 *} |
|
29 (*<*) |
20 thm id_def |
30 thm id_def |
21 thm o_assoc |
31 thm o_def[no_vars] |
22 thm image_Int |
32 thm image_def[no_vars] |
23 thm vimage_Compl |
33 thm vimage_def[no_vars] |
|
34 (*>*) |
24 |
35 |
25 |
36 subsection{*Some Relations*} |
26 subsection{*Relations*} |
|
27 |
37 |
28 thm Id_def |
38 thm Id_def |
29 thm converse_comp |
39 thm converse_def |
30 thm Image_def |
40 thm Image_def |
31 thm relpow.simps |
41 thm relpow.simps |
32 thm rtrancl_idemp |
42 thm rtrancl_idemp |
33 thm trancl_converse |
43 thm trancl_converse |
34 |
44 |
115 |
125 |
116 Show that the semantics for @{term EF} satisfies the following recursion equation: |
126 Show that the semantics for @{term EF} satisfies the following recursion equation: |
117 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"} |
127 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"} |
118 \end{exercise} |
128 \end{exercise} |
119 *} |
129 *} |
120 |
130 (*<*) |
121 end |
131 end |
122 |
132 (*>*) |
123 |
|