5 lemma rtrancl_eq_trancl [simp]: |
5 lemma rtrancl_eq_trancl [simp]: |
6 assumes "x \<noteq> y" |
6 assumes "x \<noteq> y" |
7 shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+" |
7 shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+" |
8 using assms by (metis rtrancl_eq_or_trancl) |
8 using assms by (metis rtrancl_eq_or_trancl) |
9 |
9 |
|
10 (* NOT NEEDED : FIXME *) |
10 lemma trancl_split: |
11 lemma trancl_split: |
11 "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r" |
12 "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r" |
12 by (induct rule:trancl_induct, auto) |
13 by (induct rule:trancl_induct, auto) |
13 |
14 |
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 |
15 |
22 lemma unique_base: |
16 section {* Single_Valuedness *} |
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 |
17 |
30 lemma unique_chain_star: |
18 lemma single_valued_Collect: |
31 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
19 assumes "single_valuedP r" |
32 and xy: "(x, y) \<in> r^*" |
20 and "inj f" |
33 and xz: "(x, z) \<in> r^*" |
21 shows "single_valued {(f x, g y) | x y. r x y}" |
34 shows "(y, z) \<in> r^* \<or> (z, y) \<in> r^*" |
22 using assms |
35 thm single_valued_confluent single_valued_def unique xy xz |
23 unfolding single_valued_def inj_on_def |
36 by (metis single_valued_confluent single_valued_def unique xy xz) |
24 apply(auto) |
|
25 done |
37 |
26 |
38 lemma unique_chain: |
27 lemma single_valued_union: |
39 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
28 assumes "single_valued r" "single_valued q" |
|
29 and "Domain r \<inter> Domain q = {}" |
|
30 shows "single_valued (r \<union> q)" |
|
31 using assms |
|
32 unfolding single_valued_def |
|
33 by auto |
|
34 |
|
35 lemma single_valuedP_update: |
|
36 assumes "single_valuedP r" |
|
37 shows "single_valuedP (r(x := y))" |
|
38 using assms |
|
39 oops |
|
40 |
|
41 lemma single_valued_confluent2: |
|
42 assumes unique: "single_valued r" |
40 and xy: "(x, y) \<in> r^+" |
43 and xy: "(x, y) \<in> r^+" |
41 and xz: "(x, z) \<in> r^+" |
44 and xz: "(x, z) \<in> r^+" |
42 and neq_yz: "y \<noteq> z" |
45 and neq_yz: "y \<noteq> z" |
43 shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" |
46 shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" |
44 proof - |
47 proof - |
45 have xy_star: "(x, y) \<in> r^*" |
48 have "(x, y) \<in> r^*" "(x, z) \<in> r^*" using xy xz by simp_all |
46 and xz_star: "(x, z) \<in> r^*" using xy xz by simp_all |
49 with single_valued_confluent[OF unique] |
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 |
50 have "(y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*" by auto |
49 with neq_yz |
51 with neq_yz |
50 show ?thesis by(auto) |
52 show "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" by simp |
51 qed |
53 qed |
|
54 |
|
55 lemmas unique_chain = single_valued_confluent2 |
|
56 |
|
57 |
52 |
58 |
53 definition funof :: "[('a * 'b)set, 'a] => 'b" where |
59 definition funof :: "[('a * 'b)set, 'a] => 'b" where |
54 "funof r == (\<lambda>x. THE y. (x, y) \<in> r)" |
60 "funof r == (\<lambda>x. THE y. (x, y) \<in> r)" |
55 |
61 |
56 lemma funof_eq: "[|single_valued r; (x, y) \<in> r|] ==> funof r x = y" |
62 lemma funof_eq: "[|single_valued r; (x, y) \<in> r|] ==> funof r x = y" |