Theory BIT_pairwise

theory BIT_pairwise
imports List_Factoring BIT

section "BIT is pairwise"

theory BIT_pairwise
imports List_Factoring BIT
begin

lemma L_nths: "S ⊆ {..<length init}
  ⟹ map_pmf (λl. nths l S) (Prob_Theory.bv (length init))
      = (Prob_Theory.bv (length (nths init S)))"
proof(induct init arbitrary: S)
  case (Cons a as)
  then have passt: "{j. Suc j ∈ S} ⊆ {..<length as}" by auto

  have " map_pmf (λl. nths l S) (Prob_Theory.bv (length (a # as))) = 
    Prob_Theory.bv (length as) ⤜
    (λx. bernoulli_pmf (1 / 2) ⤜
          (λxa. return_pmf
                  ((if 0 ∈ S then [xa] else []) @ nths x {j. Suc j ∈ S})))"
      by(simp add: map_pmf_def bind_return_pmf bind_assoc_pmf nths_Cons) 
  also have "… = (bernoulli_pmf (1 / 2)) ⤜ 
          (λxa. (Prob_Theory.bv (length as) ⤜
    (λx. return_pmf ((if 0 ∈ S then [xa] else []) @ nths x {j. Suc j ∈ S}))))"
        by(rule bind_commute_pmf)
   also have "… = (bernoulli_pmf (1 / 2)) ⤜ 
          (λxa. (map_pmf (λx. (nths x {j. Suc j ∈ S})) (Prob_Theory.bv (length as)))
              ⤜  (λxs. return_pmf ((if 0 ∈ S then [xa] else []) @ xs)))"
      by(simp add: bind_return_pmf bind_assoc_pmf map_pmf_def)
   also have "… = (bernoulli_pmf (1 / 2)) ⤜ 
          (λxa. Prob_Theory.bv (length (nths as {j. Suc j ∈ S}))
              ⤜  (λxs. return_pmf ((if 0 ∈ S then [xa] else []) @ xs)))"
        using Cons(1)[OF passt] by auto
   also have "… = Prob_Theory.bv (length (nths (a # as) S))"
      apply(auto simp add: nths_Cons bind_return_pmf')
      by(rule bind_commute_pmf)
   finally show ?case .
qed (simp)

lemma L_nths_Lxy:
  assumes "x∈set init" "y∈set init" "x≠y" "distinct init" 
  shows "map_pmf (λl. nths l {index init x,index init y}) (Prob_Theory.bv (length init))
      = (Prob_Theory.bv (length (Lxy init {x,y})))"
proof -
  from assms(4) have setinit: "(index init) ` set init = {0..<length init}" 
  proof(induct init)
    case (Cons a as)
    with Cons have iH: "index as ` set as = {0..<length as}" by auto
    from Cons have 1:"(set as ∩ {x. (a ≠ x)}) = set as" by fastforce
    have 2: "(λa. Suc (index as a)) ` set as =
            (λa. Suc a) ` ((index as) ` set as )" by auto
    show ?case
    apply(simp add: 1 2 iH) by auto
  qed simp

  have xy_le: "index init x<length init" "index init y<length init" using assms by auto
  have "map_pmf (λl. nths l {index init x,index init y}) (Prob_Theory.bv (length init))
      = (Prob_Theory.bv (length (nths init {index init x,index init y})))"
        apply(rule L_nths)
        using assms(1,2) by auto
  moreover have "length (Lxy init {x,y}) = length (nths init {index init x,index init y})"
  proof -
    have "set (Lxy init {x,y}) = {x,y}" 
      using assms(1,2) by(simp add: Lxy_set_filter)
    moreover have "card {x,y} = 2" using assms(3) by auto
    moreover have "distinct (Lxy init {x,y})" using assms(4) by(simp add: Lxy_distinct)
    ultimately have 1: "length (Lxy init {x,y}) = 2" by(simp add: distinct_card[symmetric])
    have "set (nths init {index init x,index init y}) = {(init ! i) | i.  i < length init ∧ i ∈ {index init x,index init y}}" 
      using assms(1,2) by(simp add: set_nths)
    moreover have "card {(init ! i) | i.  i < length init ∧ i ∈ {index init x,index init y}} = 2"
    proof -
      have 1: "{(init ! i) | i.  i < length init ∧ i ∈ {index init x,index init y}} = {init ! index init x, init ! index init y}" using xy_le by blast
      also have "… = {x,y}" using nth_index assms(1,2) by auto 
      finally show ?thesis using assms(3) by auto
    qed
    moreover have "distinct (nths init {index init x,index init y})" using assms(4) by(simp)
    ultimately have 2: "length (nths init {index init x,index init y}) = 2" by(simp add: distinct_card[symmetric])
    show ?thesis using 1 2 by simp
  qed
  ultimately show ?thesis by simp
qed
  
lemma nths_map: "map f (nths xs S) = nths (map f xs) S"
apply(induct xs arbitrary: S) by(simp_all  add: nths_Cons)

lemma nths_empty: "(∀i∈S. i≥length xs) ⟹ nths xs S = []"
proof -
  assume "(∀i∈S. i≥length xs)"
  then have "set (nths xs S) = {}" apply(simp add: set_nths) by force
  then show "nths xs S = []" by simp
qed


lemma nths_project': "i < length xs ⟹ j < length xs ⟹ i<j
   ⟹ nths xs {i,j} = [xs!i, xs!j]"
proof -
  assume il: "i < length xs" and jl: "j < length xs" and ij: "i<j"

  from il obtain a as where dec1: "a @ [xs!i] @ as = xs" 
           and "a = take i xs" "as=drop (Suc i) xs" 
           and length_a: "length a = i" and length_as: "length as = length xs - i - 1"using id_take_nth_drop by fastforce
  have "j≥length (a @ [xs!i])" using length_a ij by auto
  then have "((a @ [xs!i]) @ as) ! j = as ! (j-length (a @ [xs ! i]))" using nth_append[where xs="a @ [xs!i]" and ys="as"]
    by(simp)
  then have xsj: "xs ! j = as ! (j-i-1)" using dec1 length_a by auto   
  have las: "(j-i-1) < length as" using length_as jl ij by simp
  obtain b c where dec2: "b @ [xs!j] @ c = as"
            and "b = take (j-i-1) as" "c=drop (Suc (j-i-1)) as"
            and length_b: "length b = j-i-1" using id_take_nth_drop[OF las] xsj by force
  have xs_dec: "a @ [xs!i] @ b @ [xs!j] @ c = xs" using dec1 dec2 by auto 
         
  have s2: "{k. (k + i ∈ {i, j})} = {0,j-i}"  using ij by force
  have s3: "{k. (k  + length [xs ! i] ∈ {0, j-i})} = {j-i-1}"  using ij by force
  have s4: "{k. (k  + length b ∈ {j-i-1})} = {0}"  using length_b by force
  have s5: "{k. (k  + length [xs!j] ∈ {0})} = {}" by force
  have l1: "nths a {i,j} = []"
    apply(rule nths_empty) using length_a ij by fastforce
  have l2: "nths b {j - Suc i} = []"
    apply(rule nths_empty) using length_b ij by fastforce
  have "nths ( a @ [xs!i] @ b @ [xs!j] @ c) {i,j} = [xs!i, xs!j]"
      apply(simp only: nths_append length_a s2 s3 s4 s5)
      by(simp add: l1 l2)
  then show "nths xs {i,j} = [xs!i, xs!j]" unfolding xs_dec .
qed

lemma nths_project:
  assumes  "i < length xs" "j < length xs" "i<j"
   shows "nths xs {i,j} ! 0 = xs ! i ∧ nths xs {i,j} ! 1 = xs ! j"
proof -
  from assms have "nths xs {i,j} = [xs!i, xs!j]" by(rule nths_project')
  then show ?thesis by simp
qed

lemma BIT_pairwise':
  assumes "set qs ⊆ set init"    
    "(x,y)∈ {(x,y). x ∈ set init ∧ y∈set init ∧ x≠y}"
   and  xny:"x ≠ y" and dinit: "distinct init"
  shows "Pbefore_in x y BIT qs init = Pbefore_in x y BIT (Lxy qs {x,y}) (Lxy init {x,y})"                    
proof -
  from assms have xyininit: "{x, y} ⊆ set init" 
        and qsininit: "set qs ⊆ set init" by auto 

  have xyininit': "{y,x} ⊆ set init" using xyininit by auto
 
  have a: "x ∈ set init" "y∈set init" using assms by auto 

    { fix n
    have strong: "set qs ⊆ set init ⟹
      map_pmf (λ(l,(w,i)). (Lxy l {x,y},(nths w {index init x,index init y},Lxy init {x,y}))) (config_rand BIT init qs) =
      config_rand BIT (Lxy init {x, y}) (Lxy qs {x, y}) " (is "?inv ⟹ ?L qs = ?R qs")
    proof (induct qs rule: rev_induct)
      case Nil 

      have " map_pmf (λ(l,(w,i)). (Lxy l {x,y},(nths w {index init x,index init y},Lxy init {x,y}))) (config_rand BIT init [])
          =  map_pmf (λw. (Lxy init {x,y}, (w, Lxy init {x,y}))) (map_pmf (λl. nths l {index init x,index init y}) (Prob_Theory.bv (length init)))"
              by(simp add: bind_return_pmf map_pmf_def bind_assoc_pmf split_def BIT_init_def)
      also have "… = map_pmf (λw. (Lxy init {x,y}, (w, Lxy init {x,y}))) (Prob_Theory.bv (length (Lxy init {x, y})))" 
          using L_nths_Lxy[OF a xny dinit] by simp
      also have "… = config_rand BIT  (Lxy init {x, y}) (Lxy [] {x, y})"
          by(simp add: BIT_init_def bind_return_pmf bind_assoc_pmf map_pmf_def)
      finally show ?case . 
    next
      case (snoc q qs)
      then have qininit: "q ∈  set init" 
            and qsininit: "set qs ⊆ set init" using qsininit by auto

      from  snoc(1)[OF qsininit] have iH: "?L qs = ?R qs" by (simp add: split_def)

      show ?case 
      proof (cases "q ∈ {x,y}")
        case True
        note whatisq=this
 
        have "?L (qs@[q]) =
         map_pmf (λ(l,(w,i)). (Lxy l {x,y},(nths w {index init x,index init y},Lxy init {x,y}))) (config_rand BIT init qs ⤜
              (λs. BIT_step s q ⤜ (λ(a, nis). return_pmf (step (fst s) q a, nis))))"
             by(simp add: split_def config'_rand_snoc) 
        also have "… =
        map_pmf (λ(l,(w,i)). (Lxy l {x,y}, (nths w {index init x,index init y},Lxy init {x,y}))) (config_rand BIT init qs) ⤜
        (λs.
            BIT_step s q ⤜
            (λ(a, nis). return_pmf (step (fst s) q a, nis))) "
           apply(simp add: map_pmf_def split_def bind_return_pmf bind_assoc_pmf)
           apply(simp add: BIT_step_def bind_return_pmf)
        proof (rule bind_pmf_cong, goal_cases)
          case (2 z)
          let ?s = "fst z"
          let ?b = "fst (snd z)"

          from 2 have z: "set (?s) = set init" using config_rand_set[of BIT, simplified]  by metis
          with True have qLxy: "q ∈ set (Lxy (?s) {x, y})" using   xyininit by (simp add: Lxy_set_filter)
          from 2 have dz: "distinct (?s)" using dinit config_rand_distinct[of BIT, simplified] by metis
          then have dLxy: "distinct (Lxy (?s) {x, y})" using Lxy_distinct by auto

          from 2 have [simp]: "snd (snd z) = init" using config_n_init3[simplified]   by metis

          from 2 have [simp]: "length (fst (snd z)) = length init" using config_n_fst_init_length2[simplified] by metis 

          have indexinbounds: "index init x < length init" "index init y < length init"  using a by auto
          from a xny have indnot: "index init x ≠ index init y" by auto



          have f1: "index init x < length (fst (snd z))" using xyininit by auto
          have f2: "index init y < length (fst (snd z))" using xyininit by auto
          have 3: "index init x ≠ index init y" using xny xyininit by auto

          
          from dinit have dfil: "distinct (Lxy init {x,y})" by(rule Lxy_distinct)
          have Lxy_set: "set (Lxy init {x, y}) = {x,y}" apply(simp add: Lxy_set_filter) using xyininit by fast
          then have xLxy: "x∈set (Lxy init {x, y})" by auto
          have Lxy_length: "length (Lxy init {x, y}) = 2" using dfil Lxy_set xny distinct_card by fastforce 
          have 31:  "index (Lxy init {x, y}) x < 2" 
              and  32:  "index (Lxy init {x, y}) y < 2" using Lxy_set xyininit Lxy_length by auto
          have 33: "index (Lxy init {x, y}) x ≠ index (Lxy init {x,y}) y"
            using xny xLxy by auto
 
          have a1: "nths (flip (index init (q)) (fst (snd z))) {index init x,index init y}
                = flip (index (Lxy init {x,y}) (q)) (nths (fst (snd z)) {index init x,index init y})" (is "?A=?B")
          proof (simp only: list_eq_iff_nth_eq, goal_cases)
            case 1

            {assume ass: "index init x < index init y"
              then have "index (Lxy init {x,y}) x < index (Lxy init {x,y}) y"
                using Lxy_mono[OF xyininit dinit] before_in_def a(2) by force  
              with 31 32 have ix: "index (Lxy init {x,y}) x = 0"
                      and iy: "index (Lxy init {x,y}) y = 1" by auto


             have g1: "(nths (fst (snd z)) {index init x,index init y}) 
                        = [(fst (snd z)) ! index init x, (fst (snd z)) ! index init y]"
                        apply(rule nths_project')
                          using xyininit apply(simp)
                          using xyininit apply(simp)
                          by fact


            have "nths (flip (index init (q)) (fst (snd z))) {index init x,index init y}
                  = [flip (index init (q)) (fst (snd z))!index init x,
                        flip (index init (q)) (fst (snd z))!index init y]"
                        apply(rule nths_project')
                          using xyininit apply(simp)
                          using xyininit apply(simp)
                          by fact
            also have "… = flip (index (Lxy init {x,y}) (q)) [(fst (snd z)) ! index init x, (fst (snd z)) ! index init y]" 
              apply(cases "q=x")
                apply(simp add: ix) using flip_other[OF f2 f1 3] flip_itself[OF f1] apply(simp)
                using whatisq apply(simp add: iy) using flip_other[OF f1 f2 3[symmetric]] flip_itself[OF f2] by(simp)
            finally have "nths (flip (index init (q)) (fst (snd z))) {index init x,index init y}
                    = flip (index (Lxy init {x,y}) (q)) (nths (fst (snd z)) {index init x,index init y})" 
                    by(simp add: g1)
                          
            }note cas1=this
            have man: "{x,y} = {y,x}" by auto
            {assume "~ index init x < index init y"
              then have ass: "index init y < index init x" using 3 by auto
              then have "index (Lxy init {x,y}) y < index (Lxy init {x,y}) x"
                using Lxy_mono[OF xyininit' dinit] xyininit a(1) man by(simp add: before_in_def)
              with 31 32 have ix: "index (Lxy init {x,y}) x = 1"
                      and iy: "index (Lxy init {x,y}) y = 0" by auto


             have g1: "(nths (fst (snd z)) {index init y,index init x}) 
                        = [(fst (snd z)) ! index init y, (fst (snd z)) ! index init x]"
                        apply(rule nths_project')
                          using xyininit apply(simp)
                          using xyininit apply(simp)
                          by fact

            have man2: "{index init x,index init y} = {index init y,index init x}" by auto
            have "nths (flip (index init (q)) (fst (snd z))) {index init y,index init x}
                  = [flip (index init (q)) (fst (snd z))!index init y,
                        flip (index init (q)) (fst (snd z))!index init x]"
                        apply(rule nths_project')
                          using xyininit apply(simp)
                          using xyininit apply(simp)
                          by fact
            also have "… = flip (index (Lxy init {x,y}) (q)) [(fst (snd z)) ! index init y, (fst (snd z)) ! index init x]" 
              apply(cases "q=x")
                apply(simp add: ix) using flip_other[OF f2 f1 3] flip_itself[OF f1] apply(simp)
                using whatisq apply(simp add: iy) using flip_other[OF f1 f2 3[symmetric]] flip_itself[OF f2] by(simp)
            finally have "nths (flip (index init (q)) (fst (snd z))) {index init y,index init x}
                    = flip (index (Lxy init {x,y}) (q)) (nths (fst (snd z)) {index init y,index init x})" 
                    by(simp add: g1)
            then have "nths (flip (index init (q)) (fst (snd z))) {index init x,index init y}
                    = flip (index (Lxy init {x,y}) (q)) (nths (fst (snd z)) {index init x,index init y})" 
                    using man2 by auto                          
            } note cas2=this

            from cas1 cas2 3 show ?case by metis 
          qed

          have a: "nths (fst (snd z)) {index init x, index init y} ! (index (Lxy init {x,y}) (q))
                    = fst (snd z) ! (index init (q))"
          proof -
            from 31 32  33have ca: "(index (Lxy init {x,y}) x = 0 ∧ index (Lxy init {x,y}) y = 1)
                    ∨ (index (Lxy init {x,y}) x = 1 ∧ index (Lxy init {x,y}) y = 0)" by force
            show ?thesis
            proof (cases "index (Lxy init {x,y}) x = 0")
              case True

              from True ca have y1: "index (Lxy init {x,y}) y = 1" by auto
              with True have "index (Lxy init {x,y}) x < index (Lxy init {x,y}) y" by auto
              then have xy: "index init x < index init y" using dinit dfil Lxy_mono 
                      using "32" before_in_def Lxy_length xyininit by fastforce 
                  

              have 4: " {index init y, index init x} =  {index init x, index init y}" by auto

              have "nths (fst (snd z)) {index init x, index init y} ! index (Lxy init {x,y}) x = (fst (snd z)) ! index init x"
                       "nths (fst (snd z)) {index init x, index init y} ! index (Lxy init {x,y}) y = (fst (snd z)) ! index init y"
                       unfolding True y1 
                          by (simp_all only: nths_project[OF f1 f2 xy])  
              with whatisq show ?thesis by auto
           next
              case False
              with ca have x1: "index (Lxy init {x,y}) x = 1" by auto
              from dinit have dfil: "distinct (Lxy init {x,y})" by(rule Lxy_distinct)

              from x1 ca have y1: "index (Lxy init {x,y}) y = 0" by auto
              with x1 have "index (Lxy init {x,y}) y < index (Lxy init {x,y}) x" by auto
              then have xy: "index init y < index init x" using dinit dfil Lxy_mono 
                      using "32" before_in_def Lxy_length xyininit by (metis a(2) indnot linorder_neqE_nat not_less0 y1) 
                  

              have 4: " {index init y, index init x} =  {index init x, index init y}" by auto
 
              have "nths (?b) {index init x, index init y} ! index (Lxy init {x,y}) x = (?b) ! index init x"
                       "nths (?b) {index init x, index init y} ! index (Lxy init {x,y}) y = (?b) ! index init y"
                       unfolding x1 y1 
                        using 4 nths_project[OF  f2 f1 xy]
                          by simp_all  
              with whatisq show ?thesis by auto
           qed
         qed


          have b: "Lxy (mtf2 (length ?s) (q) ?s) {x, y} 
                =  mtf2 (length (Lxy ?s {x, y})) (q) (Lxy ?s {x, y})" (is "?A = ?B")
          proof -
                have sA: "set ?A = {x,y}" using z xyininit by(simp add: Lxy_set_filter)
                then have xlxymA: "x ∈ set ?A"
                      and ylxymA: "y ∈ set ?A" by auto
                have dA: "distinct ?A" apply(rule Lxy_distinct) by(simp add: dz)
                have lA: "length ?A = 2" using xny sA dA distinct_card by fastforce 
                from lA ylxymA have yindA: "index ?A y < 2" by auto
                from lA xlxymA have xindA: "index ?A x < 2" by auto
                have geA: "{x,y} ⊆ set (mtf2 (length ?s) (q) ?s)" using xyininit z by auto
                have geA': "{y,x} ⊆ set (mtf2 (length ?s) (q) (?s))" using xyininit z by auto
                have man: "{y,x} = {x,y}" by auto

                have sB: "set ?B = {x,y}" using z xyininit by(simp add: Lxy_set_filter)
                then have xlxymB: "x ∈ set ?B"
                  and ylxymB: "y ∈ set ?B" by auto
                have dB: "distinct ?B" apply(simp) apply(rule Lxy_distinct) by(simp add: dz)
                have lB: "length ?B = 2" using xny sB dB distinct_card by fastforce 
                from lB ylxymB have yindB: "index ?B y < 2" by auto
                from lB xlxymB have xindB: "index ?B x < 2" by auto
                
                show ?thesis
                proof (cases "q = x")                
                  case True
                  then have xby: "x < y in (mtf2 (length (?s)) (q) (?s))"
                    apply(simp)
                          apply(rule mtf2_moves_to_front''[simplified])
                            using z xyininit xny by(simp_all add: dz)
                  then have "x < y in ?A" using Lxy_mono[OF geA] dz by(auto)
                  then have "index ?A x < index ?A y" unfolding before_in_def by auto
                  then have in1: "index ?A x = 0"
                          and in2: "index ?A y = 1"  using yindA by auto
                  have "?A = [?A!0,?A!1]" 
                          apply(simp only: list_eq_iff_nth_eq)
                            apply(auto simp: lA) apply(case_tac i) by(auto)
                  also have "… = [?A!index ?A x, ?A!index ?A y]" by(simp only: in1 in2)
                  also have "… = [x,y]" using xlxymA ylxymA  by simp    
                  finally have end1: "?A  = [x,y]" .
                  
                  have "x < y in ?B"
                    using True apply(simp)
                          apply(rule mtf2_moves_to_front''[simplified])
                            using z xyininit xny by(simp_all add: Lxy_distinct dz Lxy_set_filter)
                  then have "index ?B x < index ?B y"
                            unfolding before_in_def by auto
                  then have in1: "index ?B x = 0"
                          and in2: "index ?B y = 1"
                            using yindB by auto
  
                  have "?B = [?B!0, ?B!1]" 
                          apply(simp only: list_eq_iff_nth_eq)
                            apply(simp only: lB)
                            apply(auto) apply(case_tac i) by(auto)
                  also have "… = [?B!index ?B x,  ?B!index ?B y]"
                                 by(simp only: in1 in2)
                  also have "… = [x,y]" using xlxymB ylxymB  by simp    
                  finally have end2: "?B = [x,y]" .
  
                  then show "?A = ?B " using end1 end2 by simp
              next             
                  case False
                  with whatisq have qsy: "q=y" by simp
                  then have xby: "y < x in (mtf2 (length (?s)) (q) (?s))"
                    apply(simp)
                          apply(rule mtf2_moves_to_front''[simplified])
                            using z xyininit xny by(simp_all add: dz)
                  then have "y < x in ?A" using Lxy_mono[OF geA'] man dz by auto
                  then have "index ?A y < index ?A x" unfolding before_in_def by auto
                  then have in1: "index ?A y = 0"
                          and in2: "index ?A x = 1"  using xindA by auto
                  have "?A = [?A!0,?A!1]" 
                          apply(simp only: list_eq_iff_nth_eq)
                            apply(auto simp: lA) apply(case_tac i) by(auto)
                  also have "… = [?A!index ?A y, ?A!index ?A x]" by(simp only: in1 in2)
                  also have "… = [y,x]" using xlxymA ylxymA  by simp    
                  finally have end1: "?A  = [y,x]" .
                  
                  have "y < x in ?B"
                    using qsy apply(simp)
                          apply(rule mtf2_moves_to_front''[simplified])
                            using z xyininit xny by(simp_all add: Lxy_distinct dz Lxy_set_filter)
                  then have "index ?B y < index ?B x"
                            unfolding before_in_def by auto
                  then have in1: "index ?B y = 0"
                          and in2: "index ?B x = 1"
                            using xindB by auto
  
                  have "?B = [?B!0, ?B!1]" 
                          apply(simp only: list_eq_iff_nth_eq)
                            apply(simp only: lB)
                            apply(auto) apply(case_tac i) by(auto)
                  also have "… = [?B!index ?B y,  ?B!index ?B x]"
                                 by(simp only: in1 in2)
                  also have "… = [y,x]" using xlxymB ylxymB  by(simp )    
                  finally have end2: "?B = [y,x]" .
  
                  then show "?A = ?B " using end1 end2 by simp
              qed  
           qed 
          
          have a2: " Lxy (step (?s) (q) (if ?b ! (index init (q)) then 0 else length (?s), [])) {x, y}
              = step (Lxy (?s) {x, y}) (q) (if nths (?b) {index init x, index init y} ! (index (Lxy init {x,y}) (q)) 
                              then 0 
                              else length (Lxy (?s) {x, y}), [])"
               apply(auto simp add: a step_def) by(simp add: b)
 

           show ?case using a1 a2 by(simp)
        qed simp 
        also have "… = ?R (qs@[q])"
          using True apply(simp add: Lxy_snoc take_Suc_conv_app_nth config'_rand_snoc)  
          using iH by(simp add: split_def ) 
        finally show ?thesis .
      next
        case False
        then have qnx: "(q) ≠ x" and qny: "(q) ≠ y" by auto

        let ?proj="(λa. (Lxy (fst a) {x, y}, (nths (fst (snd a)) {index init x, index init y}, Lxy init {x, y})))"
             
        have "map_pmf ?proj (config_rand BIT init (qs@[q]))
             = map_pmf ?proj (config_rand (BIT_init, BIT_step) init qs
                ⤜ (λp. BIT_step p (q) ⤜ (λpa. return_pmf (step (fst p) (q) (fst pa), snd pa)))) "
               by (simp add: split_def take_Suc_conv_app_nth config'_rand_snoc)
        also have "… = map_pmf ?proj (config_rand (BIT_init, BIT_step) init qs)" 
            apply(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf BIT_step_def)
            proof (rule bind_pmf_cong, goal_cases)
              case (2 z)
              let ?s = "fst z"
              let ?m = "snd (snd z)"
              let ?b = "fst (snd z)"

              from 2 have sf_init: "?m = init" using config_n_init3 by auto

              from 2 have ff_len: "length (?b) = length init" using config_n_fst_init_length2 by auto
              
              have ff_ix: "index init x < length (?b)" unfolding ff_len using a(1) by auto
              have ff_iy: "index init y < length (?b)" unfolding ff_len using a(2) by auto
              have ff_q: "index init (q) < length (?b)" unfolding ff_len using qininit by auto
              have iq_ix: "index init (q) ≠ index init x" using a(1) qnx by auto
              have iq_iy: "index init (q) ≠ index init y" using a(2) qny by auto
              have ix_iy: "index init x ≠ index init y" using a(2) xny by auto

              from 2 have s_set[simp]: "set (?s) = set init" using config_rand_set by force
              have s_xin: "x∈set (?s)" using a(1) by simp
              have s_yin: "y∈set (?s)" using a(2) by simp
              from 2 have s_dist: "distinct (?s)" using config_rand_distinct dinit by force
              have s_qin: "q ∈ set (?s)" using qininit by simp


              have fstfst: "nths (flip (index ?m (q)) (?b))
              {index init x, index init y}
                  = nths (?b) {index init x, index init y}" (is "nths ?A ?I = nths ?B ?I")
              proof (cases "index init x < index init y")
                case True
                have "nths ?A ?I = [?A!index init x, ?A!index init y]"
                      apply(rule nths_project')
                        by(simp_all add: ff_ix ff_iy True)
                also have "… = [?B!index init x, ?B!index init y]"
                  unfolding sf_init using flip_other ff_ix ff_iy ff_q iq_ix iq_iy by auto
                also have "… = nths ?B ?I"
                      apply(rule nths_project'[symmetric])
                        by(simp_all add: ff_ix ff_iy True)
                finally show ?thesis .
              next
                case False
                then have yx: "index init y < index init x" using ix_iy by auto
                have man: "?I =  {index init y, index init x}" by auto
                have "nths ?A {index init y, index init x}  = [?A!index init y, ?A!index init x]"
                      apply(rule nths_project')
                        by(simp_all add: ff_ix ff_iy yx)
                also have "… = [?B!index init y, ?B!index init x]"
                  unfolding sf_init using flip_other ff_ix ff_iy ff_q iq_ix iq_iy by auto
                also have "… = nths ?B {index init y, index init x}"
                      apply(rule nths_project'[symmetric])
                        by(simp_all add: ff_ix ff_iy yx)
                finally show ?thesis by(simp add: man)
              qed


              have snd: "Lxy (step (?s) (q)
                  (if ?b ! index ?m (q) then 0 else length (?s),
                   [])) {x, y} = Lxy (?s) {x, y}" (is "Lxy ?A {x,y} = Lxy ?B {x,y}")
              proof (cases "x < y in ?B")
                case True
                note B=this
                then have A: "x<y in ?A" apply(auto simp add: step_def split_def)
                  apply(rule x_stays_before_y_if_y_not_moved_to_front)
                    by(simp_all add: a s_dist qny[symmetric] qininit)

                have "Lxy ?A {x,y} = [x,y]"
                  apply(rule Lxy_project)
                    by(simp_all add: xny set_step distinct_step A s_dist a)
                also have "... = Lxy ?B {x,y}"
                  apply(rule Lxy_project[symmetric])
                    by(simp_all add: xny B s_dist a)
                finally show ?thesis .
              next
                case False
                then have B: "y < x in ?B" using not_before_in[OF s_xin s_yin] xny by simp
                then have A: "y < x in ?A " apply(auto simp add: step_def split_def)
                  apply(rule x_stays_before_y_if_y_not_moved_to_front)
                    by(simp_all add: a s_dist qnx[symmetric] qininit)
                have man: "{x,y} = {y,x}" by auto
                have "Lxy ?A {y,x} = [y,x]"
                  apply(rule Lxy_project)
                    by(simp_all add: xny[symmetric] set_step distinct_step A s_dist a)
                also have "... = Lxy ?B {y,x}"
                  apply(rule Lxy_project[symmetric])
                    by(simp_all add: xny[symmetric] B s_dist a)
                finally show ?thesis using man by auto
              qed
 
              show ?case by(simp add: fstfst snd)
            qed simp
        also have "… = config_rand BIT (Lxy init {x, y}) (Lxy qs {x, y})"
          using iH by (auto simp: split_def)
        also have "… = ?R (qs@[q])"
          using False by(simp add: Lxy_snoc)
        finally show ?thesis by (simp add: split_def)
      qed 
    qed
    } note strong=this

  { 
    fix n::nat 
    have "Pbefore_in x y BIT qs init = 
        map_pmf (λp. x < y in fst p)
            (map_pmf (λ(l, (w, i)). (Lxy l {x, y}, (nths w {index init x, index init y}, Lxy init {x, y})))
                  (config_rand BIT init qs))" 
                  unfolding Pbefore_in_def apply(simp add: map_pmf_def bind_return_pmf bind_assoc_pmf split_def)
                  apply(rule bind_pmf_cong)
                    apply(simp)
                    proof (goal_cases)
                      case (1 z)
                      let ?s = "fst z"
                      from 1 have u: "set (?s) = set init" using config_rand[of BIT, simplified] by metis
                      from 1 have v: "distinct (?s)" using dinit config_rand[of BIT, simplified] by metis
                      have "(x < y in ?s) = (x < y in Lxy (?s) {x, y})"
                        apply(rule Lxy_mono)
                          using u xyininit apply(simp)
                          using v by simp
                      then show ?case by simp
                    qed
     also have "… = map_pmf (λp. x < y in fst p) (config_rand BIT (Lxy init {x, y}) (Lxy qs {x, y}))"
        apply(subst strong) using assms by simp_all
     also have "… = Pbefore_in x y BIT (Lxy qs {x, y}) (Lxy init {x, y})" unfolding Pbefore_in_def by simp
     finally have "Pbefore_in x y BIT qs init =
        Pbefore_in x y BIT (Lxy qs {x, y}) (Lxy init {x, y})" .      
  
  } note fine=this

  with assms show ?thesis by simp
qed
        

theorem BIT_pairwise: "pairwise BIT"
apply(rule pairwise_property_lemma)
  apply(rule BIT_pairwise') 
    by(simp_all add: BIT_step_def)


end