theory Sulzmann
  imports "Lexer" 
begin

section {* Bit-Encodings *}

fun 
  code :: "val \<Rightarrow> bool list"
where
  "code Void = []"
| "code (Char c) = []"
| "code (Left v) = False # (code v)"
| "code (Right v) = True # (code v)"
| "code (Seq v1 v2) = (code v1) @ (code v2)"
| "code (Stars []) = [True]"
| "code (Stars (v # vs)) =  False # (code v) @ code (Stars vs)"


fun 
  Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
where
  "Stars_add v (Stars vs) = Stars (v # vs)"

function
  decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)"
where
  "decode' ds ZERO = (Void, [])"
| "decode' ds ONE = (Void, ds)"
| "decode' ds (CHAR d) = (Char d, ds)"
| "decode' [] (ALT r1 r2) = (Void, [])"
| "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
| "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
                             let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
| "decode' [] (STAR r) = (Void, [])"
| "decode' (True # ds) (STAR r) = (Stars [], ds)"
| "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in
                                    let (vs, ds'') = decode' ds' (STAR r) 
                                    in (Stars_add v vs, ds''))"
by pat_completeness auto

lemma decode'_smaller:
  assumes "decode'_dom (ds, r)"
  shows "length (snd (decode' ds r)) \<le> length ds"
using assms
apply(induct ds r)
apply(auto simp add: decode'.psimps split: prod.split)
using dual_order.trans apply blast
by (meson dual_order.trans le_SucI)

termination "decode'"  
apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") 
apply(auto dest!: decode'_smaller)
by (metis less_Suc_eq_le snd_conv)

definition
  decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
where
  "decode ds r \<equiv> (let (v, ds') = decode' ds r 
                  in (if ds' = [] then Some v else None))"

lemma decode'_code_Stars:
  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" 
  shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
  using assms
  apply(induct vs)
  apply(auto)
  done

lemma decode'_code:
  assumes "\<Turnstile> v : r"
  shows "decode' ((code v) @ ds) r = (v, ds)"
using assms
  apply(induct v r arbitrary: ds) 
  apply(auto)
  using decode'_code_Stars by blast


lemma decode_code:
  assumes "\<Turnstile> v : r"
  shows "decode (code v) r = Some v"
  using assms unfolding decode_def
  by (smt append_Nil2 decode'_code old.prod.case)


datatype arexp =
  AZERO
| AONE "bool list"
| ACHAR "bool list" char
| ASEQ "bool list" arexp arexp
| AALT "bool list" arexp arexp
| ASTAR "bool list" arexp

fun fuse :: "bool list \<Rightarrow> arexp \<Rightarrow> arexp" where
  "fuse bs AZERO = AZERO"
| "fuse bs (AONE cs) = AONE (bs @ cs)" 
| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
| "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"
| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"

fun internalise :: "rexp \<Rightarrow> arexp" where
  "internalise ZERO = AZERO"
| "internalise ONE = AONE []"
| "internalise (CHAR c) = ACHAR [] c"
| "internalise (ALT r1 r2) = AALT [] (fuse [False] (internalise r1)) 
                                     (fuse [True]  (internalise r2))"
| "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)"
| "internalise (STAR r) = ASTAR [] (internalise r)"


fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bool list" where
  "retrieve (AONE bs) Void = bs"
| "retrieve (ACHAR bs c) (Char d) = bs"
| "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"
| "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
| "retrieve (ASTAR bs r) (Stars []) = bs @ [True]"
| "retrieve (ASTAR bs r) (Stars (v#vs)) = 
     bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"


fun 
  aerase :: "arexp \<Rightarrow> rexp"
where
  "aerase AZERO = ZERO"
| "aerase (AONE _) = ONE"
| "aerase (ACHAR _ c) = CHAR c"
| "aerase (AALT _ r1 r2) = ALT (aerase r1) (aerase r2)"
| "aerase (ASEQ _ r1 r2) = SEQ (aerase r1) (aerase r2)"
| "aerase (ASTAR _ r) = STAR (aerase r)"



fun
 anullable :: "arexp \<Rightarrow> bool"
where
  "anullable (AZERO) = False"
| "anullable (AONE bs) = True"
| "anullable (ACHAR bs c) = False"
| "anullable (AALT bs r1 r2) = (anullable r1 \<or> anullable r2)"
| "anullable (ASEQ bs r1 r2) = (anullable r1 \<and> anullable r2)"
| "anullable (ASTAR bs r) = True"

fun 
  amkeps :: "arexp \<Rightarrow> bool list"
where
  "amkeps(AONE bs) = bs"
| "amkeps(ASEQ bs r1 r2) = bs @ (amkeps r1) @ (amkeps r2)"
| "amkeps(AALT bs r1 r2) = (if anullable(r1) then bs @ (amkeps r1) else bs @ (amkeps r2))"
| "amkeps(ASTAR bs r) = bs @ [True]"


fun
 ader :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
where
  "ader c (AZERO) = AZERO"
| "ader c (AONE bs) = AZERO"
| "ader c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
| "ader c (AALT bs r1 r2) = AALT bs (ader c r1) (ader c r2)"
| "ader c (ASEQ bs r1 r2) = 
     (if anullable r1
      then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2))
      else ASEQ bs (ader c r1) r2)"
| "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)"


fun 
  aders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
  "aders r [] = r"
| "aders r (c#s) = aders (ader c r) s"

lemma aders_append:
  "aders r (s1 @ s2) = aders (aders r s1) s2"
  apply(induct s1 arbitrary: r s2)
  apply(simp_all)
  done

lemma anullable_correctness:
  shows "nullable (aerase r) = anullable r"
  apply(induct r)
  apply(simp_all)
  done

lemma aerase_fuse:
  shows "aerase (fuse bs r) = aerase r"
  apply(induct r)
  apply(simp_all)
  done

lemma aerase_internalise:
  shows "aerase (internalise r) = r"
  apply(induct r)
  apply(simp_all add: aerase_fuse)
  done

lemma aerase_ader:
  shows "aerase (ader a r) = der a (aerase r)"
  apply(induct r)
  apply(simp_all add: aerase_fuse anullable_correctness)
  done

lemma aerase_aders:
  shows "aerase (aders r s) = ders s (aerase r)"
  apply(induct s arbitrary: r )
  apply(simp_all add: aerase_ader)
  done

lemma retrieve_encode_STARS:
  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (internalise r) v"
  shows "code (Stars vs) = retrieve (ASTAR [] (internalise r)) (Stars vs)"
  using assms
  apply(induct vs)
  apply(simp)
  apply(simp)
  done

lemma retrieve_afuse2:
  assumes "\<Turnstile> v : (aerase r)"
  shows "retrieve (fuse bs r) v = bs @ retrieve r v"
  using assms
  apply(induct r arbitrary: v bs)
  apply(auto)
  using Prf_elims(1) apply blast
  using Prf_elims(4) apply fastforce
  using Prf_elims(5) apply fastforce
  apply (smt Prf_elims(2) append_assoc retrieve.simps(5))
   apply(erule Prf_elims)
    apply(simp)
   apply(simp)
  apply(erule Prf_elims)
  apply(simp)
  apply(case_tac vs)
   apply(simp)
  apply(simp)
  done

lemma retrieve_afuse:
  assumes "\<Turnstile> v : r"
  shows "retrieve (fuse bs (internalise r)) v = bs @ retrieve (internalise r) v"
  using assms 
  by (simp_all add: retrieve_afuse2 aerase_internalise)


lemma retrieve_encode:
  assumes "\<Turnstile> v : r"
  shows "code v = retrieve (internalise r) v"
  using assms
  apply(induct v r)
  apply(simp_all add: retrieve_afuse retrieve_encode_STARS)
  done





lemma Q00:
  assumes "s \<in> r \<rightarrow> v"
  shows "\<Turnstile> v : r"
  using assms
  apply(induct) 
        apply(auto intro: Prf.intros)
  by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5))

lemma Qa:
  assumes "anullable r"
  shows "retrieve r (mkeps (aerase r)) = amkeps r"
  using assms
  apply(induct r)
       apply(auto)
  using anullable_correctness apply auto[1]
  apply (simp add: anullable_correctness)
  by (simp add: anullable_correctness)

  
lemma Qb:
  assumes "\<Turnstile> v : der c (aerase r)"
  shows "retrieve (ader c r) v = retrieve r (injval (aerase r) c v)"
  using assms
  apply(induct r arbitrary: v c)
       apply(simp_all)
  using Prf_elims(1) apply blast
  using Prf_elims(1) apply blast
     apply(auto)[1]
  using Prf_elims(4) apply fastforce
  using Prf_elims(1) apply blast
    apply(auto split: if_splits)[1]
  apply(auto elim!: Prf_elims)[1]
       apply(rotate_tac 1)
       apply(drule_tac x="v2" in meta_spec)
       apply(drule_tac x="c" in meta_spec)
       apply(drule meta_mp)
        apply(simp)
       apply(drule sym)
       apply(simp)
       apply(subst retrieve_afuse2)
        apply (simp add: aerase_ader)
       apply (simp add: Qa)
  using anullable_correctness apply auto[1]
     apply(auto elim!: Prf_elims)[1]
  using anullable_correctness apply auto[1]
    apply(auto elim!: Prf_elims)[1]
   apply(auto elim!: Prf_elims)[1]
  apply(auto elim!: Prf_elims)[1]
  by (simp add: retrieve_afuse2 aerase_ader)

lemma MAIN:
  assumes "\<Turnstile> v : ders s r"
  shows "code (flex r id s v) = retrieve (aders (internalise r) s) v"
  using assms
  apply(induct s arbitrary: v rule: rev_induct)
  apply(simp)
  apply(simp add: retrieve_encode)
  apply(simp add: flex_append aders_append)
  apply(subst Qb)
  apply(simp add: aerase_internalise ders_append aerase_aders)
  apply(simp add: aerase_aders aerase_internalise)
  apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
  apply(drule meta_mp)
  apply(simp add: Prf_injval ders_append)
  apply(simp)
  done

fun alexer where
 "alexer r s = (if anullable (aders (internalise r) s) then 
                decode (amkeps (aders (internalise r) s)) r else None)"


lemma FIN:
  "alexer r s = lexer r s"
  apply(auto simp add: lexer_flex)
  apply (smt MAIN Q00 Qa aerase_aders aerase_internalise decode_code lexer_correctness(1) lexer_flex mkeps_nullable)
  apply (metis aerase_aders aerase_internalise anullable_correctness)
  using aerase_aders aerase_internalise anullable_correctness by force

unused_thms
  
end