907   fixes r::"rexp"

   907   fixes r::"rexp"

   908   shows "finite (UNIV // \<approx>(L r))"

   908   shows "finite (UNIV // \<approx>(L r))"

   909 by (induct r) (auto)

   909 by (induct r) (auto)

   910 

   910 

   911 

   911 

   912 section {* Closure properties *}

   913 section {* Closure properties *}

   913 

   914 

   914 abbreviation

   915 abbreviation

   915   reg :: "lang \<Rightarrow> bool"

   916   reg :: "lang \<Rightarrow> bool"

   916 where

   917 where

   975   moreover

   976   moreover

   976   have "reg (- ((- A) \<union> (- B)))" 

   977   have "reg (- ((- A) \<union> (- B)))" 

   977     using assms by blast

   978     using assms by blast

   978   ultimately show "reg (A \<inter> B)" by simp

   979   ultimately show "reg (A \<inter> B)" by simp

   979 qed

   980 qed

   981 

   982 

   982 end

   983 end