theory Sulzmann
  imports "Positions" 
begin


section {* Sulzmann's "Ordering" of Values *}

inductive ValOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ \<prec> _" [100, 100] 100)
where
  MY0: "length (flat v2) < length (flat v1) \<Longrightarrow> v1 \<prec> v2" 
| C2: "\<lbrakk>v1 \<prec> v1'; flat (Seq v1 v2) = flat (Seq v1' v2')\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1' v2')" 
| C1: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1 v2')" 
| A2: "flat v1 = flat v2 \<Longrightarrow> (Left v1) \<prec> (Right v2)"
| A3: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Right v2) \<prec> (Right v2')"
| A4: "\<lbrakk>v1 \<prec> v1'; flat v1 = flat v1'\<rbrakk> \<Longrightarrow> (Left v1) \<prec> (Left v1')"
| K1: "flat (Stars (v#vs)) = [] \<Longrightarrow> (Stars []) \<prec> (Stars (v#vs))"
| K3: "\<lbrakk>v1 \<prec> v2; flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))\<rbrakk> \<Longrightarrow> (Stars (v1#vs1)) \<prec> (Stars (v2#vs2))"
| K4: "\<lbrakk>(Stars vs1) \<prec> (Stars vs2); flat (Stars vs1) = flat (Stars vs2)\<rbrakk>  \<Longrightarrow> (Stars (v#vs1)) \<prec> (Stars (v#vs2))"


(*
inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100)
where
  C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" 
| C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" 
| A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Left v1)"
| A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Right v2)"
| A3: "v2 \<preceq>r2 v2' \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Right v2')"
| A4: "v1 \<preceq>r1 v1' \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Left v1')"
| K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<preceq>(STAR r) (Stars (v # vs))"
| K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])"
| K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))"
| K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))"
*)
(*| MY1: "Void \<preceq>ONE Void" 
| MY2: "(Char c) \<preceq>(CHAR c) (Char c)" 
| MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" 
*)

(*
lemma ValOrd_refl: 
  assumes "\<turnstile> v : r" 
  shows "v \<preceq>r v"
using assms
apply(induct r rule: Prf.induct)
apply(rule ValOrd.intros)
apply(simp)
apply(rule ValOrd.intros)
apply(simp)
apply(rule ValOrd.intros)
apply(simp)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(rule ValOrd.intros)
apply(simp)
done
*)

lemma ValOrd_irrefl: 
  assumes "\<turnstile> v : r"  "v \<prec> v" 
  shows "False"
using assms
apply(induct v r rule: Prf.induct)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
apply(erule ValOrd.cases)
apply(simp_all)
done

lemma prefix_sprefix:
  shows "xs \<sqsubseteq>pre ys \<longleftrightarrow> (xs = ys \<or> xs \<sqsubset>spre ys)"
apply(auto simp add: sprefix_list_def prefix_list_def)
done



lemma Posix_CPT2:
  assumes "v1 \<prec> v2" 
  shows "v1 :\<sqsubset>val v2" 
using assms
apply(induct v1 v2 arbitrary: rule: ValOrd.induct)
apply(rule val_ord_shorterI)
apply(simp)
apply(rule val_ord_SeqI1)
apply(simp)
apply(simp)
apply(rule val_ord_SeqI2)
apply(simp)
apply(simp)
apply(simp add: val_ord_ex_def)
apply(rule_tac x="[0]" in exI)
apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1]
apply(smt inlen_bigger)
apply(rule val_ord_RightI)
apply(simp)
apply(simp)
apply(rule val_ord_LeftI)
apply(simp)
apply(simp)
defer
apply(rule val_ord_StarsI)
apply(simp)
apply(simp)
apply(rule val_ord_StarsI2)
apply(simp)
apply(simp)
oops

lemma QQ: 
  shows "x \<le> (y::nat) \<longleftrightarrow> x = y \<or> x < y"
  by auto

lemma Posix_CPT2:
  assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s"
  shows "v1 \<prec> v2"
using assms
apply(induct r arbitrary: v1 v2 s)  
apply(auto simp add: CPTpre_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPTpre_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: CPTpre_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(simp add: val_ord_ex_def)
apply(auto simp add: val_ord_def)[1]
apply(auto simp add: CPTpre_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(auto simp add: val_ord_ex_def val_ord_def)[1]
(* SEQ case *)
apply(subst (asm) (5) CPTpre_def)
apply(subst (asm) (5) CPTpre_def)
apply(auto)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(clarify)
apply(frule val_ord_shorterE)
apply(subst (asm) QQ)
apply(erule disjE)
apply(drule val_ord_SeqE)
apply(erule disjE)
apply(drule_tac x="v1a" in meta_spec)
apply(rotate_tac 8)
apply(drule_tac x="v1b" in meta_spec)
apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply(drule meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply(rule ValOrd.intros(2))
apply(assumption)
apply(frule val_ord_shorterE)
apply(subst (asm) append_eq_append_conv_if)
apply(simp)
apply (metis append_assoc append_eq_append_conv_if length_append)


thm le
apply(clarify)
apply(rule ValOrd.intros)
apply(simp)

apply(subst (asm) (3) CPTpre_def)
apply(subst (asm) (3) CPTpre_def)
apply(auto)[1]
apply(drule_tac meta_mp)
apply(auto simp add: CPTpre_def)[1]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(erule CPrf.cases)
apply(simp_all)[7]
apply(clarify)
apply(drule val_ord_SeqE)
apply(erule disjE)
apply(simp add: append_eq_append_conv2)
apply(auto)
prefer 2
apply(rule  ValOrd.intros(2))
prefer 2
apply(simp)
thm ValOrd.intros
apply(case_tac "flat v1b = flat v1a")
apply(rule ValOrd.intros)
apply(simp)
apply(simp)




lemma Posix_CPT:
  assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPT r s" "v2 \<in> CPT r s"
  shows "v1 \<preceq>r v2" 
using assms
apply(induct r arbitrary: v1 v2 s rule: rexp.induct)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule ValOrd.intros)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(erule CPrf.cases)
apply(simp_all)
apply(rule ValOrd.intros)
(*SEQ case *)
apply(simp add: CPT_def)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
apply(erule CPrf.cases)
apply(simp_all)
apply(clarify)
thm val_ord_SEQ
apply(drule_tac r="r1a" in  val_ord_SEQ)
apply(simp)
using Prf_CPrf apply blast
using Prf_CPrf apply blast
apply(erule disjE)
apply(rule C2)
prefer 2
apply(simp)
apply(rule C1)
apply blast

apply(simp add: append_eq_append_conv2)
apply(clarify)
apply(auto)[1]
apply(drule_tac x="v1a" in meta_spec)
apply(rotate_tac 8)
apply(drule_tac x="v1b" in meta_spec)
apply(rotate_tac 8)
apply(simp)

(* HERE *)
apply(subst (asm) (3) val_ord_ex_def)
apply(clarify)
apply(subst (asm) val_ord_def)
apply(clarify)
apply(rule ValOrd.intros)


apply(simp add: val_ord_ex_def)
oops


lemma ValOrd_trans:
  assumes "x \<preceq>r y" "y \<preceq>r z"
  and "x \<in> CPT r s" "y \<in> CPT r s" "z \<in> CPT r s"
  shows "x \<preceq>r z"
using assms
apply(induct x r y arbitrary: s z rule: ValOrd.induct)
apply(rotate_tac 2)
apply(erule ValOrd.cases)
apply(simp_all)[13]
apply(rule ValOrd.intros)
apply(drule_tac x="s" in meta_spec)
apply(drule_tac x="v1'a" in meta_spec)
apply(drule_tac meta_mp)
apply(simp)
apply(drule_tac meta_mp)
apply(simp add: CPT_def)
oops

lemma ValOrd_preorder:
  "preorder_on (CPT r s) {(v1, v2). v1 \<preceq>r v2 \<and> v1 \<in> (CPT r s) \<and> v2 \<in> (CPT r s)}"
apply(simp add: preorder_on_def)
apply(rule conjI)
apply(simp add: refl_on_def)
apply(auto)
apply(rule ValOrd_refl)
apply(simp add: CPT_def)
apply(rule Prf_CPrf)
apply(auto)[1]
apply(simp add: trans_def)
apply(auto)

definition ValOrdEq :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<ge>_ _" [100, 100, 100] 100)
where 
  "v\<^sub>1 \<ge>r v\<^sub>2 \<equiv> v\<^sub>1 = v\<^sub>2 \<or> (v\<^sub>1 >r v\<^sub>2 \<and> flat v\<^sub>1 = flat v\<^sub>2)"

(*


inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
where
  "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
| "Void \<succ>EMPTY Void"
| "(Char c) \<succ>(CHAR c) (Char c)"
| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
| "(Stars []) \<succ>(STAR r) (Stars [])"
*)


section {* Bit-Encodings *}


fun 
  code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"
where
  "code Void ONE = []"
| "code (Char c) (CHAR d) = []"
| "code (Left v) (ALT r1 r2) = False # (code v r1)"
| "code (Right v) (ALT r1 r2) = True # (code v r2)"
| "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)"
| "code (Stars []) (STAR r) = [True]"
| "code (Stars (v # vs)) (STAR r) =  False # (code v r) @ code (Stars vs) (STAR r)"

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

termination
apply(size_change)
oops

term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))"

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)

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

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


lemma decode_code:
  assumes "\<turnstile> v : r"
  shows "decode (code v r) r = Some v"
using assms decode'_code[of _ _ "[]"]
by auto

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
 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)"

lemma
  assumes "\<turnstile> v : der c r"
  shows "Some (injval r c v) = decode (retrieve (ader c (internalise r)) v) r"
using assms
apply(induct c r arbitrary: v rule: der.induct)
apply(simp_all)
apply(erule Prf_elims)
apply(erule Prf_elims)
apply(case_tac "c = d")
apply(simp)
apply(erule Prf_elims)
apply(simp)
apply(simp)
apply(erule Prf_elims)
apply(auto split: prod.splits)[1]
oops

end