equal
deleted
inserted
replaced
48 shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)" |
48 shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)" |
49 apply(induct r) |
49 apply(induct r) |
50 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) |
50 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) |
51 using Nil_is_append_conv apply blast |
51 using Nil_is_append_conv apply blast |
52 apply blast |
52 apply blast |
53 apply(auto) |
53 apply(auto) |
54 using Star_cstring |
54 by (metis Star_decomp hd_Cons_tl list.distinct(1)) |
55 by (metis concat_eq_Nil_conv) |
|
56 |
55 |
57 lemma atmostempty_correctness_aux: |
56 lemma atmostempty_correctness_aux: |
58 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
57 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
59 apply(induct r) |
58 apply(induct r) |
60 apply(simp_all) |
59 apply(simp_all) |
108 |
107 |
109 |
108 |
110 lemma Star_atmostempty: |
109 lemma Star_atmostempty: |
111 assumes "A \<subseteq> {[]}" |
110 assumes "A \<subseteq> {[]}" |
112 shows "A\<star> \<subseteq> {[]}" |
111 shows "A\<star> \<subseteq> {[]}" |
113 using assms |
112 using assms |
114 using Star_cstring concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce |
113 using Star_decomp concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD |
|
114 apply(auto) |
|
115 proof - |
|
116 fix x :: "char list" |
|
117 assume a1: "x \<in> A\<star>" |
|
118 assume "\<And>c x A. c # x \<in> A\<star> \<Longrightarrow> \<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>" |
|
119 then have f2: "\<forall>cs C c. \<exists>csa. c # csa \<in> C \<or> c # cs \<notin> C\<star>" |
|
120 by auto |
|
121 obtain cc :: "char list \<Rightarrow> char" and ccs :: "char list \<Rightarrow> char list" where |
|
122 "\<And>cs. cs = [] \<or> cc cs # ccs cs = cs" |
|
123 by (metis (no_types) list.exhaust) |
|
124 then show "x = []" |
|
125 using f2 a1 by (metis assms empty_iff insert_iff list.distinct(1) subset_singletonD) |
|
126 qed |
|
127 |
115 |
128 |
116 lemma Star_empty_string_finite: |
129 lemma Star_empty_string_finite: |
117 shows "finite ({[]}\<star>)" |
130 shows "finite ({[]}\<star>)" |
118 using Star_atmostempty infinite_super by auto |
131 using Star_atmostempty infinite_super by auto |
119 |
132 |