author | nipkow |
Mon, 30 May 2022 20:58:45 +0200 | |
changeset 75496 | 99b37c391433 |
parent 71393 | fce780f9c9c6 |
permissions | -rw-r--r-- |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
1 |
theory Confluence imports |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
2 |
Main |
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 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
5 |
section \<open>Confluence\<close> |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
6 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
7 |
definition semiconfluentp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
8 |
"semiconfluentp r \<longleftrightarrow> r\<inverse>\<inverse> OO r\<^sup>*\<^sup>* \<le> r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
9 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
10 |
definition confluentp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
11 |
"confluentp r \<longleftrightarrow> r\<inverse>\<inverse>\<^sup>*\<^sup>* OO r\<^sup>*\<^sup>* \<le> r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
12 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
13 |
definition strong_confluentp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
14 |
"strong_confluentp r \<longleftrightarrow> r\<inverse>\<inverse> OO r \<le> r\<^sup>*\<^sup>* OO (r\<inverse>\<inverse>)\<^sup>=\<^sup>=" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
15 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
16 |
lemma semiconfluentpI [intro?]: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
17 |
"semiconfluentp r" if "\<And>x y z. \<lbrakk> r x y; r\<^sup>*\<^sup>* x z \<rbrakk> \<Longrightarrow> \<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
18 |
using that unfolding semiconfluentp_def rtranclp_conversep by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
19 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
20 |
lemma semiconfluentpD: "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "semiconfluentp r" "r x y" "r\<^sup>*\<^sup>* x z" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
21 |
using that unfolding semiconfluentp_def rtranclp_conversep by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
22 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
23 |
lemma confluentpI: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
24 |
"confluentp r" if "\<And>x y z. \<lbrakk> r\<^sup>*\<^sup>* x y; r\<^sup>*\<^sup>* x z \<rbrakk> \<Longrightarrow> \<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
25 |
using that unfolding confluentp_def rtranclp_conversep by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
26 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
27 |
lemma confluentpD: "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "confluentp r" "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
28 |
using that unfolding confluentp_def rtranclp_conversep by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
29 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
30 |
lemma strong_confluentpI [intro?]: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
31 |
"strong_confluentp r" if "\<And>x y z. \<lbrakk> r x y; r x z \<rbrakk> \<Longrightarrow> \<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>=\<^sup>= z u" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
32 |
using that unfolding strong_confluentp_def by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
33 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
34 |
lemma strong_confluentpD: "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>=\<^sup>= z u" if "strong_confluentp r" "r x y" "r x z" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
35 |
using that unfolding strong_confluentp_def by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
36 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
37 |
lemma semiconfluentp_imp_confluentp: "confluentp r" if r: "semiconfluentp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
38 |
proof(rule confluentpI) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
39 |
show "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "r\<^sup>*\<^sup>* x y" "r\<^sup>*\<^sup>* x z" for x y z |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
40 |
using that(2,1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
41 |
by(induction arbitrary: y rule: converse_rtranclp_induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
42 |
(blast intro: rtranclp_trans dest: r[THEN semiconfluentpD])+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
43 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
44 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
45 |
lemma confluentp_imp_semiconfluentp: "semiconfluentp r" if "confluentp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
46 |
using that by(auto intro!: semiconfluentpI dest: confluentpD[OF that]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
47 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
48 |
lemma confluentp_eq_semiconfluentp: "confluentp r \<longleftrightarrow> semiconfluentp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
49 |
by(blast intro: semiconfluentp_imp_confluentp confluentp_imp_semiconfluentp) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
50 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
51 |
lemma confluentp_conv_strong_confluentp_rtranclp: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
52 |
"confluentp r \<longleftrightarrow> strong_confluentp (r\<^sup>*\<^sup>*)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
53 |
by(auto simp add: confluentp_def strong_confluentp_def rtranclp_conversep) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
54 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
55 |
lemma strong_confluentp_into_semiconfluentp: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
56 |
"semiconfluentp r" if r: "strong_confluentp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
57 |
proof |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
58 |
show "\<exists>u. r\<^sup>*\<^sup>* y u \<and> r\<^sup>*\<^sup>* z u" if "r x y" "r\<^sup>*\<^sup>* x z" for x y z |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
59 |
using that(2,1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
60 |
apply(induction arbitrary: y rule: converse_rtranclp_induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
61 |
subgoal by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
62 |
subgoal for a b c |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
63 |
by (drule (1) strong_confluentpD[OF r, of a c])(auto 10 0 intro: rtranclp_trans) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
64 |
done |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
65 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
66 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
67 |
lemma strong_confluentp_imp_confluentp: "confluentp r" if "strong_confluentp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
68 |
unfolding confluentp_eq_semiconfluentp using that by(rule strong_confluentp_into_semiconfluentp) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
69 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
70 |
lemma semiconfluentp_equivclp: "equivclp r = r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*" if r: "semiconfluentp r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
71 |
proof(rule antisym[rotated] r_OO_conversep_into_equivclp predicate2I)+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
72 |
show "(r\<^sup>*\<^sup>* OO r\<inverse>\<inverse>\<^sup>*\<^sup>*) x y" if "equivclp r x y" for x y using that unfolding equivclp_def rtranclp_conversep |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
73 |
by(induction rule: converse_rtranclp_induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
74 |
(blast elim!: symclpE intro: converse_rtranclp_into_rtranclp rtranclp_trans dest: semiconfluentpD[OF r])+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
75 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
76 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
77 |
end |