equal
deleted
inserted
replaced
6 text {* Some properties of operator @{text "@@"}. *} |
6 text {* Some properties of operator @{text "@@"}. *} |
7 |
7 |
8 notation |
8 notation |
9 conc (infixr "\<cdot>" 100) and |
9 conc (infixr "\<cdot>" 100) and |
10 star ("_\<star>" [101] 102) |
10 star ("_\<star>" [101] 102) |
11 |
|
12 lemma conc_add_left: |
|
13 assumes a: "A = B" |
|
14 shows "C \<cdot> A = C \<cdot> B" |
|
15 using a by simp |
|
16 |
|
17 lemma star_cases: |
|
18 shows "A\<star> = {[]} \<union> A \<cdot> A\<star>" |
|
19 proof |
|
20 { fix x |
|
21 have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A \<cdot> A\<star>" |
|
22 unfolding conc_def |
|
23 by (induct rule: star_induct) (auto) |
|
24 } |
|
25 then show "A\<star> \<subseteq> {[]} \<union> A \<cdot> A\<star>" by auto |
|
26 next |
|
27 show "{[]} \<union> A \<cdot> A\<star> \<subseteq> A\<star>" |
|
28 unfolding conc_def by auto |
|
29 qed |
|
30 |
11 |
31 lemma star_decom: |
12 lemma star_decom: |
32 assumes a: "x \<in> A\<star>" "x \<noteq> []" |
13 assumes a: "x \<in> A\<star>" "x \<noteq> []" |
33 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>" |
14 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>" |
34 using a |
15 using a |
107 shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>" |
88 shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>" |
108 proof |
89 proof |
109 assume eq: "X = B \<cdot> A\<star>" |
90 assume eq: "X = B \<cdot> A\<star>" |
110 have "A\<star> = {[]} \<union> A\<star> \<cdot> A" |
91 have "A\<star> = {[]} \<union> A\<star> \<cdot> A" |
111 unfolding conc_star_comm[symmetric] |
92 unfolding conc_star_comm[symmetric] |
112 by (rule star_cases) |
93 by(metis Un_commute star_unfold_left) |
113 then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)" |
94 then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)" |
114 by (rule conc_add_left) |
95 by metis |
115 also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)" |
96 also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)" |
116 unfolding conc_Un_distrib by simp |
97 unfolding conc_Un_distrib by simp |
117 also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A" |
98 also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A" |
118 by (simp only: conc_assoc) |
99 by (simp only: conc_assoc) |
119 finally show "X = X \<cdot> A \<union> B" |
100 finally show "X = X \<cdot> A \<union> B" |