1 theory Relations imports Main begin |
|
2 |
|
3 (*Id is only used in UNITY*) |
|
4 (*refl, antisym,trans,univalent,\<dots> ho hum*) |
|
5 |
|
6 text{* |
|
7 @{thm[display] Id_def[no_vars]} |
|
8 \rulename{Id_def} |
|
9 *} |
|
10 |
|
11 text{* |
|
12 @{thm[display] relcomp_unfold[no_vars]} |
|
13 \rulename{relcomp_unfold} |
|
14 *} |
|
15 |
|
16 text{* |
|
17 @{thm[display] R_O_Id[no_vars]} |
|
18 \rulename{R_O_Id} |
|
19 *} |
|
20 |
|
21 text{* |
|
22 @{thm[display] relcomp_mono[no_vars]} |
|
23 \rulename{relcomp_mono} |
|
24 *} |
|
25 |
|
26 text{* |
|
27 @{thm[display] converse_iff[no_vars]} |
|
28 \rulename{converse_iff} |
|
29 *} |
|
30 |
|
31 text{* |
|
32 @{thm[display] converse_relcomp[no_vars]} |
|
33 \rulename{converse_relcomp} |
|
34 *} |
|
35 |
|
36 text{* |
|
37 @{thm[display] Image_iff[no_vars]} |
|
38 \rulename{Image_iff} |
|
39 *} |
|
40 |
|
41 text{* |
|
42 @{thm[display] Image_UN[no_vars]} |
|
43 \rulename{Image_UN} |
|
44 *} |
|
45 |
|
46 text{* |
|
47 @{thm[display] Domain_iff[no_vars]} |
|
48 \rulename{Domain_iff} |
|
49 *} |
|
50 |
|
51 text{* |
|
52 @{thm[display] Range_iff[no_vars]} |
|
53 \rulename{Range_iff} |
|
54 *} |
|
55 |
|
56 text{* |
|
57 @{thm[display] relpow.simps[no_vars]} |
|
58 \rulename{relpow.simps} |
|
59 |
|
60 @{thm[display] rtrancl_refl[no_vars]} |
|
61 \rulename{rtrancl_refl} |
|
62 |
|
63 @{thm[display] r_into_rtrancl[no_vars]} |
|
64 \rulename{r_into_rtrancl} |
|
65 |
|
66 @{thm[display] rtrancl_trans[no_vars]} |
|
67 \rulename{rtrancl_trans} |
|
68 |
|
69 @{thm[display] rtrancl_induct[no_vars]} |
|
70 \rulename{rtrancl_induct} |
|
71 |
|
72 @{thm[display] rtrancl_idemp[no_vars]} |
|
73 \rulename{rtrancl_idemp} |
|
74 |
|
75 @{thm[display] r_into_trancl[no_vars]} |
|
76 \rulename{r_into_trancl} |
|
77 |
|
78 @{thm[display] trancl_trans[no_vars]} |
|
79 \rulename{trancl_trans} |
|
80 |
|
81 @{thm[display] trancl_into_rtrancl[no_vars]} |
|
82 \rulename{trancl_into_rtrancl} |
|
83 |
|
84 @{thm[display] trancl_converse[no_vars]} |
|
85 \rulename{trancl_converse} |
|
86 *} |
|
87 |
|
88 text{*Relations. transitive closure*} |
|
89 |
|
90 lemma rtrancl_converseD: "(x,y) \<in> (r\<inverse>)\<^sup>* \<Longrightarrow> (y,x) \<in> r\<^sup>*" |
|
91 apply (erule rtrancl_induct) |
|
92 txt{* |
|
93 @{subgoals[display,indent=0,margin=65]} |
|
94 *}; |
|
95 apply (rule rtrancl_refl) |
|
96 apply (blast intro: rtrancl_trans) |
|
97 done |
|
98 |
|
99 |
|
100 lemma rtrancl_converseI: "(y,x) \<in> r\<^sup>* \<Longrightarrow> (x,y) \<in> (r\<inverse>)\<^sup>*" |
|
101 apply (erule rtrancl_induct) |
|
102 apply (rule rtrancl_refl) |
|
103 apply (blast intro: rtrancl_trans) |
|
104 done |
|
105 |
|
106 lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" |
|
107 by (auto intro: rtrancl_converseI dest: rtrancl_converseD) |
|
108 |
|
109 lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" |
|
110 apply (intro equalityI subsetI) |
|
111 txt{* |
|
112 after intro rules |
|
113 |
|
114 @{subgoals[display,indent=0,margin=65]} |
|
115 *}; |
|
116 apply clarify |
|
117 txt{* |
|
118 after splitting |
|
119 @{subgoals[display,indent=0,margin=65]} |
|
120 *}; |
|
121 oops |
|
122 |
|
123 |
|
124 lemma "(\<forall>u v. (u,v) \<in> A \<longrightarrow> u=v) \<Longrightarrow> A \<subseteq> Id" |
|
125 apply (rule subsetI) |
|
126 txt{* |
|
127 @{subgoals[display,indent=0,margin=65]} |
|
128 |
|
129 after subsetI |
|
130 *}; |
|
131 apply clarify |
|
132 txt{* |
|
133 @{subgoals[display,indent=0,margin=65]} |
|
134 |
|
135 subgoals after clarify |
|
136 *}; |
|
137 by blast |
|
138 |
|
139 |
|
140 |
|
141 |
|
142 text{*rejects*} |
|
143 |
|
144 lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a" |
|
145 apply (blast) |
|
146 done |
|
147 |
|
148 text{*Pow, Inter too little used*} |
|
149 |
|
150 lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)" |
|
151 apply (simp add: psubset_eq) |
|
152 done |
|
153 |
|
154 end |
|