2 theory Relations = Main:
4 ML "Pretty.setmargin 64"
6 (*Id is only used in UNITY*)
7 (*refl, antisym,trans,univalent,\<dots> ho hum*)
10 @{thm[display] Id_def[no_vars]}
15 @{thm[display] comp_def[no_vars]}
20 @{thm[display] R_O_Id[no_vars]}
25 @{thm[display] comp_mono[no_vars]}
30 @{thm[display] converse_iff[no_vars]}
31 \rulename{converse_iff}
35 @{thm[display] converse_comp[no_vars]}
36 \rulename{converse_comp}
40 @{thm[display] Image_iff[no_vars]}
45 @{thm[display] Image_UN[no_vars]}
50 @{thm[display] Domain_iff[no_vars]}
55 @{thm[display] Range_iff[no_vars]}
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}
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)
96 @{subgoals[display,indent=0,margin=65]}
98 apply (rule rtrancl_refl)
99 apply (blast intro: rtrancl_trans)
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)
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)
117 @{subgoals[display,indent=0,margin=65]}
122 @{subgoals[display,indent=0,margin=65]}
127 lemma "(\<forall>u v. (u,v) \<in> A \<longrightarrow> u=v) \<Longrightarrow> A \<subseteq> Id"
130 @{subgoals[display,indent=0,margin=65]}
136 @{subgoals[display,indent=0,margin=65]}
138 subgoals after clarify
147 lemma "(a \<in> {z. P z} \<union> {y. Q y}) = P a \<or> Q a"
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)