imports "Main" 

begin

text {* sequential composition of languages *}

definition

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

where 

  "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"

lemma lang_seq_empty:

  shows "{[]} ; L = L"

  and   "L ; {[]} = L"

unfolding lang_seq_def by auto

lemma lang_seq_null:

  shows "{} ; L = {}"

  and   "L ; {} = {}"

unfolding lang_seq_def by auto

lemma lang_seq_append:

  assumes a: "s1 \<in> L1"

  and     b: "s2 \<in> L2"

  shows "s1@s2 \<in> L1 ; L2"

unfolding lang_seq_def

using a b by auto 

lemma lang_seq_union:

  shows "(L1 \<union> L2); L3 = (L1; L3) \<union> (L2; L3)"

  and   "L1; (L2 \<union> L3) = (L1; L2) \<union> (L1; L3)"

unfolding lang_seq_def by auto

lemma lang_seq_assoc:

  shows "(L1 ; L2) ; L3 = L1 ; (L2 ; L3)"

by (simp add: lang_seq_def Collect_def mem_def expand_fun_eq)

   (metis append_assoc)

lemma lang_seq_minus:

  shows "(L1; L2) - {[]} =

           (if [] \<in> L1 then L2 - {[]} else {}) \<union> 

           (if [] \<in> L2 then L1 - {[]} else {}) \<union> ((L1 - {[]}); (L2 - {[]}))"

apply(auto simp add: lang_seq_def)

apply(metis mem_def self_append_conv)

apply(metis mem_def self_append_conv2)

apply(metis mem_def self_append_conv2)

apply(metis mem_def self_append_conv)

done

section {* Kleene star for languages defined as least fixed point *}

inductive_set

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

  for L :: "string set"

where

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

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

lemma lang_star_empty:

  shows "{}\<star> = {[]}"

by (auto elim: Star.cases)

lemma lang_star_cases:

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

proof

  { fix x

    have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"

      unfolding lang_seq_def

    by (induct rule: Star.induct) (auto)

  }

  then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto

next

  show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>" 

    unfolding lang_seq_def by auto

qed

lemma lang_star_cases':

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

proof

  { fix x

    have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L\<star> ; L"

      unfolding lang_seq_def

    apply (induct rule: Star.induct)

    apply simp

    apply simp

    apply (erule disjE)

    apply (auto)[1]

    apply (erule exE | erule conjE)+

    apply (rule disjI2)

    apply (rule_tac x = "s1 @ s1a" in exI)

    by auto

  }

  then show "L\<star> \<subseteq> {[]} \<union> L\<star> ; L" by auto

next

  show "{[]} \<union> L\<star> ; L \<subseteq> L\<star>" 

    unfolding lang_seq_def

    apply auto

    apply (erule Star.induct)

    apply auto

    apply (drule step[of _ _ "[]"])

    by (auto intro:start)

qed

lemma lang_star_simple:

  shows "L \<subseteq> L\<star>"

by (subst lang_star_cases)

   (auto simp only: lang_seq_def)

lemma lang_star_prop0_aux:

  "s2 \<in> L\<star> \<Longrightarrow> \<forall> s1. s1 \<in> L \<longrightarrow> (\<exists> s3 s4. s3 \<in> L\<star> \<and> s4 \<in> L \<and> s1 @ s2 = s3 @ s4)" 

apply (erule Star.induct)

apply (clarify, rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start)

apply (clarify, drule_tac x = s1 in spec)

apply (drule mp, simp, clarify)

apply (rule_tac x = "s1a @ s3" in exI, rule_tac x = s4 in exI)

by auto

lemma lang_star_prop0:

  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> \<exists> s3 s4. s3 \<in> L\<star> \<and> s4 \<in> L \<and> s1 @ s2 = s3 @ s4" 

by (auto dest:lang_star_prop0_aux)

lemma lang_star_prop1:

  assumes asm: "L1; L2 \<subseteq> L2" 

  shows "L1\<star>; L2 \<subseteq> L2"

proof -

  { fix s1 s2

    assume minor: "s2 \<in> L2"

    assume major: "s1 \<in> L1\<star>"

    then have "s1@s2 \<in> L2"

    proof(induct rule: Star.induct)

      case start

      show "[]@s2 \<in> L2" using minor by simp

    next

      case (step s1 s1')

      have "s1 \<in> L1" by fact

      moreover

      have "s1'@s2 \<in> L2" by fact

      ultimately have "s1@(s1'@s2) \<in> L1; L2" by (auto simp add: lang_seq_def)

      with asm have "s1@(s1'@s2) \<in> L2" by auto

      then show "(s1@s1')@s2 \<in> L2" by simp

    qed

  } 

  then show "L1\<star>; L2 \<subseteq> L2" by (auto simp add: lang_seq_def)

qed

lemma lang_star_prop2_aux:

  "s2 \<in> L2\<star> \<Longrightarrow> \<forall> s1. s1 \<in> L1 \<and> L1 ; L2 \<subseteq> L1 \<longrightarrow> s1 @ s2 \<in> L1"

apply (erule Star.induct, simp)

apply (clarify, drule_tac x = "s1a @ s1" in spec)

by (auto simp:lang_seq_def)

lemma lang_star_prop2:

  "L1; L2 \<subseteq> L1 \<Longrightarrow> L1 ; L2\<star> \<subseteq> L1"

by (auto dest!:lang_star_prop2_aux simp:lang_seq_def)

lemma lang_star_seq_subseteq: 

  shows "L ; L\<star> \<subseteq> L\<star>"

using lang_star_cases by blast

lemma lang_star_double:

  shows "L\<star>; L\<star> = L\<star>"

proof

  show "L\<star> ; L\<star> \<subseteq> L\<star>" 

    using lang_star_prop1 lang_star_seq_subseteq by blast

next

  have "L\<star> \<subseteq> L\<star> \<union> L\<star>; (L; L\<star>)" by auto

  also have "\<dots> = L\<star>;{[]} \<union> L\<star>; (L; L\<star>)" by (simp add: lang_seq_empty)

  also have "\<dots> = L\<star>; ({[]} \<union> L; L\<star>)" by (simp only: lang_seq_union)

  also have "\<dots> = L\<star>; L\<star>" using lang_star_cases by simp 

  finally show "L\<star> \<subseteq> L\<star> ; L\<star>" by simp

qed

lemma lang_star_seq_subseteq': 

  shows "L\<star>; L \<subseteq> L\<star>"

proof -

  have "L \<subseteq> L\<star>" by (rule lang_star_simple)

  then have "L\<star>; L \<subseteq> L\<star>; L\<star>" by (auto simp add: lang_seq_def)

  then show "L\<star>; L \<subseteq> L\<star>" using lang_star_double by blast

qed

lemma

  shows "L\<star> \<subseteq> L\<star>\<star>"

by (rule lang_star_simple)

section {* tricky section  *}

lemma k1:

  assumes b: "s \<in> L\<star>"

  and a: "s \<noteq> []"

  shows "s \<in> (L - {[]}); L\<star>"

using b a

apply(induct rule: Star.induct)

apply(simp)

apply(case_tac "s1=[]")

apply(simp)

apply(simp add: lang_seq_def)

apply(blast)

done

section {* (relies on lemma k1) *}

lemma zzz:

  shows "{s. c#s \<in> L1\<star>} = {s. c#s \<in> L1} ; (L1\<star>)"

apply(auto simp add: lang_seq_def Cons_eq_append_conv)

apply(drule k1)

apply(auto)[1]

apply(auto simp add: lang_seq_def)[1]

apply(rule_tac x="tl s1" in exI)

apply(rule_tac x="s2" in exI)

apply(auto)[1]

apply(auto simp add: Cons_eq_append_conv)[2]

apply(drule lang_seq_append)

apply(assumption)

apply(rotate_tac 1)

apply(drule rev_subsetD)

apply(rule lang_star_seq_subseteq)

apply(simp)

done

section {* regular expressions *}

datatype rexp =

  NULL

| EMPTY

| CHAR char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

consts L:: "'a \<Rightarrow> string set"

fun

  L_rexp :: "rexp \<Rightarrow> string set"

where

  "L_rexp (NULL) = {}"

| "L_rexp (EMPTY) = {[]}"

| "L_rexp (CHAR c) = {[c]}"

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

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

| "L_rexp (STAR r) = (L_rexp r)\<star>"

defs (overloaded)

  l_rexp_abs: "L rexp \<equiv> L_rexp rexp"

declare L_rexp.simps [simp del] L_rexp.simps [folded l_rexp_abs, simp add]

definition

  Ls :: "rexp set \<Rightarrow> string set"

where

  "Ls R = (\<Union>r\<in>R. (L r))"

lemma Ls_union:

  "Ls (R1 \<union> R2) = (Ls R1) \<union> (Ls R2)"

unfolding Ls_def by auto

text {* helper function for termination proofs *}

fun

 Left :: "rexp \<Rightarrow> rexp"

where

 "Left (SEQ r1 r2) = r1"

text {* dagger function *}

function

  dagger :: "rexp \<Rightarrow> char \<Rightarrow> rexp list" ("_ \<dagger> _")

where

  c1: "(NULL \<dagger> c) = []"

| c2: "(EMPTY) \<dagger> c = []"

| c3: "(CHAR c') \<dagger> c = (if c = c' then [EMPTY] else [])"

| c4: "(ALT r1 r2) \<dagger> c = r1 \<dagger> c @ r2 \<dagger> c"

| c5: "(SEQ NULL r2) \<dagger> c = []" 

| c6: "(SEQ EMPTY r2) \<dagger> c = r2 \<dagger> c" 

| c7: "(SEQ (CHAR c') r2) \<dagger> c = (if c = c' then [r2] else [])"

| c8: "(SEQ (SEQ r11 r12) r2) \<dagger> c = (SEQ r11 (SEQ r12 r2)) \<dagger> c" 

| c9: "(SEQ (ALT r11 r12) r2) \<dagger> c = (SEQ r11 r2) \<dagger> c @ (SEQ r12 r2) \<dagger> c" 

| c10: "(SEQ (STAR r1) r2) \<dagger> c = r2 \<dagger> c @ [SEQ r' (SEQ (STAR r1) r2). r' \<leftarrow> r1 \<dagger> c]" 

| c11: "(STAR r) \<dagger> c = [SEQ r' (STAR r) .  r' \<leftarrow> r \<dagger> c]"

by (pat_completeness) (auto)

termination dagger

  by (relation "measures [\<lambda>(r, c). size r, \<lambda>(r, c). size (Left r)]") (simp_all)

lemma dagger_correctness:

  "Ls (set r \<dagger> c) = {s. c#s \<in> L r}"

proof (induct rule: dagger.induct)

  case (1 c)

  show "Ls (set NULL \<dagger> c) = {s. c#s \<in> L NULL}" by (simp add: Ls_def)

next  

  case (2 c)

  show "Ls (set EMPTY \<dagger> c) = {s. c#s \<in> L EMPTY}" by (simp add: Ls_def)

next

  case (3 c' c)

  show "Ls (set CHAR c' \<dagger> c) = {s. c#s \<in> L (CHAR c')}" by (simp add: Ls_def)

next

  case (4 r1 r2 c)

  have ih1: "Ls (set r1 \<dagger> c) = {s. c#s \<in> L r1}" by fact

  have ih2: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact

  show "Ls (set ALT r1 r2 \<dagger> c) = {s. c#s \<in> L (ALT r1 r2)}"

    by (simp add: Ls_union ih1 ih2 Collect_disj_eq)

next

  case (5 r2 c)

  show "Ls (set SEQ NULL r2 \<dagger> c) = {s. c#s \<in> L (SEQ NULL r2)}" by (simp add: Ls_def lang_seq_null)

next

  case (6 r2 c)

  have ih: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact

  show "Ls (set SEQ EMPTY r2 \<dagger> c) = {s. c#s \<in> L (SEQ EMPTY r2)}"

    by (simp add: ih lang_seq_empty)

next

  case (7 c' r2 c)

  show "Ls (set SEQ (CHAR c') r2 \<dagger> c) = {s. c#s \<in> L (SEQ (CHAR c') r2)}"

    by (simp add: Ls_def lang_seq_def)

next

  case (8 r11 r12 r2 c)

  have ih: "Ls (set SEQ r11 (SEQ r12 r2) \<dagger> c) = {s. c#s \<in> L (SEQ r11 (SEQ r12 r2))}" by fact

  show "Ls (set SEQ (SEQ r11 r12) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (SEQ r11 r12) r2)}"

    by (simp add: ih lang_seq_assoc)

next

  case (9 r11 r12 r2 c)

  have ih1: "Ls (set SEQ r11 r2 \<dagger> c) = {s. c#s \<in> L (SEQ r11 r2)}" by fact

  have ih2: "Ls (set SEQ r12 r2 \<dagger> c) = {s. c#s \<in> L (SEQ r12 r2)}" by fact

  show "Ls (set SEQ (ALT r11 r12) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (ALT r11 r12) r2)}"

    by (simp add: Ls_union ih1 ih2 lang_seq_union Collect_disj_eq)

next

  case (10 r1 r2 c)

  have ih2: "Ls (set r2 \<dagger> c) = {s. c#s \<in> L r2}" by fact

  have ih1: "Ls (set r1 \<dagger> c) = {s. c#s \<in> L r1}" by fact

  have "Ls (set SEQ (STAR r1) r2 \<dagger> c) = Ls (set r2 \<dagger> c) \<union> (Ls (set r1 \<dagger> c); ((L r1)\<star> ; L r2))"

    by (auto simp add: lang_seq_def Ls_def)

  also have "\<dots> = {s. c#s \<in> L r2} \<union> ({s. c#s \<in> L r1} ; ((L r1)\<star> ; L r2))" using ih1 ih2 by simp

  also have "\<dots> = {s. c#s \<in> L r2} \<union> ({s. c#s \<in> L r1} ; (L r1)\<star>) ; L r2" by (simp add: lang_seq_assoc)

  also have "\<dots> = {s. c#s \<in> L r2} \<union> {s. c#s \<in> (L r1)\<star>} ; L r2" by (simp add: zzz)

  also have "\<dots> = {s. c#s \<in> L r2} \<union> {s. c#s \<in> (L r1)\<star> ; L r2}" 

    by (auto simp add: lang_seq_def Cons_eq_append_conv)

  also have "\<dots> = {s. c#s \<in> (L r1)\<star> ; L r2}" 

    by (force simp add: lang_seq_def)

  finally show "Ls (set SEQ (STAR r1) r2 \<dagger> c) = {s. c#s \<in> L (SEQ (STAR r1) r2)}" by simp

next

  case (11 r c)

  have ih: "Ls (set r \<dagger> c) = {s. c#s \<in> L r}" by fact

  have "Ls (set (STAR r) \<dagger> c) =  Ls (set r \<dagger> c) ; (L r)\<star>"

    by (auto simp add: lang_seq_def Ls_def)

  also have "\<dots> = {s. c#s \<in> L r} ;  (L r)\<star>" using ih by simp

  also have "\<dots> = {s. c#s \<in> (L r)\<star>}" using zzz by simp

  finally show "Ls (set (STAR r) \<dagger> c) = {s. c#s \<in> L (STAR r)}" by simp

qed

text {* matcher function (based on the "list"-dagger function) *}

fun

  first_True :: "bool list \<Rightarrow> bool"

where

  "first_True [] = False"

| "first_True (x#xs) = (if x then True else first_True xs)"

lemma not_first_True[simp]:

  shows "(\<not>(first_True xs)) = (\<forall>x \<in> set xs. \<not>x)"

by (induct xs) (auto)

lemma first_True:

  shows "(first_True xs) = (\<exists>x \<in> set xs. x)"

by (induct xs) (auto)

text {* matcher function *}

function

  matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool" ("_ ! _")

where

  "NULL ! s = False"

| "EMPTY ! s = (s =[])"

| "CHAR c ! s = (s = [c])" 

| "ALT r1 r2 ! s = (r1 ! s \<or> r2 ! s)"

| "STAR r ! [] = True"

| "STAR r ! c#s =  first_True [SEQ (r') (STAR r) ! s. r' \<leftarrow> r \<dagger> c]"

| "SEQ r1 r2 ! [] = (r1 ! [] \<and> r2 ! [])"

| "SEQ NULL r2 ! (c#s) = False"

| "SEQ EMPTY r2 ! (c#s) = (r2 ! c#s)"

| "SEQ (CHAR c') r2 ! (c#s) = (if c'=c then r2 ! s else False)" 

| "SEQ (SEQ r11 r12) r2 ! (c#s) = (SEQ r11 (SEQ r12 r2) ! c#s)"

| "SEQ (ALT r11 r12) r2 ! (c#s) = ((SEQ r11 r2) ! (c#s) \<or> (SEQ r12 r2) ! (c#s))"

| "SEQ (STAR r1) r2 ! (c#s) = (r2 ! (c#s) \<or> first_True [SEQ r' (SEQ (STAR r1) r2) ! s. r' \<leftarrow> r1 \<dagger> c])"

by (pat_completeness) (auto)

termination matcher 

  by(relation "measures [\<lambda>(r,s). length s, \<lambda>(r,s). size r, \<lambda>(r,s). size (Left r)]") (simp_all)

text {* positive correctness of the matcher *}

lemma matcher1:

  shows "r ! s \<Longrightarrow> s \<in> L r"

proof (induct rule: matcher.induct)

  case (1 s)

  have "NULL ! s" by fact

  then show "s \<in> L NULL" by simp

next

  case (2 s)

  have "EMPTY ! s" by fact

  then show "s \<in> L EMPTY" by simp

next

  case (3 c s)

  have "CHAR c ! s" by fact

  then show "s \<in> L (CHAR c)" by simp

next

  case (4 r1 r2 s)

  have ih1: "r1 ! s \<Longrightarrow> s \<in> L r1" by fact

  have ih2: "r2 ! s \<Longrightarrow> s \<in> L r2" by fact

  have "ALT r1 r2 ! s" by fact

  with ih1 ih2 show "s \<in> L (ALT r1 r2)" by auto

next

  case (5 r)

  have "STAR r ! []" by fact 

  then show "[] \<in> L (STAR r)" by auto

next

  case (6 r c s)

  have ih1: "\<And>rx. \<lbrakk>rx \<in> set r \<dagger> c; SEQ rx (STAR r) ! s\<rbrakk> \<Longrightarrow> s \<in> L (SEQ rx (STAR r))" by fact

  have as: "STAR r ! c#s" by fact

  then obtain r' where imp1: "r' \<in> set r \<dagger> c" and imp2: "SEQ r' (STAR r) ! s" 

    by (auto simp add: first_True)

  from imp2 imp1 have "s \<in> L (SEQ r' (STAR r))" using ih1 by simp

  then have "s \<in> L r' ; (L r)\<star>" by simp

  then have "s \<in> Ls (set r \<dagger> c) ; (L r)\<star>" using imp1 by (auto simp add: Ls_def lang_seq_def)

  then have "s \<in> {s. c#s \<in> L r} ; (L r)\<star>" by (auto simp add: dagger_correctness)

  then have "s \<in> {s. c#s \<in> (L r)\<star>}" by (simp add: zzz)

  then have "c#s \<in> {[c]}; {s. c#s \<in> (L r)\<star>}" by (auto simp add: lang_seq_def)

  then have "c#s \<in> (L r)\<star>" by (auto simp add: lang_seq_def)

  then show "c#s \<in> L (STAR r)" by simp

next

  case (7 r1 r2)

  have ih1: "r1 ! [] \<Longrightarrow> [] \<in> L r1" by fact

  have ih2: "r2 ! [] \<Longrightarrow> [] \<in> L r2" by fact

  have as: "SEQ r1 r2 ! []" by fact

  then have "r1 ! [] \<and> r2 ! []" by simp

  then show "[] \<in> L (SEQ r1 r2)" using ih1 ih2 by (simp add: lang_seq_def)

next

  case (8 r2 c s)

  have "SEQ NULL r2 ! c#s" by fact

  then show "c#s \<in> L (SEQ NULL r2)" by simp

next

  case (9 r2 c s)

  have ih1: "r2 ! c#s \<Longrightarrow> c#s \<in> L r2" by fact

  have "SEQ EMPTY r2 ! c#s" by fact

  then show "c#s \<in> L (SEQ EMPTY r2)" using ih1 by (simp add: lang_seq_def)

next

  case (10 c' r2 c s)

  have ih1: "\<lbrakk>c' = c; r2 ! s\<rbrakk> \<Longrightarrow> s \<in> L r2" by fact

  have "SEQ (CHAR c') r2 ! c#s" by fact

  then show "c#s \<in> L (SEQ (CHAR c') r2)"

    using ih1 by (auto simp add: lang_seq_def split: if_splits)

next

  case (11 r11 r12 r2 c s)

  have ih1: "SEQ r11 (SEQ r12 r2) ! c#s \<Longrightarrow> c#s \<in> L (SEQ r11 (SEQ r12 r2))" by fact

  have "SEQ (SEQ r11 r12) r2 ! c#s" by fact

  then have "c#s \<in> L (SEQ r11 (SEQ r12 r2))" using ih1 by simp

  then show "c#s \<in> L (SEQ (SEQ r11 r12) r2)" by (simp add: lang_seq_assoc)

next

  case (12 r11 r12 r2 c s)

  have ih1: "SEQ r11 r2 ! c#s \<Longrightarrow> c#s \<in> L (SEQ r11 r2)" by fact

  have ih2: "SEQ r12 r2 ! c#s \<Longrightarrow> c#s \<in> L (SEQ r12 r2)" by fact

  have "SEQ (ALT r11 r12) r2 ! c#s" by fact

  then show "c#s \<in> L (SEQ (ALT r11 r12) r2)"

    using ih1 ih2 by (auto simp add: lang_seq_union)

next

  case (13 r1 r2 c s)

  have ih1: "r2 ! c#s \<Longrightarrow> c#s \<in> L r2" by fact

  have ih2: "\<And>r'. \<lbrakk>r' \<in> set r1 \<dagger> c; SEQ r' (SEQ (STAR r1) r2) ! s\<rbrakk> \<Longrightarrow> 

                         s \<in> L (SEQ r' (SEQ (STAR r1) r2))" by fact

  have "SEQ (STAR r1) r2 ! c#s" by fact

  then have "(r2 ! c#s) \<or> (\<exists>r' \<in> set r1 \<dagger> c. SEQ r' (SEQ (STAR r1) r2) ! s)"  by (auto simp add: first_True)

  moreover

  { assume "r2 ! c#s"

    with ih1 have "c#s \<in> L r2" by simp

    then have "c # s \<in> L r1\<star> ; L r2" 

      by (auto simp add: lang_seq_def)

    then have "c#s \<in> L (SEQ (STAR r1) r2)" by simp

  }

  moreover

  { assume "\<exists>r' \<in> set r1 \<dagger> c. SEQ r' (SEQ (STAR r1) r2) ! s"

    then obtain r' where imp1: "r' \<in> set r1 \<dagger> c" and imp2: "SEQ r' (SEQ (STAR r1) r2) ! s" by blast

    from imp2 imp1 have "s \<in> L (SEQ r' (SEQ (STAR r1) r2))" using ih2 by simp

    then have "s \<in> L r' ; ((L r1)\<star> ; L r2)" by simp

    then have "s \<in> Ls (set r1 \<dagger> c) ; ((L r1)\<star> ; L r2)" using imp1 by (auto simp add: Ls_def lang_seq_def)

    then have "s \<in> {s. c#s \<in> L r1} ; ((L r1)\<star> ; L r2)" by (simp add: dagger_correctness)

    then have "s \<in> ({s. c#s \<in> L r1} ; (L r1)\<star>) ; L r2" by (simp add: lang_seq_assoc)

    then have "s \<in> {s. c#s \<in> (L r1)\<star>} ; L r2" by (simp add: zzz)

    then have "c#s \<in> {[c]}; ({s. c#s \<in> (L r1)\<star>}; L r2)" by (auto simp add: lang_seq_def)

    then have "c#s \<in> ({[c]}; {s. c#s \<in> (L r1)\<star>}) ; L r2" by (simp add: lang_seq_assoc)

    then have "c#s \<in> (L r1)\<star>; L r2" by (auto simp add: lang_seq_def)

    then have "c#s \<in> L (SEQ (STAR r1) r2)" by simp

  }

  ultimately show "c#s \<in> L (SEQ (STAR r1) r2)" by blast

qed

text {* negative correctness of the matcher *}

lemma matcher2:

  shows "\<not> r ! s \<Longrightarrow> s \<notin> L r"

proof (induct rule: matcher.induct)

  case (1 s)

  have "\<not> NULL ! s" by fact

  then show "s \<notin> L NULL" by simp

next

  case (2 s)

  have "\<not> EMPTY ! s" by fact

  then show "s \<notin> L EMPTY" by simp

next

  case (3 c s)

  have "\<not> CHAR c ! s" by fact

  then show "s \<notin> L (CHAR c)" by simp

next

  case (4 r1 r2 s)

  have ih2: "\<not> r1 ! s \<Longrightarrow> s \<notin> L r1" by fact

  have ih4: "\<not> r2 ! s \<Longrightarrow> s \<notin> L r2" by fact

  have "\<not> ALT r1 r2 ! s" by fact 

  then show "s \<notin> L (ALT r1 r2)" by (simp add: ih2 ih4)

next

  case (5 r)

  have "\<not> STAR r ! []" by fact

  then show "[] \<notin> L (STAR r)" by simp

next

  case (6 r c s)

  have ih: "\<And>rx. \<lbrakk>rx \<in> set r \<dagger> c; \<not>SEQ rx (STAR r) ! s\<rbrakk> \<Longrightarrow> s \<notin> L (SEQ rx (STAR r))" by fact

  have as: "\<not> STAR r ! c#s" by fact

  then have "\<forall>r'\<in> set r \<dagger> c. \<not> (SEQ r' (STAR r) ! s)" by simp

  then have "\<forall>r'\<in> set r \<dagger> c. s \<notin> L (SEQ r' (STAR r))" using ih by auto

  then have "\<forall>r'\<in> set r \<dagger> c. s \<notin> L r' ; ((L r)\<star>)" by simp

  then have "s \<notin> (Ls (set r \<dagger> c)) ; ((L r)\<star>)" by (auto simp add: Ls_def lang_seq_def)

  then have "s \<notin> {s. c#s \<in> L r} ; ((L r)\<star>)" by (simp add: dagger_correctness)

  then have "s \<notin> {s. c#s \<in> (L r)\<star>}" by (simp add: zzz)