theory BasicIdentities 

  imports "Lexer" 

begin

datatype rrexp = 

  RZERO

| RONE 

| RCHAR char

| RSEQ rrexp rrexp

| RALTS "rrexp list"

| RSTAR rrexp

abbreviation

  "RALT r1 r2 \<equiv> RALTS [r1, r2]"

fun

 rnullable :: "rrexp \<Rightarrow> bool"

where

  "rnullable (RZERO) = False"

| "rnullable (RONE) = True"

| "rnullable (RCHAR c) = False"

| "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)"

| "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)"

| "rnullable (RSTAR r) = True"

fun

 rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"

where

  "rder c (RZERO) = RZERO"

| "rder c (RONE) = RZERO"

| "rder c (RCHAR d) = (if c = d then RONE else RZERO)"

| "rder c (RALTS rs) = RALTS (map (rder c) rs)"

| "rder c (RSEQ r1 r2) = 

     (if rnullable r1

      then RALT   (RSEQ (rder c r1) r2) (rder c r2)

      else RSEQ   (rder c r1) r2)"

| "rder c (RSTAR r) = RSEQ  (rder c r) (RSTAR r)"

fun 

  rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"

where

  "rders r [] = r"

| "rders r (c#s) = rders (rder c r) s"

fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list"

  where

  "rdistinct [] acc = []"

| "rdistinct (x#xs)  acc = 

     (if x \<in> acc then rdistinct xs  acc 

      else x # (rdistinct xs  ({x} \<union> acc)))"

lemma rdistinct1:

  assumes "a \<in> acc"

  shows "a \<notin> set (rdistinct rs acc)"

  using assms

  apply(induct rs arbitrary: acc a)

   apply(auto)

  done

lemma rdistinct_does_the_job:

  shows "distinct (rdistinct rs s)"

  apply(induct rs s rule: rdistinct.induct)

  apply(auto simp add: rdistinct1)

  done

lemma rdistinct_concat:

  assumes "set rs \<subseteq> rset"

  shows "rdistinct (rs @ rsa) rset = rdistinct rsa rset"

  using assms

  apply(induct rs)

  apply simp+

  done

lemma distinct_not_exist:

  assumes "a \<notin> set rs"

  shows "rdistinct rs rset = rdistinct rs (insert a rset)"

  using assms

  apply(induct rs arbitrary: rset)

  apply(auto)

  done

lemma rdistinct_on_distinct:

  shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs"

  apply(induct rs)

  apply simp

  using distinct_not_exist by fastforce

lemma distinct_rdistinct_append:

  assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc"

  shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))"

  using assms

  apply(induct rs1 arbitrary: rsa acc)

   apply(auto)[1]

  apply(auto)[1]

  apply(drule_tac x="rsa" in meta_spec)

  apply(drule_tac x="{a} \<union> acc" in meta_spec)

  apply(simp)

  apply(drule meta_mp)

   apply(auto)[1]

  apply(simp)

  done

lemma rdistinct_set_equality1:

  shows "set (rdistinct rs acc) = set rs - acc"

  apply(induct rs acc rule: rdistinct.induct)

  apply(auto)

  done

lemma rdistinct_set_equality:

  shows "set (rdistinct rs {}) = set rs"

  by (simp add: rdistinct_set_equality1)

fun rflts :: "rrexp list \<Rightarrow> rrexp list"

  where 

  "rflts [] = []"

| "rflts (RZERO # rs) = rflts rs"

| "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs"

| "rflts (r1 # rs) = r1 # rflts rs"

lemma rflts_def_idiot:

  shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow> rflts (a # rs) = a # rflts rs"

  apply(case_tac a)

  apply simp_all

  done

lemma rflts_def_idiot2:

  shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)"

  apply(induct rs rule: rflts.induct)

  apply(auto)

  done

lemma flts_append:

  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"

  apply(induct rs1)

   apply simp

  apply(case_tac a)

       apply simp+

  done

fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp"

  where

  "rsimp_ALTs  [] = RZERO"

| "rsimp_ALTs [r] =  r"

| "rsimp_ALTs rs = RALTS rs"

lemma rsimpalts_conscons:

  shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)"

  by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3))

lemma rsimp_alts_equal:

  shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) "

  by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons)

fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"

  where

  "rsimp_SEQ  RZERO _ = RZERO"

| "rsimp_SEQ  _ RZERO = RZERO"

| "rsimp_SEQ RONE r2 = r2"

| "rsimp_SEQ r1 r2 = RSEQ r1 r2"

fun rsimp :: "rrexp \<Rightarrow> rrexp" 

  where

  "rsimp (RSEQ r1 r2) = rsimp_SEQ  (rsimp r1) (rsimp r2)"

| "rsimp (RALTS rs) = rsimp_ALTs  (rdistinct (rflts (map rsimp rs))  {}) "

| "rsimp r = r"

fun 

  rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"

where

  "rders_simp r [] = r"

| "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s"

fun rsize :: "rrexp \<Rightarrow> nat" where

  "rsize RZERO = 1"

| "rsize (RONE) = 1" 

| "rsize (RCHAR  c) = 1"

| "rsize (RALTS  rs) = Suc (sum_list (map rsize rs))"

| "rsize (RSEQ  r1 r2) = Suc (rsize r1 + rsize r2)"

| "rsize (RSTAR  r) = Suc (rsize r)"

abbreviation rsizes where

  "rsizes rs \<equiv> sum_list (map rsize rs)"

lemma rder_rsimp_ALTs_commute:

  shows "  (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)"

  apply(induct rs)

   apply simp

  apply(case_tac rs)

   apply simp

  apply auto

  done

lemma rsimp_aalts_smaller:

  shows "rsize (rsimp_ALTs  rs) \<le> rsize (RALTS rs)"

  apply(induct rs)

   apply simp

  apply simp

  apply(case_tac "rs = []")

   apply simp

  apply(subgoal_tac "\<exists>rsp ap. rs = ap # rsp")

   apply(erule exE)+

   apply simp

  apply simp

  by(meson neq_Nil_conv)

lemma rSEQ_mono:

  shows "rsize (rsimp_SEQ r1 r2) \<le>rsize (RSEQ r1 r2)"

  apply auto

  apply(induct r1)

       apply auto

      apply(case_tac "r2")

       apply simp_all

     apply(case_tac r2)

          apply simp_all

     apply(case_tac r2)

         apply simp_all

     apply(case_tac r2)

        apply simp_all

     apply(case_tac r2)

  apply simp_all

  done

lemma ralts_cap_mono:

  shows "rsize (RALTS rs) \<le> Suc (rsizes rs)"

  by simp

lemma rflts_mono:

  shows "rsizes (rflts rs) \<le> rsizes rs"

  apply(induct rs)

  apply simp

  apply(case_tac "a = RZERO")

   apply simp

  apply(case_tac "\<exists>rs1. a = RALTS rs1")

  apply(erule exE)

   apply simp

  apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)")

   prefer 2

  using rflts_def_idiot apply blast

  apply simp

  done

lemma rdistinct_smaller: 

  shows "rsizes (rdistinct rs ss) \<le> rsizes rs"

  apply (induct rs arbitrary: ss)

   apply simp

  by (simp add: trans_le_add2)

lemma rsimp_alts_mono :

  shows "\<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> rsize (rsimp xa) \<le> rsize xa)  \<Longrightarrow>

      rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \<le> Suc (rsizes x)"

  apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} )) 

                    \<le> rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))")

  prefer 2

  using rsimp_aalts_smaller apply auto[1]

  apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \<le>Suc (rsizes (rdistinct (rflts (map rsimp x)) {}))")

  prefer 2

  using ralts_cap_mono apply blast

  apply(subgoal_tac "rsizes (rdistinct (rflts (map rsimp x)) {}) \<le> rsizes (rflts (map rsimp x))")

  prefer 2

  using rdistinct_smaller apply presburger

  apply(subgoal_tac "rsizes (rflts (map rsimp x)) \<le> rsizes (map rsimp x)")

  prefer 2

  using rflts_mono apply blast

  apply(subgoal_tac "rsizes (map rsimp x) \<le> rsizes x")

  prefer 2

  apply (simp add: sum_list_mono)

  by linarith

lemma rsimp_mono:

  shows "rsize (rsimp r) \<le> rsize r"

  apply(induct r)

  apply simp_all

  apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))")

    apply force

  using rSEQ_mono

   apply presburger

  using rsimp_alts_mono by auto

lemma idiot:

  shows "rsimp_SEQ RONE r = r"

  apply(case_tac r)

       apply simp_all

  done

lemma idiot2:

  shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk>

    \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2"

  apply(case_tac r1)

       apply(case_tac r2)

  apply simp_all

     apply(case_tac r2)

  apply simp_all

     apply(case_tac r2)

  apply simp_all

   apply(case_tac r2)

  apply simp_all

  apply(case_tac r2)

       apply simp_all

  done

lemma rders__onechar:

  shows " (rders_simp r [c]) =  (rsimp (rders r [c]))"

  by simp

lemma rders_append:

  "rders c (s1 @ s2) = rders (rders c s1) s2"

  apply(induct s1 arbitrary: c s2)

  apply(simp_all)

  done

lemma rders_simp_append:

  "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2"

  apply(induct s1 arbitrary: c s2)

   apply(simp_all)

  done

lemma rders_simp_one_char:

  shows "rders_simp r [c] = rsimp (rder c r)"

  apply auto

  done

fun nonalt :: "rrexp \<Rightarrow> bool"

  where

  "nonalt (RALTS  rs) = False"

| "nonalt r = True"

fun good :: "rrexp \<Rightarrow> bool" where

  "good RZERO = False"

| "good (RONE) = True" 

| "good (RCHAR c) = True"

| "good (RALTS []) = False"

| "good (RALTS [r]) = False"

| "good (RALTS (r1 # r2 # rs)) = ((distinct ( (r1 # r2 # rs))) \<and>(\<forall>r' \<in> set (r1 # r2 # rs). good r' \<and> nonalt r'))"

| "good (RSEQ RZERO _) = False"

| "good (RSEQ RONE _) = False"

| "good (RSEQ  _ RZERO) = False"

| "good (RSEQ r1 r2) = (good r1 \<and> good r2)"

| "good (RSTAR r) = True"

lemma  k0a:

  shows "rflts [RALTS rs] =   rs"

  apply(simp)

  done

lemma bbbbs:

  assumes "good r" "r = RALTS rs"

  shows "rsimp_ALTs  (rflts [r]) = RALTS rs"

  using  assms

  by (metis good.simps(4) good.simps(5) k0a rsimp_ALTs.elims)

lemma bbbbs1:

  shows "nonalt r \<or> (\<exists> rs. r  = RALTS  rs)"

  by (meson nonalt.elims(3))

lemma good0:

  assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r" "distinct rs"

  shows "good (rsimp_ALTs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"

  using  assms

  apply(induct  rs rule: rsimp_ALTs.induct)

  apply(auto)

  done

lemma flts1:

  assumes "good r" 

  shows "rflts [r] \<noteq> []"

  using  assms

  apply(induct r)

       apply(simp_all)

  using good.simps(4) by blast

lemma flts2:

  assumes "good r" 

  shows "\<forall>r' \<in> set (rflts [r]). good r' \<and> nonalt r'"

  using  assms

  apply(induct r)

       apply(simp)

      apply(simp)

     apply(simp)

    prefer 2

    apply(simp)

    apply(auto)[1]

     apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)

    apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)

   apply fastforce

  apply(simp)

  done  

lemma flts3:

  assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO" 

  shows "\<forall>r \<in> set (rflts rs). good r"

  using  assms

  apply(induct rs arbitrary: rule: rflts.induct)

        apply(simp_all)

  by (metis UnE flts2 k0a)

lemma  k0:

  shows "rflts (r # rs1) = rflts [r] @ rflts rs1"

  apply(induct r arbitrary: rs1)

   apply(auto)

  done

lemma good_SEQ:

  assumes "r1 \<noteq> RZERO" "r2 \<noteq> RZERO" " r1 \<noteq> RONE"

  shows "good (RSEQ r1 r2) = (good r1 \<and> good r2)"

  using assms

  apply(case_tac r1)

       apply(simp_all)

  apply(case_tac r2)

          apply(simp_all)

  apply(case_tac r2)

         apply(simp_all)

  apply(case_tac r2)

        apply(simp_all)

  apply(case_tac r2)

       apply(simp_all)

  done

lemma rsize0:

  shows "0 < rsize r"

  apply(induct  r)

       apply(auto)

  done

fun nonnested :: "rrexp \<Rightarrow> bool"

  where

  "nonnested (RALTS []) = True"

| "nonnested (RALTS ((RALTS rs1) # rs2)) = False"

| "nonnested (RALTS (r # rs2)) = nonnested (RALTS rs2)"

| "nonnested r = True"

lemma  k00:

  shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2"

  apply(induct rs1 arbitrary: rs2)

   apply(auto)

  by (metis append.assoc k0)

lemma k0b:

  assumes "nonalt r" "r \<noteq> RZERO"

  shows "rflts [r] = [r]"

  using assms

  apply(case_tac  r)

  apply(simp_all)

  done

lemma nn1qq:

  assumes "nonnested (RALTS rs)"

  shows "\<nexists> rs1. RALTS rs1 \<in> set rs"

  using assms

  apply(induct rs rule: rflts.induct)

  apply(auto)

  done

lemma n0:

  shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"

  apply(induct rs )

   apply(auto)

    apply (metis list.set_intros(1) nn1qq nonalt.elims(3))

  apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))

  using bbbbs1 apply fastforce

  by (metis bbbbs1 list.set_intros(2) nn1qq)

lemma nn1c:

  assumes "\<forall>r \<in> set rs. nonnested r"

  shows "\<forall>r \<in> set (rflts rs). nonalt r"

  using assms

  apply(induct rs rule: rflts.induct)

        apply(auto)

  using n0 by blast

lemma nn1bb:

  assumes "\<forall>r \<in> set rs. nonalt r"

  shows "nonnested (rsimp_ALTs  rs)"