author | desharna |
Mon, 13 Jun 2022 20:02:00 +0200 | |
changeset 75560 | aeb797356de0 |
parent 73398 | 180981b87929 |
permissions | -rw-r--r-- |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
1 |
theory Confluent_Quotient imports |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
2 |
Confluence |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
3 |
begin |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
4 |
|
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
5 |
text \<open>Functors with finite setters preserve wide intersection for any equivalence relation that respects the mapper.\<close> |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
6 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
7 |
lemma Inter_finite_subset: |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
8 |
assumes "\<forall>A \<in> \<A>. finite A" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
9 |
shows "\<exists>\<B>\<subseteq>\<A>. finite \<B> \<and> (\<Inter>\<B>) = (\<Inter>\<A>)" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
10 |
proof(cases "\<A> = {}") |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
11 |
case False |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
12 |
then obtain A where A: "A \<in> \<A>" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
13 |
then have finA: "finite A" using assms by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
14 |
hence fin: "finite (A - \<Inter>\<A>)" by(rule finite_subset[rotated]) auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
15 |
let ?P = "\<lambda>x A. A \<in> \<A> \<and> x \<notin> A" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
16 |
define f where "f x = Eps (?P x)" for x |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
17 |
let ?\<B> = "insert A (f ` (A - \<Inter>\<A>))" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
18 |
have "?P x (f x)" if "x \<in> A - \<Inter>\<A>" for x unfolding f_def by(rule someI_ex)(use that A in auto) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
19 |
hence "(\<Inter>?\<B>) = (\<Inter>\<A>)" "?\<B> \<subseteq> \<A>" using A by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
20 |
moreover have "finite ?\<B>" using fin by simp |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
21 |
ultimately show ?thesis by blast |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
22 |
qed simp |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
23 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
24 |
locale wide_intersection_finite = |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
25 |
fixes E :: "'Fa \<Rightarrow> 'Fa \<Rightarrow> bool" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
26 |
and mapFa :: "('a \<Rightarrow> 'a) \<Rightarrow> 'Fa \<Rightarrow> 'Fa" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
27 |
and setFa :: "'Fa \<Rightarrow> 'a set" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
28 |
assumes equiv: "equivp E" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
29 |
and map_E: "E x y \<Longrightarrow> E (mapFa f x) (mapFa f y)" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
30 |
and map_id: "mapFa id x = x" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
31 |
and map_cong: "\<forall>a\<in>setFa x. f a = g a \<Longrightarrow> mapFa f x = mapFa g x" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
32 |
and set_map: "setFa (mapFa f x) = f ` setFa x" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
33 |
and finite: "finite (setFa x)" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
34 |
begin |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
35 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
36 |
lemma binary_intersection: |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
37 |
assumes "E y z" and y: "setFa y \<subseteq> Y" and z: "setFa z \<subseteq> Z" and a: "a \<in> Y" "a \<in> Z" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
38 |
shows "\<exists>x. E x y \<and> setFa x \<subseteq> Y \<and> setFa x \<subseteq> Z" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
39 |
proof - |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
40 |
let ?f = "\<lambda>b. if b \<in> Z then b else a" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
41 |
let ?u = "mapFa ?f y" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
42 |
from \<open>E y z\<close> have "E ?u (mapFa ?f z)" by(rule map_E) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
43 |
also have "mapFa ?f z = mapFa id z" by(rule map_cong)(use z in auto) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
44 |
also have "\<dots> = z" by(rule map_id) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
45 |
finally have "E ?u y" using \<open>E y z\<close> equivp_symp[OF equiv] equivp_transp[OF equiv] by blast |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
46 |
moreover have "setFa ?u \<subseteq> Y" using a y by(subst set_map) auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
47 |
moreover have "setFa ?u \<subseteq> Z" using a by(subst set_map) auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
48 |
ultimately show ?thesis by blast |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
49 |
qed |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
50 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
51 |
lemma finite_intersection: |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
52 |
assumes E: "\<forall>y\<in>A. E y z" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
53 |
and fin: "finite A" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
54 |
and sub: "\<forall>y\<in>A. setFa y \<subseteq> Y y \<and> a \<in> Y y" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
55 |
shows "\<exists>x. E x z \<and> (\<forall>y\<in>A. setFa x \<subseteq> Y y)" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
56 |
using fin E sub |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
57 |
proof(induction) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
58 |
case empty |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
59 |
then show ?case using equivp_reflp[OF equiv, of z] by(auto) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
60 |
next |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
61 |
case (insert y A) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
62 |
then obtain x where x: "E x z" "\<forall>y\<in>A. setFa x \<subseteq> Y y \<and> a \<in> Y y" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
63 |
hence set_x: "setFa x \<subseteq> (\<Inter>y\<in>A. Y y)" "a \<in> (\<Inter>y\<in>A. Y y)" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
64 |
from insert.prems have "E y z" and set_y: "setFa y \<subseteq> Y y" "a \<in> Y y" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
65 |
from \<open>E y z\<close> \<open>E x z\<close> have "E x y" using equivp_symp[OF equiv] equivp_transp[OF equiv] by blast |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
66 |
from binary_intersection[OF this set_x(1) set_y(1) set_x(2) set_y(2)] |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
67 |
obtain x' where "E x' x" "setFa x' \<subseteq> \<Inter> (Y ` A)" "setFa x' \<subseteq> Y y" by blast |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
68 |
then show ?case using \<open>E x z\<close> equivp_transp[OF equiv] by blast |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
69 |
qed |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
70 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
71 |
lemma wide_intersection: |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
72 |
assumes inter_nonempty: "\<Inter> Ss \<noteq> {}" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
73 |
shows "(\<Inter>As \<in> Ss. {(x, x'). E x x'} `` {x. setFa x \<subseteq> As}) \<subseteq> {(x, x'). E x x'} `` {x. setFa x \<subseteq> \<Inter> Ss}" (is "?lhs \<subseteq> ?rhs") |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
74 |
proof |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
75 |
fix x |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
76 |
assume lhs: "x \<in> ?lhs" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
77 |
from inter_nonempty obtain a where a: "\<forall>As \<in> Ss. a \<in> As" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
78 |
from lhs obtain y where y: "\<And>As. As \<in> Ss \<Longrightarrow> E (y As) x \<and> setFa (y As) \<subseteq> As" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
79 |
by atomize_elim(rule choice, auto) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
80 |
define Ts where "Ts = (\<lambda>As. insert a (setFa (y As))) ` Ss" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
81 |
have Ts_subset: "(\<Inter>Ts) \<subseteq> (\<Inter>Ss)" using a unfolding Ts_def by(auto dest: y) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
82 |
have Ts_finite: "\<forall>Bs \<in> Ts. finite Bs" unfolding Ts_def by(auto dest: y intro: finite) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
83 |
from Inter_finite_subset[OF this] obtain Us |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
84 |
where Us: "Us \<subseteq> Ts" and finite_Us: "finite Us" and Int_Us: "(\<Inter>Us) \<subseteq> (\<Inter>Ts)" by force |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
85 |
let ?P = "\<lambda>U As. As \<in> Ss \<and> U = insert a (setFa (y As))" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
86 |
define Y where "Y U = Eps (?P U)" for U |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
87 |
have Y: "?P U (Y U)" if "U \<in> Us" for U unfolding Y_def |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
88 |
by(rule someI_ex)(use that Us in \<open>auto simp add: Ts_def\<close>) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
89 |
let ?f = "\<lambda>U. y (Y U)" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
90 |
have *: "\<forall>z\<in>(?f ` Us). E z x" by(auto dest!: Y y) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
91 |
have **: "\<forall>z\<in>(?f ` Us). setFa z \<subseteq> insert a (setFa z) \<and> a \<in> insert a (setFa z)" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
92 |
from finite_intersection[OF * _ **] finite_Us obtain u |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
93 |
where u: "E u x" and set_u: "\<forall>z\<in>(?f ` Us). setFa u \<subseteq> insert a (setFa z)" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
94 |
from set_u have "setFa u \<subseteq> (\<Inter> Us)" by(auto dest: Y) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
95 |
with Int_Us Ts_subset have "setFa u \<subseteq> (\<Inter> Ss)" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
96 |
with u show "x \<in> ?rhs" by auto |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
97 |
qed |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
98 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
99 |
end |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
100 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
101 |
text \<open>Subdistributivity for quotients via confluence\<close> |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
102 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
103 |
lemma rtranclp_transp_reflp: "R\<^sup>*\<^sup>* = R" if "transp R" "reflp R" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
104 |
apply(rule ext iffI)+ |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
105 |
subgoal premises prems for x y using prems by(induction)(use that in \<open>auto intro: reflpD transpD\<close>) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
106 |
subgoal by(rule r_into_rtranclp) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
107 |
done |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
108 |
|
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
109 |
lemma rtranclp_equivp: "R\<^sup>*\<^sup>* = R" if "equivp R" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
110 |
using that by(simp add: rtranclp_transp_reflp equivp_reflp_symp_transp) |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
111 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
112 |
locale confluent_quotient = |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
113 |
fixes Rb :: "'Fb \<Rightarrow> 'Fb \<Rightarrow> bool" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
114 |
and Ea :: "'Fa \<Rightarrow> 'Fa \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
115 |
and Eb :: "'Fb \<Rightarrow> 'Fb \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
116 |
and Ec :: "'Fc \<Rightarrow> 'Fc \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
117 |
and Eab :: "'Fab \<Rightarrow> 'Fab \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
118 |
and Ebc :: "'Fbc \<Rightarrow> 'Fbc \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
119 |
and \<pi>_Faba :: "'Fab \<Rightarrow> 'Fa" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
120 |
and \<pi>_Fabb :: "'Fab \<Rightarrow> 'Fb" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
121 |
and \<pi>_Fbcb :: "'Fbc \<Rightarrow> 'Fb" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
122 |
and \<pi>_Fbcc :: "'Fbc \<Rightarrow> 'Fc" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
123 |
and rel_Fab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'Fa \<Rightarrow> 'Fb \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
124 |
and rel_Fbc :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'Fb \<Rightarrow> 'Fc \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
125 |
and rel_Fac :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'Fa \<Rightarrow> 'Fc \<Rightarrow> bool" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
126 |
and set_Fab :: "'Fab \<Rightarrow> ('a \<times> 'b) set" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
127 |
and set_Fbc :: "'Fbc \<Rightarrow> ('b \<times> 'c) set" |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
128 |
assumes confluent: "confluentp Rb" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
129 |
and retract1_ab: "\<And>x y. Rb (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z \<and> set_Fab z \<subseteq> set_Fab x" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
130 |
and retract1_bc: "\<And>x y. Rb (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z \<and> set_Fbc z \<subseteq> set_Fbc x" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
131 |
and generated_b: "Eb \<le> equivclp Rb" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
132 |
and transp_a: "transp Ea" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
133 |
and transp_c: "transp Ec" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
134 |
and equivp_ab: "equivp Eab" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
135 |
and equivp_bc: "equivp Ebc" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
136 |
and in_rel_Fab: "\<And>A x y. rel_Fab A x y \<longleftrightarrow> (\<exists>z. z \<in> {x. set_Fab x \<subseteq> {(x, y). A x y}} \<and> \<pi>_Faba z = x \<and> \<pi>_Fabb z = y)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
137 |
and in_rel_Fbc: "\<And>B x y. rel_Fbc B x y \<longleftrightarrow> (\<exists>z. z \<in> {x. set_Fbc x \<subseteq> {(x, y). B x y}} \<and> \<pi>_Fbcb z = x \<and> \<pi>_Fbcc z = y)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
138 |
and rel_compp: "\<And>A B. rel_Fac (A OO B) = rel_Fab A OO rel_Fbc B" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
139 |
and \<pi>_Faba_respect: "rel_fun Eab Ea \<pi>_Faba \<pi>_Faba" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
140 |
and \<pi>_Fbcc_respect: "rel_fun Ebc Ec \<pi>_Fbcc \<pi>_Fbcc" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
141 |
begin |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
142 |
|
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
143 |
lemma retract_ab: "Rb\<^sup>*\<^sup>* (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z \<and> set_Fab z \<subseteq> set_Fab x" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
144 |
by(induction rule: rtranclp_induct)(blast dest: retract1_ab intro: equivp_transp[OF equivp_ab] equivp_reflp[OF equivp_ab])+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
145 |
|
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
146 |
lemma retract_bc: "Rb\<^sup>*\<^sup>* (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z \<and> set_Fbc z \<subseteq> set_Fbc x" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
147 |
by(induction rule: rtranclp_induct)(blast dest: retract1_bc intro: equivp_transp[OF equivp_bc] equivp_reflp[OF equivp_bc])+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
148 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
149 |
lemma subdistributivity: "rel_Fab A OO Eb OO rel_Fbc B \<le> Ea OO rel_Fac (A OO B) OO Ec" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
150 |
proof(rule predicate2I; elim relcomppE) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
151 |
fix x y y' z |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
152 |
assume "rel_Fab A x y" and "Eb y y'" and "rel_Fbc B y' z" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
153 |
then obtain xy y'z |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
154 |
where xy: "set_Fab xy \<subseteq> {(a, b). A a b}" "x = \<pi>_Faba xy" "y = \<pi>_Fabb xy" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
155 |
and y'z: "set_Fbc y'z \<subseteq> {(a, b). B a b}" "y' = \<pi>_Fbcb y'z" "z = \<pi>_Fbcc y'z" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
156 |
by(auto simp add: in_rel_Fab in_rel_Fbc) |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
157 |
from \<open>Eb y y'\<close> have "equivclp Rb y y'" using generated_b by blast |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
158 |
then obtain u where u: "Rb\<^sup>*\<^sup>* y u" "Rb\<^sup>*\<^sup>* y' u" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
159 |
unfolding semiconfluentp_equivclp[OF confluent[THEN confluentp_imp_semiconfluentp]] |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
160 |
by(auto simp add: rtranclp_conversep) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
161 |
with xy y'z obtain xy' y'z' |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
162 |
where retract1: "Eab xy xy'" "\<pi>_Fabb xy' = u" "set_Fab xy' \<subseteq> set_Fab xy" |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
163 |
and retract2: "Ebc y'z y'z'" "\<pi>_Fbcb y'z' = u" "set_Fbc y'z' \<subseteq> set_Fbc y'z" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
164 |
by(auto dest!: retract_ab retract_bc) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
165 |
from retract1(1) xy have "Ea x (\<pi>_Faba xy')" by(auto dest: \<pi>_Faba_respect[THEN rel_funD]) |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
166 |
moreover have "rel_Fab A (\<pi>_Faba xy') u" using xy retract1 by(auto simp add: in_rel_Fab) |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
167 |
moreover have "rel_Fbc B u (\<pi>_Fbcc y'z')" using y'z retract2 by(auto simp add: in_rel_Fbc) |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
168 |
moreover have "Ec (\<pi>_Fbcc y'z') z" using retract2 y'z equivp_symp[OF equivp_bc] |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71393
diff
changeset
|
169 |
by(auto intro: \<pi>_Fbcc_respect[THEN rel_funD]) |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
170 |
ultimately show "(Ea OO rel_Fac (A OO B) OO Ec) x z" unfolding rel_compp by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
171 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
172 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
173 |
end |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
174 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
175 |
end |