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

     1 (* ID:         $Id$ *)

     2 theory Relations imports Main begin

     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] rel_comp_def[no_vars]}

    16 \rulename{rel_comp_def}

    17 *}

    19 text{*

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

    21 \rulename{R_O_Id}

    22 *}

    24 text{*

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

    26 \rulename{rel_comp_mono}

    27 *}

    29 text{*

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

    31 \rulename{converse_iff}

    32 *}

    34 text{*

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

    36 \rulename{converse_rel_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_refl[no_vars]}

    64 \rulename{rtrancl_refl}

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

    67 \rulename{r_into_rtrancl}

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

    70 \rulename{rtrancl_trans}

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

    73 \rulename{rtrancl_induct}

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

    76 \rulename{rtrancl_idemp}

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

    79 \rulename{r_into_trancl}

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

    82 \rulename{trancl_trans}

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

    85 \rulename{trancl_into_rtrancl}

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

    88 \rulename{trancl_converse}

    89 *}

    91 text{*Relations.  transitive closure*}

    93 lemma rtrancl_converseD: "(x,y) \<in> (r\<inverse>)\<^sup>* \<Longrightarrow> (y,x) \<in> r\<^sup>*"

    94 apply (erule rtrancl_induct)

    95 txt{*

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

    97 *};

    98  apply (rule rtrancl_refl)

    99 apply (blast intro: rtrancl_trans)

   100 done

   103 lemma rtrancl_converseI: "(y,x) \<in> r\<^sup>* \<Longrightarrow> (x,y) \<in> (r\<inverse>)\<^sup>*"

   104 apply (erule rtrancl_induct)

   105  apply (rule rtrancl_refl)

   106 apply (blast intro: rtrancl_trans)

   107 done

   109 lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"

   110 by (auto intro: rtrancl_converseI dest: rtrancl_converseD)

   112 lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"

   113 apply (intro equalityI subsetI)

   114 txt{*

   115 after intro rules

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

   118 *};

   119 apply clarify

   120 txt{*

   121 after splitting

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

   123 *};

   124 oops

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

   128 apply (rule subsetI)

   129 txt{*

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

   132 after subsetI

   133 *};

   134 apply clarify

   135 txt{*

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

   138 subgoals after clarify

   139 *};

   140 by blast

   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_eq)

   155 done

   157 end

author	berghofe
	Wed, 07 May 2008 10:57:19 +0200
changeset 26806	40b411ec05aa
parent 16417	9bc16273c2d4
child 36754	403585a89772
permissions	-rw-r--r--