|
1 theory Relations = Main: |
|
2 |
|
3 ML "Pretty.setmargin 64" |
|
4 |
|
5 (*Id is only used in UNITY*) |
|
6 (*refl, antisym,trans,univalent,\<dots> ho hum*) |
|
7 |
|
8 text{* |
|
9 @{thm[display]"Id_def"} |
|
10 \rulename{Id_def} |
|
11 *} |
|
12 |
|
13 text{* |
|
14 @{thm[display]"comp_def"} |
|
15 \rulename{comp_def} |
|
16 *} |
|
17 |
|
18 text{* |
|
19 @{thm[display]"R_O_Id"} |
|
20 \rulename{R_O_Id} |
|
21 *} |
|
22 |
|
23 text{* |
|
24 @{thm[display]"comp_mono"} |
|
25 \rulename{comp_mono} |
|
26 *} |
|
27 |
|
28 text{* |
|
29 @{thm[display]"converse_iff"} |
|
30 \rulename{converse_iff} |
|
31 *} |
|
32 |
|
33 text{* |
|
34 @{thm[display]"converse_comp"} |
|
35 \rulename{converse_comp} |
|
36 *} |
|
37 |
|
38 text{* |
|
39 @{thm[display]"Image_iff"} |
|
40 \rulename{Image_iff} |
|
41 *} |
|
42 |
|
43 text{* |
|
44 @{thm[display]"Image_UN"} |
|
45 \rulename{Image_UN} |
|
46 *} |
|
47 |
|
48 text{* |
|
49 @{thm[display]"Domain_iff"} |
|
50 \rulename{Domain_iff} |
|
51 *} |
|
52 |
|
53 text{* |
|
54 @{thm[display]"Range_iff"} |
|
55 \rulename{Range_iff} |
|
56 *} |
|
57 |
|
58 text{* |
|
59 @{thm[display]"relpow.simps"} |
|
60 \rulename{relpow.simps} |
|
61 |
|
62 @{thm[display]"rtrancl_unfold"} |
|
63 \rulename{rtrancl_unfold} |
|
64 |
|
65 @{thm[display]"rtrancl_refl"} |
|
66 \rulename{rtrancl_refl} |
|
67 |
|
68 @{thm[display]"r_into_rtrancl"} |
|
69 \rulename{r_into_rtrancl} |
|
70 |
|
71 @{thm[display]"rtrancl_trans"} |
|
72 \rulename{rtrancl_trans} |
|
73 |
|
74 @{thm[display]"rtrancl_induct"} |
|
75 \rulename{rtrancl_induct} |
|
76 |
|
77 @{thm[display]"rtrancl_idemp"} |
|
78 \rulename{rtrancl_idemp} |
|
79 |
|
80 @{thm[display]"r_into_trancl"} |
|
81 \rulename{r_into_trancl} |
|
82 |
|
83 @{thm[display]"trancl_trans"} |
|
84 \rulename{trancl_trans} |
|
85 |
|
86 @{thm[display]"trancl_into_rtrancl"} |
|
87 \rulename{trancl_into_rtrancl} |
|
88 |
|
89 @{thm[display]"trancl_converse"} |
|
90 \rulename{trancl_converse} |
|
91 *} |
|
92 |
|
93 text{*Relations. transitive closure*} |
|
94 |
|
95 lemma rtrancl_converseD: "(x,y) \<in> (r^-1)^* \<Longrightarrow> (y,x) \<in> r^*" |
|
96 apply (erule rtrancl_induct) |
|
97 apply (rule rtrancl_refl) |
|
98 apply (blast intro: r_into_rtrancl rtrancl_trans) |
|
99 done |
|
100 |
|
101 text{* |
|
102 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline |
|
103 \isanewline |
|
104 goal\ {\isacharparenleft}lemma\ rtrancl{\isacharunderscore}converseD{\isacharparenright}{\isacharcolon}\isanewline |
|
105 {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharparenleft}r{\isacharcircum}{\isacharminus}\isadigit{1}{\isacharparenright}{\isacharcircum}{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}\isanewline |
|
106 \ \isadigit{1}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}\isanewline |
|
107 \ \isadigit{2}{\isachardot}\ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharparenleft}r{\isacharcircum}{\isacharminus}\isadigit{1}{\isacharparenright}{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharminus}\isadigit{1}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}{\isasymrbrakk}\isanewline |
|
108 \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}z{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk} |
|
109 *} |
|
110 |
|
111 lemma rtrancl_converseI: "(y,x) \<in> r^* \<Longrightarrow> (x,y) \<in> (r^-1)^*" |
|
112 apply (erule rtrancl_induct) |
|
113 apply (rule rtrancl_refl) |
|
114 apply (blast intro: r_into_rtrancl rtrancl_trans) |
|
115 done |
|
116 |
|
117 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" |
|
118 apply (auto intro: rtrancl_converseI dest: rtrancl_converseD) |
|
119 done |
|
120 |
|
121 |
|
122 lemma "A \<subseteq> Id" |
|
123 apply (rule subsetI) |
|
124 apply (auto) |
|
125 oops |
|
126 |
|
127 text{* |
|
128 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline |
|
129 \isanewline |
|
130 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline |
|
131 A\ {\isasymsubseteq}\ Id\isanewline |
|
132 \ \isadigit{1}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ Id |
|
133 |
|
134 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{2}\isanewline |
|
135 \isanewline |
|
136 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline |
|
137 A\ {\isasymsubseteq}\ Id\isanewline |
|
138 \ \isadigit{1}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ A\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ b |
|
139 *} |
|
140 |
|
141 text{*questions: do we cover force? (Why not?) |
|
142 Do we include tables of operators in ASCII and X-symbol notation like in the Logics manuals?*} |
|
143 |
|
144 |
|
145 text{*rejects*} |
|
146 |
|
147 lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a" |
|
148 apply (blast) |
|
149 done |
|
150 |
|
151 text{*Pow, Inter too little used*} |
|
152 |
|
153 lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)" |
|
154 apply (simp add: psubset_def) |
|
155 done |
|
156 |
|
157 (* |
|
158 text{* |
|
159 @{thm[display]"DD"} |
|
160 \rulename{DD} |
|
161 *} |
|
162 *) |
|
163 |
|
164 end |