theory Simplifying

  imports "Lexer" 

begin

section {* Lexer including simplifications *}

fun F_RIGHT where

  "F_RIGHT f v = Right (f v)"

fun F_LEFT where

  "F_LEFT f v = Left (f v)"

fun F_ALT where

  "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"

| "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)"  

| "F_ALT f1 f2 v = v"

fun F_SEQ1 where

  "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"

fun F_SEQ2 where 

  "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"

fun F_SEQ where 

  "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"

| "F_SEQ f1 f2 v = v"

fun simp_ALT where

  "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"

| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"

| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"

(* where is ZERO *)

fun simp_SEQ where

  "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"

| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"

| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  

lemma simp_SEQ_simps[simp]:

  "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))

                    else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))

                    else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"

by (induct p1 p2 rule: simp_SEQ.induct) (auto)

lemma simp_ALT_simps[simp]:

  "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))

                    else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))

                    else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"

by (induct p1 p2 rule: simp_ALT.induct) (auto)

fun 

  simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"

where

  "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" 

| "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" 

| "simp r = (r, id)"

fun 

  slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"

where

  "slexer r [] = (if nullable r then Some(mkeps r) else None)"

| "slexer r (c#s) = (let (rs, fr) = simp (der c r) in

                         (case (slexer rs s) of  

                            None \<Rightarrow> None

                          | Some(v) \<Rightarrow> Some(injval r c (fr v))))"

lemma slexer_better_simp:

  "slexer r (c#s) = (case (slexer (fst (simp (der c r))) s) of  

                            None \<Rightarrow> None

                          | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (der c r))) v)))"

by (auto split: prod.split option.split)

lemma L_fst_simp:

  shows "L(r) = L(fst (simp r))"

by (induct r) (auto)

lemma Posix_simp:

  assumes "s \<in> (fst (simp r)) \<rightarrow> v" 

  shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"

using assms

proof(induct r arbitrary: s v rule: rexp.induct)

  case (ALT r1 r2 s v)

  have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact

  have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact

  have as: "s \<in> fst (simp (ALT r1 r2)) \<rightarrow> v" by fact

  consider (ZERO_ZERO) "fst (simp r1) = ZERO" "fst (simp r2) = ZERO"

         | (ZERO_NZERO) "fst (simp r1) = ZERO" "fst (simp r2) \<noteq> ZERO"

         | (NZERO_ZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) = ZERO"

         | (NZERO_NZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO" by auto

  then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" 

    proof(cases)

      case (ZERO_ZERO)

      with as have "s \<in> ZERO \<rightarrow> v" by simp 

      then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" by (rule Posix_elims(1))

    next

      case (ZERO_NZERO)

      with as have "s \<in> fst (simp r2) \<rightarrow> v" by simp

      with IH2 have "s \<in> r2 \<rightarrow> snd (simp r2) v" by simp

      moreover

      from ZERO_NZERO have "fst (simp r1) = ZERO" by simp

      then have "L (fst (simp r1)) = {}" by simp

      then have "L r1 = {}" using L_fst_simp by simp

      then have "s \<notin> L r1" by simp 

      ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right (snd (simp r2) v)" by (rule Posix_ALT2)

      then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"

      using ZERO_NZERO by simp

    next

      case (NZERO_ZERO)

      with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp

      with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp

      then have "s \<in> ALT r1 r2 \<rightarrow> Left (snd (simp r1) v)" by (rule Posix_ALT1) 

      then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_ZERO by simp

    next

      case (NZERO_NZERO)

      with as have "s \<in> ALT (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp

      then consider (Left) v1 where "v = Left v1" "s \<in> (fst (simp r1)) \<rightarrow> v1"

                  | (Right) v2 where "v = Right v2" "s \<in> (fst (simp r2)) \<rightarrow> v2" "s \<notin> L (fst (simp r1))"

                  by (erule_tac Posix_elims(4)) 

      then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v"

      proof(cases)

        case (Left)

        then have "v = Left v1" "s \<in> r1 \<rightarrow> (snd (simp r1) v1)" using IH1 by simp_all

        then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO

          by (simp_all add: Posix_ALT1)

      next 

        case (Right)

        then have "v = Right v2" "s \<in> r2 \<rightarrow> (snd (simp r2) v2)" "s \<notin> L r1" using IH2 L_fst_simp by simp_all

        then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO

          by (simp_all add: Posix_ALT2)

      qed

    qed

next

  case (SEQ r1 r2 s v)

  have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact

  have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact

  have as: "s \<in> fst (simp (SEQ r1 r2)) \<rightarrow> v" by fact

  consider (ONE_ONE) "fst (simp r1) = ONE" "fst (simp r2) = ONE"

         | (ONE_NONE) "fst (simp r1) = ONE" "fst (simp r2) \<noteq> ONE"

         | (NONE_ONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) = ONE"

         | (NONE_NONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) \<noteq> ONE" by auto

  then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" 

  proof(cases)

      case (ONE_ONE)

      with as have b: "s \<in> ONE \<rightarrow> v" by simp 

      from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 ONE_ONE by simp

      moreover

      from b have c: "s = []" "v = Void" using Posix_elims(2) by auto

      moreover

      have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)

      then have "[] \<in> fst (simp r2) \<rightarrow> Void" using ONE_ONE by simp

      then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp

      ultimately have "([] @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) Void)"

        using Posix_SEQ by blast 

      then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using c ONE_ONE by simp

    next

      case (ONE_NONE)

      with as have b: "s \<in> fst (simp r2) \<rightarrow> v" by simp 

      from b have "s \<in> r2 \<rightarrow> snd (simp r2) v" using IH2 ONE_NONE by simp

      moreover

      have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)

      then have "[] \<in> fst (simp r1) \<rightarrow> Void" using ONE_NONE by simp

      then have "[] \<in> r1 \<rightarrow> snd (simp r1) Void" using IH1 by simp

      moreover

      from ONE_NONE(1) have "L (fst (simp r1)) = {[]}" by simp

      then have "L r1 = {[]}" by (simp add: L_fst_simp[symmetric])

      ultimately have "([] @ s) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) v)"

        by(rule_tac Posix_SEQ) auto

      then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using ONE_NONE by simp

    next

      case (NONE_ONE)

        with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp

        with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp

      moreover

        have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE)

        then have "[] \<in> fst (simp r2) \<rightarrow> Void" using NONE_ONE by simp

        then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp

      ultimately have "(s @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)"

        by(rule_tac Posix_SEQ) auto

      then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp

    next

      case (NONE_NONE)

      with as have "s \<in> SEQ (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp

      then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2"

                     "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2"

                     "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)"

                     by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) 

      then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)"

        using IH1 IH2 by auto             

      then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE

        by(auto intro: Posix_SEQ)

    qed

qed (simp_all)

lemma slexer_correctness:

  shows "slexer r s = lexer r s"

proof(induct s arbitrary: r)

  case Nil

  show "slexer r [] = lexer r []" by simp

next 

  case (Cons c s r)

  have IH: "\<And>r. slexer r s = lexer r s" by fact

  show "slexer r (c # s) = lexer r (c # s)" 

   proof (cases "s \<in> L (der c r)")

     case True

       assume a1: "s \<in> L (der c r)"

       then obtain v1 where a2: "lexer (der c r) s = Some v1" "s \<in> der c r \<rightarrow> v1"

         using lexer_correct_Some by auto

       from a1 have "s \<in> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp

       then obtain v2 where a3: "lexer (fst (simp (der c r))) s = Some v2" "s \<in> (fst (simp (der c r))) \<rightarrow> v2"

          using lexer_correct_Some by auto

       then have a4: "slexer (fst (simp (der c r))) s = Some v2" using IH by simp

       from a3(2) have "s \<in> der c r \<rightarrow> (snd (simp (der c r))) v2" using Posix_simp by simp

       with a2(2) have "v1 = (snd (simp (der c r))) v2" using Posix_determ by simp

       with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split)

     next 

     case False

       assume b1: "s \<notin> L (der c r)"

       then have "lexer (der c r) s = None" using lexer_correct_None by simp

       moreover

       from b1 have "s \<notin> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp

       then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp

       then have "slexer (fst (simp (der c r))) s = None" using IH by simp

       ultimately show "slexer r (c # s) = lexer r (c # s)" 

         by (simp del: slexer.simps add: slexer_better_simp)

   qed

 qed  

fun simp2_ALT where

  "simp2_ALT ZERO r2 seen = (r2, seen)"

| "simp2_ALT r1 ZERO seen = (r1, seen)"

| "simp2_ALT r1 r2 seen = (ALT r1 r2, seen)"

fun simp2_SEQ where

  "simp2_SEQ ZERO r2 seen = (ZERO, seen)"

| "simp2_SEQ r1 ZERO seen = (ZERO, seen)"

| "simp2_SEQ ONE r2 seen = (r2, seen \<union> {r2})"

| "simp2_SEQ r1 ONE seen = (r1, seen \<union> {r1})"

| "simp2_SEQ r1 r2 seen = (SEQ r1 r2, seen \<union> {SEQ r1 r2})"  

fun 

  simp2 :: "rexp \<Rightarrow> rexp set \<Rightarrow> rexp * rexp set"

where

  "simp2 (ALT r1 r2) seen = 

      (let (r1s, seen1) = simp2 r1 seen in 

       let (r2s, seen2) = simp2 r2 seen1 

       in simp2_ALT r1s r2s seen2)" 

| "simp2 (SEQ r1 r2) seen = 

      (let (r1s, _) = simp2 r1 {} in 

       let (r2s, _) = simp2 r2 {} 

       in if (SEQ r1s r2s \<in> seen) then (ZERO, seen)

       else simp2_SEQ r1s r2s seen)"

| "simp2 r seen = (if r \<in> seen then (ZERO, seen) else (r, seen \<union> {r}))"

lemma simp2_ALT[simp]: 

  shows "L (fst (simp2_ALT r1 r2 seen)) = L r1 \<union> L r2"

  apply(induct r1 r2 seen rule: simp2_ALT.induct)

  apply(simp_all)

  done

lemma test1:

  shows "snd (simp2_ALT r1 r2 rs) = rs"

  apply(induct r1 r2 rs rule: simp2_ALT.induct)

  apply(auto)

  done

lemma test2:

  shows "rs \<subseteq> snd (simp2_SEQ r1 r2 rs)"

  apply(induct r1 r2 rs rule: simp2_SEQ.induct)

  apply(auto)

  done

lemma test3:

  shows "rs \<subseteq> snd (simp2 r rs)"

  apply(induct r rs rule: simp2.induct)

  apply(auto split: prod.split)

  apply (metis set_mp test1)

  by (meson set_mp test2)

lemma test3a:

  shows "\<Union>(L ` snd (simp2 r rs)) \<subseteq> L(r) \<union> (\<Union> (L ` rs))"

  apply(induct r rs rule: simp2.induct)

  apply(auto split: prod.split simp add: Sequ_def)

  apply (smt UN_iff Un_iff set_mp test1)

lemma test:

  assumes "(\<Union>r' \<in> rs. L r') \<subseteq> L r"

  shows "L(fst (simp2 r rs)) \<subseteq> L(r)"

  using assms

  apply(induct r arbitrary: rs)

  apply(simp only: simp2.simps)

  apply(simp)

  apply(simp only: simp2.simps)

  apply(simp)

  apply(simp only: simp2.simps)

  apply(simp)

  prefer 3

  apply(simp only: simp2.simps)

  apply(simp)

  prefer 2

  apply(simp only: simp2.simps)

   apply(simp)

   apply(subst prod.split)

  apply(rule allI)+

   apply(rule impI)

  apply(subst prod.split)

  apply(rule allI)+

   apply(rule impI)

   apply(simp)

   apply(drule_tac x="rs" in meta_spec)

  apply(simp)

  apply(drule_tac x="x2" in meta_spec)

   apply(simp)

   apply(auto)[1]

    apply(subgoal_tac "rs \<subseteq> x2a")

     prefer 2

  apply (metis order_trans prod.sel(2) test3)

   apply(rule antisym)

  prefer 2

    apply(simp)

    apply(rule conjI)

     apply(drule meta_mp)

  prefer 2

      apply(simp)

      apply(auto)[1]

    apply(auto)[1]

  thm prod.split

   apply(auto split: prod.split)[1]

     apply(drule_tac x="rs" in meta_spec)

     apply(drule_tac x="rs" in meta_spec)

     apply(simp)

     apply(rule_tac x="SEQ x1 x1a" in bexI)

      apply(simp add: Sequ_def)

      apply(auto)[1]

     apply(simp)

  apply(subgoal_tac "L (fst (simp2_SEQ x1 x1a rs)) \<subseteq> L x1 \<union> L x1a")

     apply(frule_tac x="{}" in meta_spec)

  apply(rotate_tac 1)

     apply(frule_tac x="{}" in meta_spec)

     apply(simp)

     apply(rule_tac x="SEQ x1 x1a" in bexI)

      apply(simp add: Sequ_def)

      apply(auto)[1]

  apply(simp)

  using L.simps(2) apply blast

  prefer 3

  apply(simp only: simp2.simps)

    apply(simp)

  using L.simps(3) apply blast

  prefer 2

   apply(simp add: Sequ_def)

   apply(auto)[1]

  oops  

end