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

     1 (* ID:         $Id$ *)

     2 theory Relations = Main:

     4 ML "Pretty.setmargin 64"

     6 (*Id is only used in UNITY*)

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

     9 text{*

    10 @{thm[display] Id_def[no_vars]}

    11 \rulename{Id_def}

    12 *}

    14 text{*

    15 @{thm[display] comp_def[no_vars]}

    16 \rulename{comp_def}

    17 *}

    19 text{*

    20 @{thm[display] R_O_Id[no_vars]}

    21 \rulename{R_O_Id}

    22 *}

    24 text{*

    25 @{thm[display] comp_mono[no_vars]}

    26 \rulename{comp_mono}

    27 *}

    29 text{*

    30 @{thm[display] converse_iff[no_vars]}

    31 \rulename{converse_iff}

    32 *}

    34 text{*

    35 @{thm[display] converse_comp[no_vars]}

    36 \rulename{converse_comp}

    37 *}

    39 text{*

    40 @{thm[display] Image_iff[no_vars]}

    41 \rulename{Image_iff}

    42 *}

    44 text{*

    45 @{thm[display] Image_UN[no_vars]}

    46 \rulename{Image_UN}

    47 *}

    49 text{*

    50 @{thm[display] Domain_iff[no_vars]}

    51 \rulename{Domain_iff}

    52 *}

    54 text{*

    55 @{thm[display] Range_iff[no_vars]}

    56 \rulename{Range_iff}

    57 *}

    59 text{*

    60 @{thm[display] relpow.simps[no_vars]}

    61 \rulename{relpow.simps}

    63 @{thm[display] rtrancl_unfold[no_vars]}

    64 \rulename{rtrancl_unfold}

    66 @{thm[display] rtrancl_refl[no_vars]}

    67 \rulename{rtrancl_refl}

    69 @{thm[display] r_into_rtrancl[no_vars]}

    70 \rulename{r_into_rtrancl}

    72 @{thm[display] rtrancl_trans[no_vars]}

    73 \rulename{rtrancl_trans}

    75 @{thm[display] rtrancl_induct[no_vars]}

    76 \rulename{rtrancl_induct}

    78 @{thm[display] rtrancl_idemp[no_vars]}

    79 \rulename{rtrancl_idemp}

    81 @{thm[display] r_into_trancl[no_vars]}

    82 \rulename{r_into_trancl}

    84 @{thm[display] trancl_trans[no_vars]}

    85 \rulename{trancl_trans}

    87 @{thm[display] trancl_into_rtrancl[no_vars]}

    88 \rulename{trancl_into_rtrancl}

    90 @{thm[display] trancl_converse[no_vars]}

    91 \rulename{trancl_converse}

    92 *}

    94 text{*Relations.  transitive closure*}

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

    97 apply (erule rtrancl_induct)

    98 txt{*

    99 @{subgoals[display,indent=0,margin=65]}

   100 *};

   101  apply (rule rtrancl_refl)

   102 apply (blast intro: r_into_rtrancl rtrancl_trans)

   103 done

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

   107 apply (erule rtrancl_induct)

   108  apply (rule rtrancl_refl)

   109 apply (blast intro: r_into_rtrancl rtrancl_trans)

   110 done

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

   113 by (auto intro: rtrancl_converseI dest: rtrancl_converseD)

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

   116 apply (intro equalityI subsetI)

   117 txt{*

   118 after intro rules

   120 @{subgoals[display,indent=0,margin=65]}

   121 *};

   122 apply clarify

   123 txt{*

   124 after splitting

   125 @{subgoals[display,indent=0,margin=65]}

   126 *};

   127 oops

   130 lemma "(\<forall>u v. (u,v) \<in> A \<longrightarrow> u=v) \<Longrightarrow> A \<subseteq> Id"

   131 apply (rule subsetI)

   132 txt{*

   133 @{subgoals[display,indent=0,margin=65]}

   135 after subsetI

   136 *};

   137 apply clarify

   138 txt{*

   139 @{subgoals[display,indent=0,margin=65]}

   141 subgoals after clarify

   142 *};

   143 by blast

   148 text{*rejects*}

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

   151 apply (blast)

   152 done

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

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

   157 apply (simp add: psubset_def)

   158 done

   160 end

author	paulson
	Thu, 11 Jan 2001 11:35:39 +0100
changeset 10864	f0b0a125ae4b
parent 10341	6eb91805a012
child 11080	22855d091249
permissions	-rw-r--r--