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