equal
deleted
inserted
replaced
47 apply(induct r) |
47 apply(induct r) |
48 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) |
48 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def) |
49 using Nil_is_append_conv apply blast |
49 using Nil_is_append_conv apply blast |
50 apply blast |
50 apply blast |
51 apply(auto) |
51 apply(auto) |
52 using Star_string by fastforce |
52 using Star_cstring |
|
53 by (metis concat_eq_Nil_conv) |
53 |
54 |
54 |
55 |
55 lemma atmostempty_correctness_aux: |
56 lemma atmostempty_correctness_aux: |
56 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
57 shows "atmostempty r \<longleftrightarrow> \<not> somechars r" |
57 apply(induct r) |
58 apply(induct r) |
76 |
77 |
77 lemma Star_atmostempty: |
78 lemma Star_atmostempty: |
78 assumes "A \<subseteq> {[]}" |
79 assumes "A \<subseteq> {[]}" |
79 shows "A\<star> \<subseteq> {[]}" |
80 shows "A\<star> \<subseteq> {[]}" |
80 using assms |
81 using assms |
81 using Star_string concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce |
82 using Star_cstring concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce |
82 |
83 |
83 lemma Star_empty_string_finite: |
84 lemma Star_empty_string_finite: |
84 shows "finite ({[]}\<star>)" |
85 shows "finite ({[]}\<star>)" |
85 using Star_atmostempty infinite_super by auto |
86 using Star_atmostempty infinite_super by auto |
86 |
87 |