term "TYPE (nat * int)"

term "TYPE ('a)"

definition

  P:: "'a itself \<Rightarrow> bool"

where

  "P (TYPE ('a)) \<equiv> ((\<lambda>x. (x::'a)) = (\<lambda>x. x))"

definition

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

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

text {* Two Simple Properties about Sequential Composition *}

lemma seq_empty [simp]:

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

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

by (simp_all add: Seq_def)

lemma seq_null [simp]:

  shows "A ;; {} = {}"

  and   "{} ;; A = {}"

by (simp_all add: Seq_def)

  for A :: "string set"

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

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

text {* A Standard Property of Star *}

lemma star_cases:

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

unfolding Seq_def

by (auto) (metis Star.simps)

lemma star_decomp: 

  assumes a: "c # x \<in> A\<star>" 

  shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"

using a

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

   (auto simp add: append_eq_Cons_conv)

section {* Left-Quotient of a Set *}

definition

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

where

  "Der c A \<equiv> {s. [c] @ s \<in> A}"

lemma Der_null [simp]:

  shows "Der c {} = {}"

unfolding Der_def

by auto

lemma Der_empty [simp]:

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

unfolding Der_def

by auto

lemma Der_char [simp]:

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

unfolding Der_def

by auto

lemma Der_union [simp]:

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

unfolding Der_def

by auto

lemma Der_seq [simp]:

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

unfolding Der_def Seq_def

by (auto simp add: Cons_eq_append_conv)

lemma Der_star [simp]:

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

proof -    

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

    by (simp only: star_cases[symmetric])

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

    by (simp only: Der_union Der_empty) (simp)

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

    by simp

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

    unfolding Seq_def Der_def

    by (auto dest: star_decomp)

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

qed

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

  matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"

  "matcher r s = nullable (derivative s r)"

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

by (induct r) (auto simp add: Seq_def) 

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

by (induct r) 

   (simp_all add: nullable_correctness)

lemma matcher_correctness:

  shows "matcher r s \<longleftrightarrow> s \<in> L r"

   (simp_all add: nullable_correctness der_correctness Der_def)

value "matcher NULL []"

value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"

value "matcher (CHAR a) [a,a]"

value "matcher (STAR (CHAR a)) []"

value "matcher (STAR (CHAR a))  [a,a]"

value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"

value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"

fun