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 

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

    26 

    27 definition

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

    29 where

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

    31 

    32 definition

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

    34 where

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

    36 

    37 lemma Der_null [simp]:

    38   shows "Der c {} = {}"

    39 unfolding Der_def

    40 by auto

    41 

    42 lemma Der_empty [simp]:

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

    44 unfolding Der_def

    45 by auto

    46 

    47 lemma Der_char [simp]:

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

    49 unfolding Der_def

    50 by auto

    51 

    52 lemma Der_union [simp]:

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

    54 unfolding Der_def

    55 by auto

    56 

    57 lemma Der_Sequ [simp]:

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

    59 unfolding Der_def Sequ_def

    60 by (auto simp add: Cons_eq_append_conv)

    61 

    62 

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

    64 

    65 inductive_set

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

    67   for A :: "string set"

    68 where

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

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

    71 

    72 (* Arden's lemma *)

    73 

    74 lemma Star_cases:

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

    76 unfolding Sequ_def

    77 by (auto) (metis Star.simps)

    78 

    79 lemma Star_decomp: 

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

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

    82 using assms

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

    84    (auto simp add: append_eq_Cons_conv)

    85 

    86 lemma Star_Der_Sequ: 

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

    88 unfolding Der_def Sequ_def

    89 by(auto simp add: Star_decomp)

    90 

    91 

    92 lemma Der_star[simp]:

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

    94 proof -    

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

    96     by (simp only: Star_cases[symmetric])

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

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

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

   100     by simp

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

   102     using Star_Der_Sequ by auto

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

   104 qed

   105 

   106 lemma Star_concat:

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

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

   109 using assms by (induct ss) (auto)

   110 

   111 lemma Star_split:

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

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

   114 using assms

   115   apply(induct rule: Star.induct)

   116   using concat.simps(1) apply fastforce

   117   apply(clarify)

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

   119 

   120 

   121 

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

   123 

   124 datatype rexp =

   125   ZERO

   126 | ONE

   127 | CH char

   128 | SEQ rexp rexp

   129 | ALT rexp rexp

   130 | STAR rexp

   131 

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

   133  

   134 fun

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

   136 where

   137   "L (ZERO) = {}"

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

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

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

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

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

   143 

   144 

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

   146 

   147 fun

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

   149 where

   150   "nullable (ZERO) = False"

   151 | "nullable (ONE) = True"

   152 | "nullable (CH c) = False"

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

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

   155 | "nullable (STAR r) = True"

   156 

   157 

   158 fun

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

   160 where

   161   "der c (ZERO) = ZERO"

   162 | "der c (ONE) = ZERO"

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

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

   165 | "der c (SEQ r1 r2) = 

   166      (if nullable r1

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

   168       else SEQ (der c r1) r2)"

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

   170 

   171 fun 

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

   173 where

   174   "ders [] r = r"

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

   176 

   177 

   178 lemma nullable_correctness:

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

   180 by (induct r) (auto simp add: Sequ_def) 

   181 

   182 lemma der_correctness:

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

   184 by (induct r) (simp_all add: nullable_correctness)

   185 

   186 lemma ders_correctness:

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

   188   by (induct s arbitrary: r)

   189      (simp_all add: Ders_def der_correctness Der_def)

   190 

   191 lemma ders_append:

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

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

   194 

   195 lemma ders_snoc:

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

   197   by (simp add: ders_append)

   198 

   199 

   200 (*

   201 datatype ctxt = 

   202     SeqC rexp bool

   203   | AltCL rexp

   204   | AltCH rexp 

   205   | StarC rexp 

   206 

   207 function

   208      down :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"

   209 and  up :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"

   210 where

   211   "down c (SEQ r1 r2) ctxts =

   212      (if (nullable r1) then down c r1 (SeqC r2 True # ctxts) 

   213       else down c r1 (SeqC r2 False # ctxts))"

   214 | "down c (CH d) ctxts = 

   215      (if c = d then up c ONE ctxts else up c ZERO ctxts)"

   216 | "down c ONE ctxts = up c ZERO ctxts"

   217 | "down c ZERO ctxts = up c ZERO ctxts"

   218 | "down c (ALT r1 r2) ctxts = down c r1 (AltCH r2 # ctxts)"

   219 | "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)"

   220 | "up c r [] = (r, [])"

   221 | "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts"

   222 | "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)"

   223 | "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts"

   224 | "up c r (AltCH r2 # ctxts) = down c r2 (AltCL r # ctxts)"

   225 | "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts"

   226   apply(pat_completeness)

   227   apply(auto)

   228   done

   229 

   230 termination

   231   sorry

   232 

   233 *)

   234 

   235 

   236 end