author | wenzelm |
Sat, 26 Jun 2021 20:55:43 +0200 | |
changeset 73884 | 0a12ca4f3e8d |
parent 73398 | 180981b87929 |
permissions | -rw-r--r-- |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
1 |
theory Regex_ACI |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
2 |
imports "HOL-Library.Confluent_Quotient" |
71393
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:
71469
diff
changeset
|
5 |
datatype 'a rexp = Zero | Eps | Atom 'a | Alt "'a rexp" "'a rexp" | Conc "'a rexp" "'a rexp" | Star "'a rexp" |
71393
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 |
inductive ACI (infix "~" 64) where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
8 |
a1: "Alt (Alt r s) t ~ Alt r (Alt s t)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
9 |
| a2: "Alt r (Alt s t) ~ Alt (Alt r s) t" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
10 |
| c: "Alt r s ~ Alt s r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
11 |
| i: "r ~ Alt r r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
12 |
| R: "r ~ r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
13 |
| A: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Alt r s ~ Alt r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
14 |
| C: "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> Conc r s ~ Conc r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
15 |
| S: "r ~ r' \<Longrightarrow> Star r ~ Star r'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
16 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
17 |
declare ACI.intros[intro] |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
18 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
19 |
abbreviation ACIcl (infix "~~" 64) where "(~~) \<equiv> equivclp (~)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
20 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
21 |
lemma eq_set_preserves_inter: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
22 |
fixes eq set |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
23 |
assumes "\<And>r s. eq r s \<Longrightarrow> set r = set s" and "Ss \<noteq> {}" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
24 |
shows "(\<Inter>As\<in>Ss. {(x, x'). eq x x'} `` {x. set x \<subseteq> As}) \<subseteq> {(x, x'). eq x x'} `` {x. set x \<subseteq> \<Inter> Ss}" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
25 |
using assms by (auto simp: subset_eq) metis |
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 ACI_map_respects: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
28 |
fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
29 |
assumes "r ~ s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
30 |
shows "map_rexp f r ~ map_rexp f s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
31 |
using assms by (induct r s rule: ACI.induct) auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
32 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
33 |
lemma ACIcl_map_respects: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
34 |
fixes f :: "'a \<Rightarrow> 'b" and r s :: "'a rexp" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
35 |
assumes "r ~~ s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
36 |
shows "map_rexp f r ~~ map_rexp f s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
37 |
using assms by (induct rule: equivclp_induct) (auto intro: ACI_map_respects equivclp_trans) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
38 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
39 |
lemma ACI_set_eq: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
40 |
fixes r s :: "'a rexp" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
41 |
assumes "r ~ s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
42 |
shows "set_rexp r = set_rexp s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
43 |
using assms by (induct r s rule: ACI.induct) auto |
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 ACIcl_set_eq: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
46 |
fixes r s :: "'a rexp" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
47 |
assumes "r ~~ s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
48 |
shows "set_rexp r = set_rexp s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
49 |
using assms by (induct rule: equivclp_induct) (auto dest: ACI_set_eq) |
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 Alt_eq_map_rexp_iff: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
52 |
"Alt r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
53 |
"map_rexp f x = Alt r s \<longleftrightarrow> (\<exists>r' s'. x = Alt r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
54 |
by (cases x; auto)+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
55 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
56 |
lemma Conc_eq_map_rexp_iff: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
57 |
"Conc r s = map_rexp f x \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
58 |
"map_rexp f x = Conc r s \<longleftrightarrow> (\<exists>r' s'. x = Conc r' s' \<and> map_rexp f r' = r \<and> map_rexp f s' = s)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
59 |
by (cases x; auto)+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
60 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
61 |
lemma Star_eq_map_rexp_iff: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
62 |
"Star r = map_rexp f x \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
63 |
"map_rexp f x = Star r \<longleftrightarrow> (\<exists>r'. x = Star r' \<and> map_rexp f r' = r)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
64 |
by (cases x; auto)+ |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
65 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
66 |
lemma AA: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Alt r s ~~ Alt r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
67 |
proof (induct rule: equivclp_induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
68 |
case base |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
69 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
70 |
by (induct rule: equivclp_induct) (auto elim!: equivclp_trans) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
71 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
72 |
case (step s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
73 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
74 |
by (auto elim!: equivclp_trans) |
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 |
lemma AAA: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Alt r s) (Alt r' s')" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
78 |
proof (induct r r' rule: rtranclp.induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
79 |
case (rtrancl_refl r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
80 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
81 |
by (induct s s' rule: rtranclp.induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
82 |
(auto elim!: rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
83 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
84 |
case (rtrancl_into_rtrancl a b c) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
85 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
86 |
by (auto elim!: rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
87 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
88 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
89 |
lemma CC: "r ~~ r' \<Longrightarrow> s ~~ s' \<Longrightarrow> Conc r s ~~ Conc r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
90 |
proof (induct rule: equivclp_induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
91 |
case base |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
92 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
93 |
by (induct rule: equivclp_induct) (auto elim!: equivclp_trans) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
94 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
95 |
case (step s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
96 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
97 |
by (auto elim!: equivclp_trans) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
98 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
99 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
100 |
lemma CCC: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* s s' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Conc r s) (Conc r' s')" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
101 |
proof (induct r r' rule: rtranclp.induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
102 |
case (rtrancl_refl r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
103 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
104 |
by (induct s s' rule: rtranclp.induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
105 |
(auto elim!: rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
106 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
107 |
case (rtrancl_into_rtrancl a b c) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
108 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
109 |
by (auto elim!: rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
110 |
qed |
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 |
lemma SS: "r ~~ r' \<Longrightarrow> Star r ~~ Star r'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
113 |
proof (induct rule: equivclp_induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
114 |
case (step s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
115 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
116 |
by (auto elim!: equivclp_trans) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
117 |
qed auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
118 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
119 |
lemma SSS: "(~)\<^sup>*\<^sup>* r r' \<Longrightarrow> (~)\<^sup>*\<^sup>* (Star r) (Star r')" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
120 |
proof (induct r r' rule: rtranclp.induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
121 |
case (rtrancl_into_rtrancl a b c) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
122 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
123 |
by (auto elim!: rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
124 |
qed auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
125 |
|
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
126 |
lemma map_rexp_ACI_inv: "map_rexp f x ~ y \<Longrightarrow> \<exists>z. x ~~ z \<and> y = map_rexp f z \<and> set_rexp z \<subseteq> set_rexp x" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
127 |
proof (induct "map_rexp f x" y arbitrary: x rule: ACI.induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
128 |
case (a1 r s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
129 |
then obtain r' s' t' where "x = Alt (Alt r' s') t'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
130 |
"map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
131 |
by (auto simp: Alt_eq_map_rexp_iff) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
132 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
133 |
by (intro exI[of _ "Alt r' (Alt s' t')"]) auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
134 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
135 |
case (a2 r s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
136 |
then obtain r' s' t' where "x = Alt r' (Alt s' t')" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
137 |
"map_rexp f r' = r" "map_rexp f s' = s" "map_rexp f t' = t" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
138 |
by (auto simp: Alt_eq_map_rexp_iff) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
139 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
140 |
by (intro exI[of _ "Alt (Alt r' s') t'"]) auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
141 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
142 |
case (c r s) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
143 |
then obtain r' s' where "x = Alt r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
144 |
"map_rexp f r' = r" "map_rexp f s' = s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
145 |
by (auto simp: Alt_eq_map_rexp_iff) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
146 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
147 |
by (intro exI[of _ "Alt s' r'"]) auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
148 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
149 |
case (i r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
150 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
151 |
by (intro exI[of _ "Alt r r"]) auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
152 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
153 |
case (R r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
154 |
then show ?case by (auto intro: exI[of _ r]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
155 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
156 |
case (A r rr s ss) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
157 |
then obtain r' s' where "x = Alt r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
158 |
"map_rexp f r' = r" "map_rexp f s' = s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
159 |
by (auto simp: Alt_eq_map_rexp_iff) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
160 |
moreover from A(2)[OF this(2)[symmetric]] A(4)[OF this(3)[symmetric]] obtain rr' ss' where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
161 |
"r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'" |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
162 |
"set_rexp rr' \<subseteq> set_rexp r'" "set_rexp ss' \<subseteq> set_rexp s'" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
163 |
by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
164 |
ultimately show ?case using A(1,3) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
165 |
by (intro exI[of _ "Alt rr' ss'"]) (auto intro!: AA) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
166 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
167 |
case (C r rr s ss) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
168 |
then obtain r' s' where "x = Conc r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
169 |
"map_rexp f r' = r" "map_rexp f s' = s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
170 |
by (auto simp: Conc_eq_map_rexp_iff) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
171 |
moreover from C(2)[OF this(2)[symmetric]] C(4)[OF this(3)[symmetric]] obtain rr' ss' where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
172 |
"r' ~~ rr'" "rr = map_rexp f rr'" "s' ~~ ss'" "ss = map_rexp f ss'" |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
173 |
"set_rexp rr' \<subseteq> set_rexp r'" "set_rexp ss' \<subseteq> set_rexp s'" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
174 |
by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
175 |
ultimately show ?case using C(1,3) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
176 |
by (intro exI[of _ "Conc rr' ss'"]) (auto intro!: CC) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
177 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
178 |
case (S r rr) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
179 |
then obtain r' where "x = Star r'" "map_rexp f r' = r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
180 |
by (auto simp: Star_eq_map_rexp_iff) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
181 |
moreover from S(2)[OF this(2)[symmetric]] obtain rr' where "r' ~~ rr'" "rr = map_rexp f rr'" |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
182 |
"set_rexp rr' \<subseteq> set_rexp r'" |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
183 |
by blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
184 |
ultimately show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
185 |
by (intro exI[of _ "Star rr'"]) (auto intro!: SS) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
186 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
187 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
188 |
lemma reflclp_ACI: "(~)\<^sup>=\<^sup>= = (~)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
189 |
unfolding fun_eq_iff |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
190 |
by auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
191 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
192 |
lemma strong_confluentp_ACI: "strong_confluentp (~)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
193 |
apply (rule strong_confluentpI, unfold reflclp_ACI) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
194 |
subgoal for x y z |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
195 |
proof (induct x y arbitrary: z rule: ACI.induct) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
196 |
case (a1 r s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
197 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
198 |
by (auto intro: AAA converse_rtranclp_into_rtranclp) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
199 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
200 |
case (a2 r s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
201 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
202 |
by (auto intro: AAA converse_rtranclp_into_rtranclp) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
203 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
204 |
case (c r s) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
205 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
206 |
by (cases rule: ACI.cases) (auto intro: AAA) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
207 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
208 |
case (i r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
209 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
210 |
by (auto intro: AAA) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
211 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
212 |
case (R r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
213 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
214 |
by auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
215 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
216 |
note A1 = ACI.A[OF _ R] |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
217 |
note A2 = ACI.A[OF R] |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
218 |
case (A r r' s s') |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
219 |
from A(5,1-4) show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
220 |
proof (cases rule: ACI.cases) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
221 |
case inner: (a1 r'' s'') |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
222 |
from A(1,3) show ?thesis |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
223 |
unfolding inner |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
224 |
proof (elim ACI.cases[of _ r'], goal_cases Xa1 Xa2 XC XI XR XP XT XS) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
225 |
case (Xa1 rr ss tt) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
226 |
with A(3) show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
227 |
by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
228 |
(metis a1 a2 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
229 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
230 |
case (Xa2 r s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
231 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
232 |
by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
233 |
(metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
234 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
235 |
case (XC r s) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
236 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
237 |
by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
238 |
(metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
239 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
240 |
case (XI r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
241 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
242 |
apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF i ACI.A[OF i]]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
243 |
apply hypsubst |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
244 |
apply (rule converse_rtranclp_into_rtranclp, rule a1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
245 |
apply (rule converse_rtranclp_into_rtranclp, rule a1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
246 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
247 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
248 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
249 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
250 |
apply (rule converse_rtranclp_into_rtranclp, rule a2) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
251 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
252 |
apply blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
253 |
done |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
254 |
qed auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
255 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
256 |
case inner: (a2 s'' t'') |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
257 |
with A(1,3) show ?thesis |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
258 |
unfolding inner |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
259 |
proof (elim ACI.cases[of _ s'], goal_cases Xa1 Xa2 XC XI XR XP XT XS) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
260 |
case (Xa1 rr ss tt) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
261 |
with A(3) show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
262 |
by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
263 |
(metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
264 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
265 |
case (Xa2 r s t) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
266 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
267 |
by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
268 |
(metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
269 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
270 |
case (XC r s) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
271 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
272 |
by (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
273 |
(metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
274 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
275 |
case (XI r) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
276 |
then show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
277 |
apply (elim exI[where P = "\<lambda>x. _ x \<and> _ ~ x", OF conjI[OF _ ACI.A[OF ACI.A[OF _ i] i]], rotated]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
278 |
apply hypsubst |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
279 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
280 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
281 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
282 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
283 |
apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
284 |
apply (rule converse_rtranclp_into_rtranclp, rule a2) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
285 |
apply blast |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
286 |
done |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
287 |
qed auto |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
288 |
qed (auto 5 0 intro: AAA) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
289 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
290 |
case (C r r' s s') |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
291 |
from C(5,1-4) show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
292 |
by (cases rule: ACI.cases) (auto 5 0 intro: CCC) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
293 |
next |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
294 |
case (S r r') |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
295 |
from S(3,1,2) show ?case |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
296 |
by (cases rule: ACI.cases) (auto intro: SSS) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
297 |
qed |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
298 |
done |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
299 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
300 |
lemma confluent_quotient_ACI: |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
301 |
"confluent_quotient (~) (~~) (~~) (~~) (~~) (~~) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
302 |
(map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
303 |
rel_rexp rel_rexp rel_rexp set_rexp set_rexp" |
73398
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
304 |
by unfold_locales (auto dest: ACIcl_set_eq ACIcl_map_respects simp: rexp.in_rel rexp.rel_compp map_rexp_ACI_inv |
180981b87929
generalized confluence-based subdistributivity theorem for quotients;
traytel
parents:
71469
diff
changeset
|
305 |
intro: equivpI reflpI sympI transpI |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
306 |
strong_confluentp_imp_confluentp[OF strong_confluentp_ACI]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
307 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
308 |
inductive ACIEQ (infix "\<approx>" 64) where |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
309 |
a: "Alt (Alt r s) t \<approx> Alt r (Alt s t)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
310 |
| c: "Alt r s \<approx> Alt s r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
311 |
| i: "Alt r r \<approx> r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
312 |
| A: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Alt r s \<approx> Alt r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
313 |
| C: "r \<approx> r' \<Longrightarrow> s \<approx> s' \<Longrightarrow> Conc r s \<approx> Conc r' s'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
314 |
| S: "r \<approx> r' \<Longrightarrow> Star r \<approx> Star r'" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
315 |
| r: "r \<approx> r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
316 |
| s: "r \<approx> s \<Longrightarrow> s \<approx> r" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
317 |
| t: "r \<approx> s \<Longrightarrow> s \<approx> t \<Longrightarrow> r \<approx> t" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
318 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
319 |
lemma ACIEQ_le_ACIcl: "r \<approx> s \<Longrightarrow> r ~~ s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
320 |
by (induct r s rule: ACIEQ.induct) (auto intro: AA CC SS equivclp_sym equivclp_trans) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
321 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
322 |
lemma ACI_le_ACIEQ: "r ~ s \<Longrightarrow> r \<approx> s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
323 |
by (induct r s rule: ACI.induct) (auto intro: ACIEQ.intros) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
324 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
325 |
lemma ACIcl_le_ACIEQ: "r ~~ s \<Longrightarrow> r \<approx> s" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
326 |
by (induct rule: equivclp_induct) (auto 0 3 intro: ACIEQ.intros ACI_le_ACIEQ) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
327 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
328 |
lemma ACIEQ_alt: "(\<approx>) = (~~)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
329 |
by (simp add: ACIEQ_le_ACIcl ACIcl_le_ACIEQ antisym predicate2I) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
330 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
331 |
quotient_type 'a ACI_rexp = "'a rexp" / "(\<approx>)" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
332 |
unfolding ACIEQ_alt by (auto intro!: equivpI reflpI sympI transpI) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
333 |
|
71469
d7ef73df3d15
lift BNF witnesses for quotients (unless better ones are specified by the user)
traytel
parents:
71393
diff
changeset
|
334 |
lift_bnf 'a ACI_rexp |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
335 |
unfolding ACIEQ_alt |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
336 |
subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI]) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
337 |
subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto) |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
338 |
done |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
339 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
340 |
datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp" |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
341 |
|
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
diff
changeset
|
342 |
end |