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