wneuper/isa: doc-src/TutorialI/Sets/Relations.thy@2ec9c808a8a7

     1 theory Relations = Main:

     3 ML "Pretty.setmargin 64"

     5 (*Id is only used in UNITY*)

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

     8 text{*

     9 @{thm[display]"Id_def"}

    10 \rulename{Id_def}

    11 *}

    13 text{*

    14 @{thm[display]"comp_def"}

    15 \rulename{comp_def}

    16 *}

    18 text{*

    19 @{thm[display]"R_O_Id"}

    20 \rulename{R_O_Id}

    21 *}

    23 text{*

    24 @{thm[display]"comp_mono"}

    25 \rulename{comp_mono}

    26 *}

    28 text{*

    29 @{thm[display]"converse_iff"}

    30 \rulename{converse_iff}

    31 *}

    33 text{*

    34 @{thm[display]"converse_comp"}

    35 \rulename{converse_comp}

    36 *}

    38 text{*

    39 @{thm[display]"Image_iff"}

    40 \rulename{Image_iff}

    41 *}

    43 text{*

    44 @{thm[display]"Image_UN"}

    45 \rulename{Image_UN}

    46 *}

    48 text{*

    49 @{thm[display]"Domain_iff"}

    50 \rulename{Domain_iff}

    51 *}

    53 text{*

    54 @{thm[display]"Range_iff"}

    55 \rulename{Range_iff}

    56 *}

    58 text{*

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

    60 \rulename{relpow.simps}

    62 @{thm[display]"rtrancl_unfold"}

    63 \rulename{rtrancl_unfold}

    65 @{thm[display]"rtrancl_refl"}

    66 \rulename{rtrancl_refl}

    68 @{thm[display]"r_into_rtrancl"}

    69 \rulename{r_into_rtrancl}

    71 @{thm[display]"rtrancl_trans"}

    72 \rulename{rtrancl_trans}

    74 @{thm[display]"rtrancl_induct"}

    75 \rulename{rtrancl_induct}

    77 @{thm[display]"rtrancl_idemp"}

    78 \rulename{rtrancl_idemp}

    80 @{thm[display]"r_into_trancl"}

    81 \rulename{r_into_trancl}

    83 @{thm[display]"trancl_trans"}

    84 \rulename{trancl_trans}

    86 @{thm[display]"trancl_into_rtrancl"}

    87 \rulename{trancl_into_rtrancl}

    89 @{thm[display]"trancl_converse"}

    90 \rulename{trancl_converse}

    91 *}

    93 text{*Relations.  transitive closure*}

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

    96   apply (erule rtrancl_induct)

    97    apply (rule rtrancl_refl)

    98   apply (blast intro: r_into_rtrancl rtrancl_trans)

    99   done

   101 text{*

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

   103 \isanewline

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

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

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

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

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

   109 *}

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

   112   apply (erule rtrancl_induct)

   113    apply (rule rtrancl_refl)

   114   apply (blast intro: r_into_rtrancl rtrancl_trans)

   115   done

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

   118   apply (auto intro: rtrancl_converseI dest: rtrancl_converseD)

   119   done

   122 lemma "A \<subseteq> Id"

   123   apply (rule subsetI)

   124   apply (auto)

   125   oops

   127 text{*

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

   129 \isanewline

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

   131 A\ {\isasymsubseteq}\ Id\isanewline

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

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

   135 \isanewline

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

   137 A\ {\isasymsubseteq}\ Id\isanewline

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

   139 *}

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

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

   145 text{*rejects*}

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

   148   apply (blast)

   149   done

   151 text{*Pow, Inter too little used*}

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

   154   apply (simp add: psubset_def)

   155   done

   157 (*

   158 text{*

   159 @{thm[display]"DD"}

   160 \rulename{DD}

   161 *}

   162 *)

   164 end

author	paulson
	Mon, 23 Oct 2000 16:24:52 +0200
changeset 10294	2ec9c808a8a7
child 10341	6eb91805a012
permissions	-rw-r--r--