1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/Sets/Relations.thy Mon Oct 23 16:24:52 2000 +0200
1.3 @@ -0,0 +1,164 @@
1.4 +theory Relations = Main:
1.5 +
1.6 +ML "Pretty.setmargin 64"
1.7 +
1.8 +(*Id is only used in UNITY*)
1.9 +(*refl, antisym,trans,univalent,\<dots> ho hum*)
1.10 +
1.11 +text{*
1.12 +@{thm[display]"Id_def"}
1.13 +\rulename{Id_def}
1.14 +*}
1.15 +
1.16 +text{*
1.17 +@{thm[display]"comp_def"}
1.18 +\rulename{comp_def}
1.19 +*}
1.20 +
1.21 +text{*
1.22 +@{thm[display]"R_O_Id"}
1.23 +\rulename{R_O_Id}
1.24 +*}
1.25 +
1.26 +text{*
1.27 +@{thm[display]"comp_mono"}
1.28 +\rulename{comp_mono}
1.29 +*}
1.30 +
1.31 +text{*
1.32 +@{thm[display]"converse_iff"}
1.33 +\rulename{converse_iff}
1.34 +*}
1.35 +
1.36 +text{*
1.37 +@{thm[display]"converse_comp"}
1.38 +\rulename{converse_comp}
1.39 +*}
1.40 +
1.41 +text{*
1.42 +@{thm[display]"Image_iff"}
1.43 +\rulename{Image_iff}
1.44 +*}
1.45 +
1.46 +text{*
1.47 +@{thm[display]"Image_UN"}
1.48 +\rulename{Image_UN}
1.49 +*}
1.50 +
1.51 +text{*
1.52 +@{thm[display]"Domain_iff"}
1.53 +\rulename{Domain_iff}
1.54 +*}
1.55 +
1.56 +text{*
1.57 +@{thm[display]"Range_iff"}
1.58 +\rulename{Range_iff}
1.59 +*}
1.60 +
1.61 +text{*
1.62 +@{thm[display]"relpow.simps"}
1.63 +\rulename{relpow.simps}
1.64 +
1.65 +@{thm[display]"rtrancl_unfold"}
1.66 +\rulename{rtrancl_unfold}
1.67 +
1.68 +@{thm[display]"rtrancl_refl"}
1.69 +\rulename{rtrancl_refl}
1.70 +
1.71 +@{thm[display]"r_into_rtrancl"}
1.72 +\rulename{r_into_rtrancl}
1.73 +
1.74 +@{thm[display]"rtrancl_trans"}
1.75 +\rulename{rtrancl_trans}
1.76 +
1.77 +@{thm[display]"rtrancl_induct"}
1.78 +\rulename{rtrancl_induct}
1.79 +
1.80 +@{thm[display]"rtrancl_idemp"}
1.81 +\rulename{rtrancl_idemp}
1.82 +
1.83 +@{thm[display]"r_into_trancl"}
1.84 +\rulename{r_into_trancl}
1.85 +
1.86 +@{thm[display]"trancl_trans"}
1.87 +\rulename{trancl_trans}
1.88 +
1.89 +@{thm[display]"trancl_into_rtrancl"}
1.90 +\rulename{trancl_into_rtrancl}
1.91 +
1.92 +@{thm[display]"trancl_converse"}
1.93 +\rulename{trancl_converse}
1.94 +*}
1.95 +
1.96 +text{*Relations. transitive closure*}
1.97 +
1.98 +lemma rtrancl_converseD: "(x,y) \<in> (r^-1)^* \<Longrightarrow> (y,x) \<in> r^*"
1.99 + apply (erule rtrancl_induct)
1.100 + apply (rule rtrancl_refl)
1.101 + apply (blast intro: r_into_rtrancl rtrancl_trans)
1.102 + done
1.103 +
1.104 +text{*
1.105 +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline
1.106 +\isanewline
1.107 +goal\ {\isacharparenleft}lemma\ rtrancl{\isacharunderscore}converseD{\isacharparenright}{\isacharcolon}\isanewline
1.108 +{\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
1.109 +\ \isadigit{1}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}\isanewline
1.110 +\ \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
1.111 +\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}z{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}
1.112 +*}
1.113 +
1.114 +lemma rtrancl_converseI: "(y,x) \<in> r^* \<Longrightarrow> (x,y) \<in> (r^-1)^*"
1.115 + apply (erule rtrancl_induct)
1.116 + apply (rule rtrancl_refl)
1.117 + apply (blast intro: r_into_rtrancl rtrancl_trans)
1.118 + done
1.119 +
1.120 +lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
1.121 + apply (auto intro: rtrancl_converseI dest: rtrancl_converseD)
1.122 + done
1.123 +
1.124 +
1.125 +lemma "A \<subseteq> Id"
1.126 + apply (rule subsetI)
1.127 + apply (auto)
1.128 + oops
1.129 +
1.130 +text{*
1.131 +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline
1.132 +\isanewline
1.133 +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
1.134 +A\ {\isasymsubseteq}\ Id\isanewline
1.135 +\ \isadigit{1}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ Id
1.136 +
1.137 +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{2}\isanewline
1.138 +\isanewline
1.139 +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
1.140 +A\ {\isasymsubseteq}\ Id\isanewline
1.141 +\ \isadigit{1}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ A\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ b
1.142 +*}
1.143 +
1.144 +text{*questions: do we cover force? (Why not?)
1.145 +Do we include tables of operators in ASCII and X-symbol notation like in the Logics manuals?*}
1.146 +
1.147 +
1.148 +text{*rejects*}
1.149 +
1.150 +lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a"
1.151 + apply (blast)
1.152 + done
1.153 +
1.154 +text{*Pow, Inter too little used*}
1.155 +
1.156 +lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)"
1.157 + apply (simp add: psubset_def)
1.158 + done
1.159 +
1.160 +(*
1.161 +text{*
1.162 +@{thm[display]"DD"}
1.163 +\rulename{DD}
1.164 +*}
1.165 +*)
1.166 +
1.167 +end