equal
deleted
inserted
replaced
46 fixes A::"('a::finite) lang" |
46 fixes A::"('a::finite) lang" |
47 assumes "regular A" |
47 assumes "regular A" |
48 shows "regular (- A)" |
48 shows "regular (- A)" |
49 proof - |
49 proof - |
50 from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode) |
50 from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode) |
51 then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def) |
51 then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_def) |
52 then show "regular (- A)" by (simp add: Myhill_Nerode) |
52 then show "regular (- A)" by (simp add: Myhill_Nerode) |
53 qed |
53 qed |
54 |
54 |
55 lemma closure_difference [intro]: |
55 lemma closure_difference [intro]: |
56 fixes A::"('a::finite) lang" |
56 fixes A::"('a::finite) lang" |