1theory Relations imports Main begin 2 3(*Id is only used in UNITY*) 4(*refl, antisym,trans,univalent,\<dots> ho hum*) 5 6text\<open> 7@{thm[display] Id_def[no_vars]} 8\rulename{Id_def} 9\<close> 10 11text\<open> 12@{thm[display] relcomp_unfold[no_vars]} 13\rulename{relcomp_unfold} 14\<close> 15 16text\<open> 17@{thm[display] R_O_Id[no_vars]} 18\rulename{R_O_Id} 19\<close> 20 21text\<open> 22@{thm[display] relcomp_mono[no_vars]} 23\rulename{relcomp_mono} 24\<close> 25 26text\<open> 27@{thm[display] converse_iff[no_vars]} 28\rulename{converse_iff} 29\<close> 30 31text\<open> 32@{thm[display] converse_relcomp[no_vars]} 33\rulename{converse_relcomp} 34\<close> 35 36text\<open> 37@{thm[display] Image_iff[no_vars]} 38\rulename{Image_iff} 39\<close> 40 41text\<open> 42@{thm[display] Image_UN[no_vars]} 43\rulename{Image_UN} 44\<close> 45 46text\<open> 47@{thm[display] Domain_iff[no_vars]} 48\rulename{Domain_iff} 49\<close> 50 51text\<open> 52@{thm[display] Range_iff[no_vars]} 53\rulename{Range_iff} 54\<close> 55 56text\<open> 57@{thm[display] relpow.simps[no_vars]} 58\rulename{relpow.simps} 59 60@{thm[display] rtrancl_refl[no_vars]} 61\rulename{rtrancl_refl} 62 63@{thm[display] r_into_rtrancl[no_vars]} 64\rulename{r_into_rtrancl} 65 66@{thm[display] rtrancl_trans[no_vars]} 67\rulename{rtrancl_trans} 68 69@{thm[display] rtrancl_induct[no_vars]} 70\rulename{rtrancl_induct} 71 72@{thm[display] rtrancl_idemp[no_vars]} 73\rulename{rtrancl_idemp} 74 75@{thm[display] r_into_trancl[no_vars]} 76\rulename{r_into_trancl} 77 78@{thm[display] trancl_trans[no_vars]} 79\rulename{trancl_trans} 80 81@{thm[display] trancl_into_rtrancl[no_vars]} 82\rulename{trancl_into_rtrancl} 83 84@{thm[display] trancl_converse[no_vars]} 85\rulename{trancl_converse} 86\<close> 87 88text\<open>Relations. transitive closure\<close> 89 90lemma rtrancl_converseD: "(x,y) \<in> (r\<inverse>)\<^sup>* \<Longrightarrow> (y,x) \<in> r\<^sup>*" 91apply (erule rtrancl_induct) 92txt\<open> 93@{subgoals[display,indent=0,margin=65]} 94\<close> 95 apply (rule rtrancl_refl) 96apply (blast intro: rtrancl_trans) 97done 98 99 100lemma rtrancl_converseI: "(y,x) \<in> r\<^sup>* \<Longrightarrow> (x,y) \<in> (r\<inverse>)\<^sup>*" 101apply (erule rtrancl_induct) 102 apply (rule rtrancl_refl) 103apply (blast intro: rtrancl_trans) 104done 105 106lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" 107by (auto intro: rtrancl_converseI dest: rtrancl_converseD) 108 109lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" 110apply (intro equalityI subsetI) 111txt\<open> 112after intro rules 113 114@{subgoals[display,indent=0,margin=65]} 115\<close> 116apply clarify 117txt\<open> 118after splitting 119@{subgoals[display,indent=0,margin=65]} 120\<close> 121oops 122 123 124lemma "(\<forall>u v. (u,v) \<in> A \<longrightarrow> u=v) \<Longrightarrow> A \<subseteq> Id" 125apply (rule subsetI) 126txt\<open> 127@{subgoals[display,indent=0,margin=65]} 128 129after subsetI 130\<close> 131apply clarify 132txt\<open> 133@{subgoals[display,indent=0,margin=65]} 134 135subgoals after clarify 136\<close> 137by blast 138 139 140 141 142text\<open>rejects\<close> 143 144lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a" 145apply (blast) 146done 147 148text\<open>Pow, Inter too little used\<close> 149 150lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)" 151apply (simp add: psubset_eq) 152done 153 154end 155