1 theory RegLangs

     2   imports Main "HOL-Library.Sublist"

     3 begin

     4 

     5 section \<open>Sequential Composition of Languages\<close>

     6 

     7 definition

     8   Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)

     9 where 

    10   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"

    11 

    12 text \<open>Two Simple Properties about Sequential Composition\<close>

    13 

    14 lemma Sequ_empty_string [simp]:

    15   shows "A ;; {[]} = A"

    16   and   "{[]} ;; A = A"

    17 by (simp_all add: Sequ_def)

    18 

    19 lemma Sequ_empty [simp]:

    20   shows "A ;; {} = {}"

    21   and   "{} ;; A = {}"

    22   by (simp_all add: Sequ_def)

    23 

    24 lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A ;; B"

    25 by (auto simp add: Sequ_def)

    26 

    27 lemma concE[elim]: 

    28 assumes "w \<in> A ;; B"

    29 obtains u v where "u \<in> A" "v \<in> B" "w = u@v"

    30 using assms by (auto simp: Sequ_def)

    31 

    32 lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs : A \<Longrightarrow> xs \<in> A ;; B"

    33 by (metis append_Nil2 concI)

    34 

    35 lemma conc_assoc: "(A ;; B) ;; C = A ;; (B ;; C)"

    36 by (auto elim!: concE) (simp only: append_assoc[symmetric] concI)

    37 

    38 

    39 text \<open>Language power operations\<close>

    40 

    41 overloading lang_pow == "compow :: nat \<Rightarrow> string set \<Rightarrow> string set"

    42 begin

    43   primrec lang_pow :: "nat \<Rightarrow> string set \<Rightarrow> string set" where

    44   "lang_pow 0 A = {[]}" |

    45   "lang_pow (Suc n) A = A ;; (lang_pow n A)"

    46 end

    47 

    48 

    49 lemma conc_pow_comm:

    50   shows "A ;; (A ^^ n) = (A ^^ n) ;; A"

    51 by (induct n) (simp_all add: conc_assoc[symmetric])

    52 

    53 lemma lang_pow_add: "A ^^ (n + m) = (A ^^ n) ;; (A ^^ m)"

    54   by (induct n) (auto simp: conc_assoc)

    55 

    56 lemma lang_empty: 

    57   fixes A::"string set"

    58   shows "A ^^ 0 = {[]}"

    59   by simp

    60 

    61 section \<open>Semantic Derivative (Left Quotient) of Languages\<close>

    62 

    63 definition

    64   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"

    65 where

    66   "Der c A \<equiv> {s. c # s \<in> A}"

    67 

    68 definition

    69   Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"

    70 where

    71   "Ders s A \<equiv> {s'. s @ s' \<in> A}"

    72 

    73 lemma Der_null [simp]:

    74   shows "Der c {} = {}"

    75 unfolding Der_def

    76 by auto

    77 

    78 lemma Der_empty [simp]:

    79   shows "Der c {[]} = {}"

    80 unfolding Der_def

    81 by auto

    82 

    83 lemma Der_char [simp]:

    84   shows "Der c {[d]} = (if c = d then {[]} else {})"

    85 unfolding Der_def

    86 by auto

    87 

    88 lemma Der_union [simp]:

    89   shows "Der c (A \<union> B) = Der c A \<union> Der c B"

    90 unfolding Der_def

    91 by auto

    92 

    93 lemma Der_Sequ [simp]:

    94   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"

    95 unfolding Der_def Sequ_def

    96 by (auto simp add: Cons_eq_append_conv)

    97 

    98 

    99 section \<open>Kleene Star for Languages\<close>

   100 

   101 inductive_set

   102   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

   103   for A :: "string set"

   104 where

   105   start[intro]: "[] \<in> A\<star>"

   106 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"

   107 

   108 (* Arden's lemma *)

   109 

   110 lemma Star_cases:

   111   shows "A\<star> = {[]} \<union> A ;; A\<star>"

   112 unfolding Sequ_def

   113 by (auto) (metis Star.simps)

   114 

   115 lemma Star_decomp: 

   116   assumes "c # x \<in> A\<star>" 

   117   shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"

   118 using assms

   119 by (induct x\<equiv>"c # x" rule: Star.induct) 

   120    (auto simp add: append_eq_Cons_conv)

   121 

   122 lemma Star_Der_Sequ: 

   123   shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"

   124 unfolding Der_def Sequ_def

   125 by(auto simp add: Star_decomp)

   126 

   127 lemma Der_inter[simp]:   "Der a (A \<inter> B) = Der a A \<inter> Der a B"

   128   and Der_compl[simp]:   "Der a (-A) = - Der a A"

   129   and Der_Union[simp]:   "Der a (Union M) = Union(Der a ` M)"

   130   and Der_UN[simp]:      "Der a (UN x:I. S x) = (UN x:I. Der a (S x))"

   131 by (auto simp: Der_def)

   132 

   133 lemma Der_star[simp]:

   134   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"

   135 proof -    

   136   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  

   137     by (simp only: Star_cases[symmetric])

   138   also have "... = Der c (A ;; A\<star>)"

   139     by (simp only: Der_union Der_empty) (simp)

   140   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"

   141     by simp

   142   also have "... =  (Der c A) ;; A\<star>"

   143     using Star_Der_Sequ by auto

   144   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .

   145 qed

   146 

   147 lemma Der_pow[simp]:

   148   shows "Der c (A ^^ n) = (if n = 0 then {} else (Der c A) ;; (A ^^ (n - 1)))"

   149   apply(induct n arbitrary: A)

   150    apply(auto simp add: Cons_eq_append_conv)

   151   by (metis Suc_pred concI_if_Nil2 conc_assoc conc_pow_comm lang_pow.simps(2))

   152 

   153 

   154 lemma Star_concat:

   155   assumes "\<forall>s \<in> set ss. s \<in> A"  

   156   shows "concat ss \<in> A\<star>"

   157 using assms by (induct ss) (auto)

   158 

   159 lemma Star_split:

   160   assumes "s \<in> A\<star>"

   161   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])"

   162 using assms

   163   apply(induct rule: Star.induct)

   164   using concat.simps(1) apply fastforce

   165   apply(clarify)

   166   by (metis append_Nil concat.simps(2) set_ConsD)

   167 

   168 

   169 

   170 

   171 section \<open>Regular Expressions\<close>

   172 

   173 datatype rexp =

   174   ZERO

   175 | ONE

   176 | CH char

   177 | SEQ rexp rexp

   178 | ALT rexp rexp

   179 | STAR rexp

   180 | NTIMES rexp nat

   181 

   182 section \<open>Semantics of Regular Expressions\<close>

   183  

   184 fun

   185   L :: "rexp \<Rightarrow> string set"

   186 where

   187   "L (ZERO) = {}"

   188 | "L (ONE) = {[]}"

   189 | "L (CH c) = {[c]}"

   190 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"

   191 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"

   192 | "L (STAR r) = (L r)\<star>"

   193 | "L (NTIMES r n) = (L r) ^^ n"

   194 

   195 section \<open>Nullable, Derivatives\<close>

   196 

   197 fun

   198  nullable :: "rexp \<Rightarrow> bool"

   199 where

   200   "nullable (ZERO) = False"

   201 | "nullable (ONE) = True"

   202 | "nullable (CH c) = False"

   203 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"

   204 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"

   205 | "nullable (STAR r) = True"

   206 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"

   207 

   208 fun

   209  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"

   210 where

   211   "der c (ZERO) = ZERO"

   212 | "der c (ONE) = ZERO"

   213 | "der c (CH d) = (if c = d then ONE else ZERO)"

   214 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

   215 | "der c (SEQ r1 r2) = 

   216      (if nullable r1

   217       then ALT (SEQ (der c r1) r2) (der c r2)

   218       else SEQ (der c r1) r2)"

   219 | "der c (STAR r) = SEQ (der c r) (STAR r)"

   220 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))"

   221 

   222 

   223 fun 

   224  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"

   225 where

   226   "ders [] r = r"

   227 | "ders (c # s) r = ders s (der c r)"

   228 

   229 

   230 lemma pow_empty_iff:

   231   shows "[] \<in> (L r) ^^ n \<longleftrightarrow> (if n = 0 then True else [] \<in> (L r))"

   232   by (induct n) (auto simp add: Sequ_def)

   233 

   234 lemma nullable_correctness:

   235   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"

   236   by (induct r) (auto simp add: Sequ_def pow_empty_iff) 

   237 

   238 lemma der_correctness:

   239   shows "L (der c r) = Der c (L r)"

   240   apply (induct r) 

   241         apply(auto simp add: nullable_correctness Sequ_def)

   242   using Der_def apply force

   243   using Der_def apply auto[1]

   244   apply (smt (verit, ccfv_SIG) Der_def append_eq_Cons_conv mem_Collect_eq)

   245   using Der_def apply force

   246   using Der_Sequ Sequ_def by auto

   247 

   248 lemma ders_correctness:

   249   shows "L (ders s r) = Ders s (L r)"

   250   by (induct s arbitrary: r)

   251      (simp_all add: Ders_def der_correctness Der_def)

   252 

   253 lemma ders_append:

   254   shows "ders (s1 @ s2) r = ders s2 (ders s1 r)"

   255   by (induct s1 arbitrary: s2 r) (auto)

   256 

   257 lemma ders_snoc:

   258   shows "ders (s @ [c]) r = der c (ders s r)"

   259   by (simp add: ders_append)

   260 

   261 

   262 end