theory Relations = Main:

ML "Pretty.setmargin 64"

(*Id is only used in UNITY*)

(*refl, antisym,trans,univalent,\<dots> ho hum*)

text{*

@{thm[display]"Id_def"}

\rulename{Id_def}

*}

text{*

@{thm[display]"comp_def"}

\rulename{comp_def}

*}

text{*

@{thm[display]"R_O_Id"}

\rulename{R_O_Id}

*}

text{*

@{thm[display]"comp_mono"}

\rulename{comp_mono}

*}

text{*

@{thm[display]"converse_iff"}

\rulename{converse_iff}

*}

text{*

@{thm[display]"converse_comp"}

\rulename{converse_comp}

*}

text{*

@{thm[display]"Image_iff"}

\rulename{Image_iff}

*}

text{*

@{thm[display]"Image_UN"}

\rulename{Image_UN}

*}

text{*

@{thm[display]"Domain_iff"}

\rulename{Domain_iff}

*}

text{*

@{thm[display]"Range_iff"}

\rulename{Range_iff}

*}

text{*

@{thm[display]"relpow.simps"}

\rulename{relpow.simps}

@{thm[display]"rtrancl_unfold"}

\rulename{rtrancl_unfold}

@{thm[display]"rtrancl_refl"}

\rulename{rtrancl_refl}

@{thm[display]"r_into_rtrancl"}

\rulename{r_into_rtrancl}

@{thm[display]"rtrancl_trans"}

\rulename{rtrancl_trans}

@{thm[display]"rtrancl_induct"}

\rulename{rtrancl_induct}

@{thm[display]"rtrancl_idemp"}

\rulename{rtrancl_idemp}

@{thm[display]"r_into_trancl"}

\rulename{r_into_trancl}

@{thm[display]"trancl_trans"}

\rulename{trancl_trans}

@{thm[display]"trancl_into_rtrancl"}

\rulename{trancl_into_rtrancl}

@{thm[display]"trancl_converse"}

\rulename{trancl_converse}

*}

text{*Relations.  transitive closure*}

lemma rtrancl_converseD: "(x,y) \<in> (r^-1)^* \<Longrightarrow> (y,x) \<in> r^*"

  apply (erule rtrancl_induct)

   apply (rule rtrancl_refl)

  apply (blast intro: r_into_rtrancl rtrancl_trans)

  done

text{*

proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline

\isanewline

goal\ {\isacharparenleft}lemma\ rtrancl{\isacharunderscore}converseD{\isacharparenright}{\isacharcolon}\isanewline

{\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

\ \isadigit{1}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}\isanewline

\ \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

\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}z{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}

*}

lemma rtrancl_converseI: "(y,x) \<in> r^* \<Longrightarrow> (x,y) \<in> (r^-1)^*"

  apply (erule rtrancl_induct)

   apply (rule rtrancl_refl)

  apply (blast intro: r_into_rtrancl rtrancl_trans)

  done

lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"

  apply (auto intro: rtrancl_converseI dest: rtrancl_converseD)

  done

lemma "A \<subseteq> Id"

  apply (rule subsetI)

  apply (auto)

  oops

text{*

proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline

\isanewline

goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline

A\ {\isasymsubseteq}\ Id\isanewline

\ \isadigit{1}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymLongrightarrow}\ x\ {\isasymin}\ Id

proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{2}\isanewline

\isanewline

goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline

A\ {\isasymsubseteq}\ Id\isanewline

\ \isadigit{1}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ A\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ b

*}

text{*questions: do we cover force?  (Why not?)

Do we include tables of operators in ASCII and X-symbol notation like in the Logics manuals?*}

text{*rejects*}

lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a"

  apply (blast)

  done

text{*Pow, Inter too little used*}

lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)"

  apply (simp add: psubset_def)

  done

(*

text{*

@{thm[display]"DD"}

\rulename{DD}

*}

*)

end