Theory WS1S_Prelim

section ‹WS1S Interpretations›

(*<*)
theory WS1S_Prelim
imports
  FSet_More
  Deriving.Compare_Instances
  "List-Index.List_Index"
begin

hide_const (open) cut
(*>*)

definition "eval P x = (x |∈| P)"
definition "downshift P = (λx. x - Suc 0) |`| (P |-| {|0|})"
definition "upshift P = Suc |`| P"
definition "lift bs i P = (if bs ! i then finsert 0 (upshift P) else upshift P)"
definition "snoc n bs i P = (if bs ! i then finsert n P else P)"
definition "cut n P = ffilter (λi. i < n) P"
definition "len P = (if P = {||} then 0 else Suc (fMax P))"

datatype order = FO | SO
derive linorder order
instantiation order :: enum begin
  definition "enum_order = [FO, SO]"
  definition "enum_all_order P = (P FO  P SO)"
  definition "enum_ex_order P = (P FO  P SO)"
  lemmas enum_defs = enum_order_def enum_all_order_def enum_ex_order_def
  instance proof qed (auto simp: enum_defs, (metis (full_types) order.exhaust)+)
end

typedef idx = "UNIV :: (nat × nat) set" by (rule UNIV_witness)

setup_lifting type_definition_idx

lift_definition SUC :: "order  idx  idx" is
  "λord (m, n). case ord of FO  (Suc m, n) | SO  (m, Suc n)" .
lift_definition LESS :: "order  nat  idx  bool" is
  "λord l (m, n). case ord of FO  l < m | SO  l < n" .
abbreviation "LEQ ord l idx  LESS ord l (SUC ord idx)"

definition "MSB Is 
  if P  set Is. P = {||} then 0 else Suc (Max (P  set Is. fset P))"

lemma MSB_Nil[simp]: "MSB [] = 0"
  unfolding MSB_def by simp

lemma MSB_Cons[simp]: "MSB (I # Is) = max (if I = {||} then 0 else Suc (fMax I)) (MSB Is)"
  unfolding MSB_def including fset.lifting
  by transfer (auto simp: Max_Un list_all_iff Sup_bot_conv(2)[symmetric] simp del: Sup_bot_conv(2))

lemma MSB_append[simp]: "MSB (I1 @ I2) = max (MSB I1) (MSB I2)"
  by (induct I1) auto

lemma MSB_insert_nth[simp]:
  "MSB (insert_nth n P Is) = max (if P = {||} then 0 else Suc (fMax P)) (MSB Is)"
  by (subst (2) append_take_drop_id[of n Is, symmetric])
    (simp only: insert_nth_take_drop MSB_append MSB_Cons MSB_Nil)

lemma MSB_greater:
  "i < length Is; p |∈| Is ! i  p < MSB Is"
  unfolding MSB_def by (fastforce simp: Bex_def in_set_conv_nth less_Suc_eq_le intro: Max_ge)

lemma MSB_mono: "set I1  set I2  MSB I1  MSB I2"
  unfolding MSB_def including fset.lifting
  by transfer (auto simp: list_all_iff intro!: Max_ge)

lemma MSB_map_index'_CONS[simp]:
  "MSB (map_index' i (lift bs) Is) =
  (if MSB Is = 0  (i  {i ..< i + length Is}. ¬ bs ! i) then 0 else Suc (MSB Is))"
  by (induct Is arbitrary: i)
   (auto split: if_splits simp: mono_fMax_commute[where f = Suc, symmetric] mono_def
    lift_def upshift_def,
    metis atLeastLessThan_iff le_antisym not_less_eq_eq)

lemma MSB_map_index'_SNOC[simp]:
  "MSB Is  n  MSB (map_index' i (snoc n bs) Is) =
  (if (i  {i ..< i + length Is}. ¬ bs ! i) then MSB Is else Suc n)"
  by (induct Is arbitrary: i)
    (auto split: if_splits simp: mono_fMax_commute[where f = Suc, symmetric] mono_def
    snoc_def, (metis atLeastLessThan_iff le_antisym not_less_eq_eq)+)

lemma MSB_replicate[simp]: "MSB (replicate n P) = (if P = {||}  n = 0 then 0 else Suc (fMax P))"
  by (induct n) auto

typedef interp =
  "{(n :: nat, I1 :: nat fset list, I2  :: nat fset list) | n I1 I2. MSB (I1 @ I2)  n}"
  by auto

setup_lifting type_definition_interp

lift_definition assigns :: "nat  interp  order  nat fset" ("___" [900, 999, 999] 999)
  is "λn (_, I1, I2) ord. case ord of FO  if n < length I1 then I1 ! n else {||}
    | SO  if n < length I2 then I2 ! n else {||}" .
lift_definition nvars :: "interp  idx" ("#V _" [1000] 900)
  is "λ(_, I1, I2). (length I1, length I2)" .
lift_definition Length :: "interp  nat"
  is "λ(n, _, _). n" .
lift_definition Extend :: "order  nat  interp  nat fset  interp"
  is "λord i (n, I1, I2) P. case ord of
      FO  (max n (if P = {||} then 0 else Suc (fMax P)), insert_nth i P I1, I2)
    | SO  (max n (if P = {||} then 0 else Suc (fMax P)), I1, insert_nth i P I2)"
  using MSB_mono by (auto simp del: insert_nth_take_drop split: order.splits)

lift_definition CONS :: "(bool list × bool list)  interp  interp"
  is "λ(bs1, bs2) (n, I1, I2).
   (Suc n, map_index (lift bs1) I1, map_index (lift bs2) I2)"
  by auto

lift_definition SNOC :: "(bool list × bool list)  interp  interp"
  is "λ(bs1, bs2) (n, I1, I2).
   (Suc n, map_index (snoc n bs1) I1, map_index (snoc n bs2) I2)"
  by (auto simp: Let_def)

type_synonym atom = "bool list × bool list"

lift_definition zero :: "idx  atom"
  is "λ(m, n). (replicate m False, replicate n False)" .

definition "extend ord b 
  λ(bs1, bs2). case ord of FO  (b # bs1, bs2) | SO  (bs1, b # bs2)"
lift_definition size_atom :: "bool list × bool list  idx"
  is "λ(bs1, bs2). (length bs1, length bs2)" .

lift_definition σ :: "idx  atom list"
  is "(λ(n, N). map (λbs. (take n bs, drop n bs)) (List.n_lists (n + N) [True, False]))" .

lemma fMin_fimage_Suc[simp]: "x |∈| A  fMin (Suc |`| A) = Suc (fMin A)"
  by (rule fMin_eqI) (auto intro: fMin_in)

lemma fMin_eq_0[simp]: "0 |∈| A  fMin A = (0 :: nat)"
  by (rule fMin_eqI) auto

lemma insert_nth_Cons[simp]:
  "insert_nth i x (y # xs) = (case i of 0  x # y # xs | Suc i  y # insert_nth i x xs)"
  by (cases i) simp_all

lemma insert_nth_commute[simp]:
  assumes "j  i" "i  length xs"
  shows "insert_nth j y (insert_nth i x xs) = insert_nth (Suc i) x (insert_nth j y xs)"
  using assms by (induct xs arbitrary: i j) (auto simp del: insert_nth_take_drop split: nat.splits)

lemma SUC_SUC[simp]: "SUC ord (SUC ord' idx) = SUC ord' (SUC ord idx)"
  by transfer (auto split: order.splits)

lemma LESS_SUC[simp]:
  "LESS ord 0 (SUC ord idx)"
  "LESS ord (Suc l) (SUC ord idx) = LESS ord l idx"
  "ord  ord'  LESS ord l (SUC ord' idx) = LESS ord l idx"
  "LESS ord l idx  LESS ord l (SUC ord' idx)"
  by (transfer, force split: order.splits)+

lemma nvars_Extend[simp]:
  "#V (Extend ord i 𝔄 P) = SUC ord (#V 𝔄)"
  by (transfer, force split: order.splits)

lemma Length_Extend[simp]:
  "Length (Extend k i 𝔄 P) = max (Length 𝔄) (if P = {||} then 0 else Suc (fMax P))"
  unfolding max_def by (split if_splits, transfer) (force split: order.splits)

lemma assigns_Extend[simp]:
  "LEQ ord i (#V 𝔄) mExtend ord i 𝔄 Pord = (if m = i then P else (if m > i then m - Suc 0 else m)𝔄ord)"
  "ord  ord'  mExtend ord i 𝔄 Pord' = m𝔄ord'"
  by (transfer, force simp: min_def nth_append split: order.splits)+

lemma Extend_commute_safe[simp]:
  "j  i; LEQ ord i (#V 𝔄) 
    Extend ord j (Extend ord i 𝔄 P1) P2 = Extend ord (Suc i) (Extend ord j 𝔄 P2) P1"
  by (transfer,
    force simp del: insert_nth_take_drop simp: replicate_add[symmetric] split: order.splits)

lemma Extend_commute_unsafe:
  "ord  ord'  Extend ord j (Extend ord' i 𝔄 P1) P2 = Extend ord' i (Extend ord j 𝔄 P2) P1"
  by (transfer, force simp: replicate_add[symmetric] split: order.splits)

lemma Length_CONS[simp]:
  "Length (CONS x 𝔄) = Suc (Length 𝔄)"
  by (transfer, force split: order.splits)

lemma Length_SNOC[simp]:
  "Length (SNOC x 𝔄) = Suc (Length 𝔄)"
  by (transfer, force simp: Let_def split: order.splits)

lemma nvars_CONS[simp]:
  "#V (CONS x 𝔄) = #V 𝔄"
  by (transfer, force)

lemma nvars_SNOC[simp]:
  "#V (SNOC x 𝔄) = #V 𝔄"
  by (transfer, force simp: Let_def)

lemma assigns_CONS[simp]:
  assumes "#V 𝔄 = size_atom bs1_bs2"
  shows "LESS ord x (#V 𝔄)  xCONS bs1_bs2 𝔄ord =
    (if case_prod case_order bs1_bs2 ord ! x then finsert 0 (upshift (x𝔄ord)) else upshift (x𝔄ord))"
  by (insert assms, transfer) (auto simp: lift_def split: order.splits)

lemma assigns_SNOC[simp]:
  assumes "#V 𝔄 = size_atom bs1_bs2"
  shows "LESS ord x (#V 𝔄)  xSNOC bs1_bs2 𝔄ord =
    (if case_prod case_order bs1_bs2 ord ! x then finsert (Length 𝔄) (x𝔄ord) else x𝔄ord)"
  by (insert assms, transfer) (force simp: snoc_def Let_def split: order.splits)

lemma map_index'_eq_conv[simp]:
  "map_index' i f xs = map_index' j g xs = (k < length xs. f (i + k) (xs ! k) = g (j + k) (xs ! k))"
proof (induct xs arbitrary: i j)
  case Cons from Cons(1)[of "Suc i" "Suc j"] show ?case by (auto simp: nth_Cons split: nat.splits)
qed simp

lemma fMax_Diff_0[simp]: "Suc m |∈| P  fMax (P |-| {|0|}) = fMax P"
  by (rule fMax_eqI) (auto intro: fMax_in dest: fMax_ge)

lemma Suc_fMax_pred_fimage[simp]:
  assumes "Suc p |∈| P" "0 |∉| P"
  shows "Suc (fMax ((λx. x - Suc 0) |`| P)) = fMax P"
  using assms by (subst mono_fMax_commute[of Suc, unfolded mono_def, simplified]) (auto simp: o_def)

lemma Extend_CONS[simp]: "#V 𝔄 = size_atom x  Extend ord 0 (CONS x 𝔄) P =
  CONS (extend ord (eval P 0) x) (Extend ord 0 𝔄 (downshift P))"
  by transfer (auto simp: extend_def o_def gr0_conv_Suc
    mono_fMax_commute[of Suc, symmetric, unfolded mono_def, simplified]
    lift_def upshift_def downshift_def eval_def
    dest!: fsubset_fsingletonD split: order.splits)

lemma size_atom_extend[simp]:
  "size_atom (extend ord b x) = SUC ord (size_atom x)"
  unfolding extend_def by transfer (simp split: prod.splits order.splits)

lemma size_atom_zero[simp]:
  "size_atom (zero idx) = idx"
  unfolding extend_def by transfer (simp split: prod.splits order.splits)

lemma interp_eqI:
  "Length 𝔄 = Length 𝔅; #V 𝔄 = #V 𝔅; m k. LESS k m (#V 𝔄)  m𝔄k = m𝔅k  𝔄 = 𝔅"
  by transfer (force split: order.splits intro!: nth_equalityI)

lemma Extend_SNOC_cut[unfolded eval_def cut_def Length_SNOC, simp]:
  "len P  Length (SNOC x 𝔄); #V 𝔄 = size_atom x 
  Extend ord 0 (SNOC x 𝔄) P =
    SNOC (extend ord (if eval P (Length 𝔄) then True else False) x) (Extend ord 0 𝔄 (cut (Length 𝔄) P))"
  by transfer (fastforce simp: extend_def len_def cut_def ffilter_eq_fempty_iff snoc_def eval_def
    split: if_splits order.splits dest: fMax_ge fMax_boundedD intro: fMax_in)

lemma nth_replicate_simp: "replicate m x ! i = (if i < m then x else [] ! (i - m))"
  by (induct m arbitrary: i) (auto simp: nth_Cons')

lemma MSB_eq_SucD: "MSB Is = Suc x  Pset Is. x |∈| P"
  using Max_in[of "xset Is. fset x"]
  unfolding MSB_def by (force split: if_splits)

lemma append_replicate_inj:
  assumes "xs  []  last xs  x" and "ys  []  last ys  x"
  shows "xs @ replicate m x = ys @ replicate n x  (xs = ys  m = n)"
proof safe
  from assms have assms': "xs  []  rev xs ! 0  x" "ys  []  rev ys ! 0  x"
    by (auto simp: hd_rev hd_conv_nth[symmetric])
  assume *: "xs @ replicate m x = ys @ replicate n x"
  then have "rev (xs @ replicate m x) = rev (ys @ replicate n x)" ..
  then have "replicate m x @ rev xs = replicate n x @ rev ys" by simp
  then have "take (max m n) (replicate m x @ rev xs) = take (max m n) (replicate n x @ rev ys)" by simp
  then have "replicate m x @ take (max m n - m) (rev xs) =
    replicate n x @ take (max m n - n) (rev ys)" by (auto simp: min_def max_def split: if_splits)
  then have "(replicate m x @ take (max m n - m) (rev xs)) ! min m n =
    (replicate n x @ take (max m n - n) (rev ys)) ! min m n" by simp
  with arg_cong[OF *, of length, simplified] assms' show "m = n"
    by (cases "xs = []" "ys = []" rule: bool.exhaust[case_product bool.exhaust])
      (auto simp: min_def nth_append split: if_splits)
  with * show "xs = ys" by auto
qed

lemma fin_lift[simp]: "m |∈| lift bs i (I ! i)  (case m of 0  bs ! i | Suc m  m |∈| I ! i)"
  unfolding lift_def upshift_def by (auto split: nat.splits)

lemma ex_Length_0[simp]:
  "𝔄. Length 𝔄 = 0  #V 𝔄 = idx"
  by transfer (auto intro!: exI[of _ "replicate m {||}" for m])

lemma is_empty_inj[simp]: "Length 𝔄 = 0; Length 𝔅 = 0; #V 𝔄 = #V 𝔅  𝔄 = 𝔅"
  by transfer (simp add: list_eq_iff_nth_eq split: prod.splits,
    metis MSB_greater fMax_in less_nat_zero_code)

lemma set_σ_length_atom[simp]: "(x  set (σ idx))  idx = size_atom x"
  by transfer (auto simp: set_n_lists enum_UNIV image_iff intro!: exI[of _ "I1 @ I2" for I1 I2])

lemma distinct_σ[simp]: "distinct (σ idx)"
  by transfer (auto 0 4 simp: distinct_map distinct_n_lists set_n_lists inj_on_def
    intro: iffD2[OF append_eq_append_conv]
      box_equals[OF _ append_take_drop_id append_take_drop_id, of n _ n for n])

lemma fMin_less_Length[simp]: "x |∈| m1𝔄k  fMin (m1𝔄k) < Length 𝔄"
  by transfer
    (force elim: order.strict_trans2[OF MSB_greater, rotated -1] intro: fMin_in split: order.splits)

lemma fMax_less_Length[simp]: "x |∈| m1𝔄k  fMax (m1𝔄k) < Length 𝔄"
  by transfer
    (force elim: order.strict_trans2[OF MSB_greater, rotated -1] intro: fMax_in split: order.splits)

lemma min_Length_fMin[simp]: "x |∈| m1𝔄k  min (Length 𝔄) (fMin (m1𝔄k)) = fMin (m1𝔄k)"
  using fMin_less_Length[of x m1 𝔄 k] unfolding fMin_def by auto

lemma max_Length_fMin[simp]: "x |∈| m1𝔄k  max (Length 𝔄) (fMin (m1𝔄k)) = Length 𝔄"
  using fMin_less_Length[of x m1 𝔄 k] unfolding fMin_def by auto

lemma min_Length_fMax[simp]: "x |∈| m1𝔄k  min (Length 𝔄) (fMax (m1𝔄k)) = fMax (m1𝔄k)"
  using fMax_less_Length[of x m1 𝔄 k] unfolding fMax_def by auto

lemma max_Length_fMax[simp]: "x |∈| m1𝔄k  max (Length 𝔄) (fMax (m1𝔄k)) = Length 𝔄"
  using fMax_less_Length[of x m1 𝔄 k] unfolding fMax_def by auto

lemma assigns_less_Length[simp]: "x |∈| m1𝔄k  x < Length 𝔄"
  by transfer (force dest: MSB_greater split: order.splits if_splits)

lemma Length_notin_assigns[simp]: "Length 𝔄 |∉| m𝔄k"
  by (metis assigns_less_Length less_not_refl)

lemma nth_zero[simp]: "LESS ord m (#V 𝔄)  ¬ case_prod case_order (zero (#V 𝔄)) ord ! m"
  by transfer (auto split: order.splits)

lemma in_fimage_Suc[simp]: "x |∈| Suc |`| A  (y. y |∈| A  x = Suc y)"
  by blast

lemma fimage_Suc_inj[simp]: "Suc |`| A = Suc |`| B  A = B"
  by blast

lemma MSB_eq0_D: "MSB I = 0  x < length I  I ! x = {||}"
  unfolding MSB_def by (auto split: if_splits)

lemma Suc_in_fimage_Suc: "Suc x |∈| Suc |`| X  x |∈| X"
  by auto

lemma Suc_in_fimage_Suc_o_Suc[simp]: "Suc x |∈| (Suc  Suc) |`| X  x |∈| Suc |`| X"
  by auto

lemma finsert_same_eq_iff[simp]: "finsert k X = finsert k Y  X |-| {|k|} = Y |-| {|k|}"
  by auto


lemma fimage_Suc_o_Suc_eq_fimage_Suc_iff[simp]:
  "((Suc  Suc) |`| X = Suc |`| Y)  (Suc |`| X = Y)"
  by (metis fimage_Suc_inj fset.map_comp)

lemma fMax_image_Suc[simp]: "x |∈| P  fMax (Suc |`| P) = Suc (fMax P)"
  by (rule fMax_eqI) (metis Suc_le_mono fMax_ge fimageE, metis fimageI fempty_iff fMax_in)

lemma fimage_Suc_eq_singleton[simp]: "(fimage Suc Z = {|y|})  (x. Z = {|x|}  Suc x = y)"
  by (cases y) auto

lemma len_downshift_helper:
  "x |∈| P  Suc (fMax ((λx. x - Suc 0) |`| (P |-| {|0|})))  fMax P  xa |∈| P  xa = 0"
proof -
  assume a1: "xa |∈| P"
  assume a2: "Suc (fMax ((λx. x - Suc 0) |`| (P |-| {|0|})))  fMax P"
  have "xa |∈| {|0|}  xa = 0" by fastforce
  moreover
  { assume "xa |∉| {|0|}"
    hence "0 |∉| P |-| {|0|}  xa |∉| {|0|}" by blast
    then obtain esk11 :: "nat  nat" where "xa = 0" using a1 a2 by (metis Suc_fMax_pred_fimage fMax_Diff_0 fminus_iff not0_implies_Suc) }
  ultimately show "xa = 0" by blast
qed

lemma CONS_inj[simp]: "size_atom x = #V 𝔄  size_atom y = #V 𝔄  #V 𝔄 = #V 𝔅 
  CONS x 𝔄 = CONS y 𝔅  (x = y  𝔄 = 𝔅)"
  by transfer (auto simp: list_eq_iff_nth_eq lift_def upshift_def split: if_splits; blast)

lemma Suc_minus1: "Suc (x - Suc 0) = (if x = 0 then Suc 0 else x)"
  by auto

lemma fset_eq_empty_iff: "(fset X = {}) = (X = {||})"
  by (metis bot_fset.rep_eq fset_inverse)

lemma fset_le_singleton_iff: "(fset X  {x}) = (X = {||}  X = {|x|})"
  by (metis finsert.rep_eq fset_eq_empty_iff fset_inject order_refl singleton_insert_inj_eq subset_singletonD)

lemma MSB_decreases:
  "MSB I  Suc m  MSB (map (λX. (λI1. I1 - Suc 0) |`| (X |-| {|0|})) I)  m"
  unfolding MSB_def
  by (auto simp add: not_le less_Suc_eq_le fset_eq_empty_iff fset_le_singleton_iff
    split: if_splits dest!: iffD1[OF Max_le_iff, rotated -1] iffD1[OF Max_ge_iff, rotated -1]; force)

lemma CONS_surj[dest]:
  assumes "Length 𝔄 > 0"
  shows "x 𝔅. 𝔄 = CONS x 𝔅  #V 𝔅 = #V 𝔄  size_atom x = #V 𝔄"
proof -
  have "MSB I1  Suc m  MSB I2  Suc m  a b ab ba.
    (I1. length ab = length I1  (i<length ab. ab ! i = I1 ! i) 
      (I2. length ba = length I2  (i<length ba. ba ! i = I2 ! i) 
        MSB I1  m  MSB I2  m)) 
    I1 = map_index (lift a) ab 
    I2 = map_index (lift b) ba 
    length ab = length I1 
    length ba = length I2 
    length a = length I1 
    length b = length I2"
    for m I1 I2
    by (auto simp: list_eq_iff_nth_eq lift_def upshift_def split: if_splits
        intro!: exI[of _ "map (λX. 0 |∈| X) _"] exI[of _ "map (λX. (λx. x - Suc 0) |`| (X |-| {|0|})) _"],
        auto simp: MSB_decreases upshift_def Suc_minus1 fimage_iff intro: rev_fBexI split: if_splits)
  with assms show ?thesis
    by transfer (auto simp: gr0_conv_Suc list_eq_iff_nth_eq)
qed
 
(*<*)
end
(*>*)