|
1 theory Graphs |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 lemma rtrancl_eq_trancl [simp]: |
|
6 assumes "x \<noteq> y" |
|
7 shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+" |
|
8 using assms by (metis rtrancl_eq_or_trancl) |
|
9 |
|
10 lemma trancl_split: |
|
11 "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r" |
|
12 by (induct rule:trancl_induct, auto) |
|
13 |
|
14 lemma unique_minus: |
|
15 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
|
16 and xy: "(x, y) \<in> r" |
|
17 and xz: "(x, z) \<in> r^+" |
|
18 and neq: "y \<noteq> z" |
|
19 shows "(y, z) \<in> r^+" |
|
20 by (metis converse_tranclE neq unique xy xz) |
|
21 |
|
22 lemma unique_base: |
|
23 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
|
24 and xy: "(x, y) \<in> r" |
|
25 and xz: "(x, z) \<in> r^+" |
|
26 and neq_yz: "y \<noteq> z" |
|
27 shows "(y, z) \<in> r^+" |
|
28 by (metis neq_yz unique unique_minus xy xz) |
|
29 |
|
30 lemma unique_chain_star: |
|
31 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
|
32 and xy: "(x, y) \<in> r^*" |
|
33 and xz: "(x, z) \<in> r^*" |
|
34 shows "(y, z) \<in> r^* \<or> (z, y) \<in> r^*" |
|
35 thm single_valued_confluent single_valued_def unique xy xz |
|
36 by (metis single_valued_confluent single_valued_def unique xy xz) |
|
37 |
|
38 lemma unique_chain: |
|
39 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
|
40 and xy: "(x, y) \<in> r^+" |
|
41 and xz: "(x, z) \<in> r^+" |
|
42 and neq_yz: "y \<noteq> z" |
|
43 shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" |
|
44 proof - |
|
45 have xy_star: "(x, y) \<in> r^*" |
|
46 and xz_star: "(x, z) \<in> r^*" using xy xz by simp_all |
|
47 from unique_chain_star[OF unique xy_star xz_star] |
|
48 have "(y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*" by auto |
|
49 with neq_yz |
|
50 show ?thesis by(auto) |
|
51 qed |
|
52 |
|
53 definition funof :: "[('a * 'b)set, 'a] => 'b" where |
|
54 "funof r == (\<lambda>x. THE y. (x, y) \<in> r)" |
|
55 |
|
56 lemma funof_eq: "[|single_valued r; (x, y) \<in> r|] ==> funof r x = y" |
|
57 by (simp add: funof_def single_valued_def, blast) |
|
58 |
|
59 lemma funof_Pair_in: |
|
60 "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r" |
|
61 by (force simp add: funof_eq) |
|
62 |
|
63 lemma funof_in: |
|
64 "[|r `` {x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" |
|
65 by (force simp add: funof_eq) |
|
66 |
|
67 lemma single_valuedP_update: |
|
68 shows "single_valuedP r \<Longrightarrow> single_valuedP (r(x := y))" |
|
69 oops |
|
70 |
|
71 end |