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