equal
deleted
inserted
replaced
32 assumes a: "x \<in> A\<star>" "x \<noteq> []" |
32 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>" |
33 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>" |
34 using a |
34 using a |
35 by (induct rule: star_induct) (blast)+ |
35 by (induct rule: star_induct) (blast)+ |
36 |
36 |
37 lemma seq_pow_comm: |
37 lemma conc_pow_comm: |
38 shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A" |
38 shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A" |
39 by (induct n) (simp_all add: conc_assoc[symmetric]) |
39 by (induct n) (simp_all add: conc_assoc[symmetric]) |
40 |
40 |
41 lemma seq_star_comm: |
41 lemma conc_star_comm: |
42 shows "A \<cdot> A\<star> = A\<star> \<cdot> A" |
42 shows "A \<cdot> A\<star> = A\<star> \<cdot> A" |
43 unfolding star_def seq_pow_comm conc_UNION_distrib |
43 unfolding star_def conc_pow_comm conc_UNION_distrib |
44 by simp |
44 by simp |
45 |
45 |
46 |
46 |
47 text {* Two lemmas about the length of strings in @{text "A \<up> n"} *} |
47 text {* Two lemmas about the length of strings in @{text "A \<up> n"} *} |
48 |
48 |
66 moreover have "0 < length s1" using * a by auto |
66 moreover have "0 < length s1" using * a by auto |
67 ultimately show "Suc n < length s" unfolding eq |
67 ultimately show "Suc n < length s" unfolding eq |
68 by (simp only: length_append) |
68 by (simp only: length_append) |
69 qed |
69 qed |
70 |
70 |
71 lemma seq_pow_length: |
71 lemma conc_pow_length: |
72 assumes a: "[] \<notin> A" |
72 assumes a: "[] \<notin> A" |
73 and b: "s \<in> B \<cdot> (A ^^ Suc n)" |
73 and b: "s \<in> B \<cdot> (A ^^ Suc n)" |
74 shows "n < length s" |
74 shows "n < length s" |
75 proof - |
75 proof - |
76 from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n" |
76 from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n" |
77 unfolding Seq_def by auto |
77 by auto |
78 from * have " n < length s2" by (rule pow_length[OF a]) |
78 from * have " n < length s2" by (rule pow_length[OF a]) |
79 then show "n < length s" using eq by simp |
79 then show "n < length s" using eq by simp |
80 qed |
80 qed |
81 |
81 |
82 |
82 |
106 assumes nemp: "[] \<notin> A" |
106 assumes nemp: "[] \<notin> A" |
107 shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>" |
107 shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>" |
108 proof |
108 proof |
109 assume eq: "X = B \<cdot> A\<star>" |
109 assume eq: "X = B \<cdot> A\<star>" |
110 have "A\<star> = {[]} \<union> A\<star> \<cdot> A" |
110 have "A\<star> = {[]} \<union> A\<star> \<cdot> A" |
111 unfolding seq_star_comm[symmetric] |
111 unfolding conc_star_comm[symmetric] |
112 by (rule star_cases) |
112 by (rule star_cases) |
113 then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)" |
113 then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)" |
114 by (rule conc_add_left) |
114 by (rule conc_add_left) |
115 also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)" |
115 also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)" |
116 unfolding conc_Un_distrib by simp |
116 unfolding conc_Un_distrib by simp |
126 unfolding conc_def star_def UNION_def by auto |
126 unfolding conc_def star_def UNION_def by auto |
127 moreover |
127 moreover |
128 { fix s::"'a list" |
128 { fix s::"'a list" |
129 obtain k where "k = length s" by auto |
129 obtain k where "k = length s" by auto |
130 then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)" |
130 then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)" |
131 using seq_pow_length[OF nemp] by blast |
131 using conc_pow_length[OF nemp] by blast |
132 assume "s \<in> X" |
132 assume "s \<in> X" |
133 then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" |
133 then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" |
134 using arden_helper[OF eq, of "k"] by auto |
134 using arden_helper[OF eq, of "k"] by auto |
135 then have "s \<in> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using not_in by auto |
135 then have "s \<in> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using not_in by auto |
136 moreover |
136 moreover |