[STATEMENT]
lemma proper_interval_integer_simps [code]:
  includes integer.lifting fixes x y :: integer and xo yo :: "integer option" shows
  "proper_interval (Some x) (Some y) = (1 < y - x)"
  "proper_interval None yo = True"
  "proper_interval xo None = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval (Some x) (Some y) = (1 < y - x) &&& proper_interval None yo = True &&& proper_interval xo None = True
[PROOF STEP]
by(transfer, simp)+


[STATEMENT]
lemma proper_interval_natural_simps [code]:
  includes natural.lifting fixes x y :: natural and xo :: "natural option" shows
  "proper_interval xo None = True"
  "proper_interval None (Some y) \<longleftrightarrow> y > 0"
  "proper_interval (Some x) (Some y) \<longleftrightarrow> y - x > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval xo None = True &&& proper_interval None (Some y) = (0 < y) &&& proper_interval (Some x) (Some y) = (1 < y - x)
[PROOF STEP]
by(transfer, simp)+


[STATEMENT]
lemma char_less_iff_nat_of_char: "x < y \<longleftrightarrow> of_char x < (of_char y :: nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y) = (of_char x < of_char y)
[PROOF STEP]
by (fact less_char_def)


[STATEMENT]
lemma nat_of_char_inject [simp]: "of_char x = (of_char y :: nat) \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_char x = of_char y) = (x = y)
[PROOF STEP]
by (fact of_char_eq_iff)


[STATEMENT]
lemma char_le_iff_nat_of_char: "x \<le> y \<longleftrightarrow> of_char x \<le> (of_char y :: nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> y) = (of_char x \<le> of_char y)
[PROOF STEP]
by (fact less_eq_char_def)


[STATEMENT]
lemma length_last_fusion_code [code]:
  "length_last_fusion g s =
  (if list.has_next g s then
     let (x, s') = list.next g s
     in fold_fusion g (\<lambda>x (n, _). (n + 1, x)) s' (1, x)
   else (0, undefined))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length_last_fusion g s = (if list.has_next g s then let (x, s') = list.next g s in fold_fusion g (\<lambda>x (n, uu_). (n + 1, x)) s' (1, x) else (0, undefined))
[PROOF STEP]
unfolding length_last_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length_last (list.unfoldr g s) = (if list.has_next g s then let (x, s') = list.next g s in fold_fusion g (\<lambda>x (n, uu_). (n + 1, x)) s' (1, x) else (0, undefined))
[PROOF STEP]
by(subst list.unfoldr.simps)(simp add: length_last_Nil length_last_Cons_code fold_fusion_def split_beta)


[STATEMENT]
lemma set_less_eq_aux_Compl_fusion_code:
  "set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 \<longleftrightarrow>
   (list.has_next g1 s1 \<longrightarrow> list.has_next g2 s2 \<longrightarrow>
    (let (x, s1') = list.next g1 s1;
         (y, s2') = list.next g2 s2
     in if x < y then proper_interval ao (Some x) \<or> set_less_eq_aux_Compl_fusion g1 g2 (Some x) s1' s2
        else if y < x then proper_interval ao (Some y) \<or> set_less_eq_aux_Compl_fusion g1 g2 (Some y) s1 s2'
        else proper_interval ao (Some y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 = (list.has_next g1 s1 \<longrightarrow> list.has_next g2 s2 \<longrightarrow> (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \<or> set_less_eq_aux_Compl_fusion g1 g2 (Some x) s1' s2 else if y < x then proper_interval ao (Some y) \<or> set_less_eq_aux_Compl_fusion g1 g2 (Some y) s1 s2' else proper_interval ao (Some y)))
[PROOF STEP]
unfolding set_less_eq_aux_Compl_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_eq_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2) = (list.has_next g1 s1 \<longrightarrow> list.has_next g2 s2 \<longrightarrow> (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \<or> set_less_eq_aux_Compl (Some x) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if y < x then proper_interval ao (Some y) \<or> set_less_eq_aux_Compl (Some y) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else proper_interval ao (Some y)))
[PROOF STEP]
by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma Compl_set_less_eq_aux_fusion_code:
  "Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 \<longleftrightarrow>
  (if list.has_next g1 s1 then
     let (x, s1') = list.next g1 s1
     in if list.has_next g2 s2 then
          let (y, s2') = list.next g2 s2
          in if x < y then \<not> proper_interval ao (Some x) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2
             else if y < x then \<not> proper_interval ao (Some y) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2'
             else \<not> proper_interval ao (Some y)
        else \<not> proper_interval ao (Some x) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2
   else if list.has_next g2 s2 then
     let (y, s2') = list.next g2 s2
     in \<not> proper_interval ao (Some y) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2'
   else \<not> proper_interval ao None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then \<not> proper_interval ao (Some x) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2 else if y < x then \<not> proper_interval ao (Some y) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2' else \<not> proper_interval ao (Some y) else \<not> proper_interval ao (Some x) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2 else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in \<not> proper_interval ao (Some y) \<and> Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2' else \<not> proper_interval ao None)
[PROOF STEP]
unfolding Compl_set_less_eq_aux_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_eq_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2) = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then \<not> proper_interval ao (Some x) \<and> Compl_set_less_eq_aux (Some x) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if y < x then \<not> proper_interval ao (Some y) \<and> Compl_set_less_eq_aux (Some y) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else \<not> proper_interval ao (Some y) else \<not> proper_interval ao (Some x) \<and> Compl_set_less_eq_aux (Some x) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in \<not> proper_interval ao (Some y) \<and> Compl_set_less_eq_aux (Some y) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else \<not> proper_interval ao None)
[PROOF STEP]
by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma set_less_aux_Compl_fusion_code:
  "set_less_aux_Compl_fusion g1 g2 ao s1 s2 \<longleftrightarrow>
  (if list.has_next g1 s1 then
     let (x, s1') = list.next g1 s1
     in if list.has_next g2 s2 then
          let (y, s2') = list.next g2 s2
          in if x < y then proper_interval ao (Some x) \<or> set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2
             else if y < x then proper_interval ao (Some y) \<or> set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2'
             else proper_interval ao (Some y)
        else proper_interval ao (Some x) \<or> set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2
   else if list.has_next g2 s2 then
     let (y, s2') = list.next g2 s2
     in proper_interval ao (Some y) \<or> set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2'
   else proper_interval ao None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_aux_Compl_fusion g1 g2 ao s1 s2 = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \<or> set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2 else if y < x then proper_interval ao (Some y) \<or> set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2' else proper_interval ao (Some y) else proper_interval ao (Some x) \<or> set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2 else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in proper_interval ao (Some y) \<or> set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2' else proper_interval ao None)
[PROOF STEP]
unfolding set_less_aux_Compl_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2) = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \<or> set_less_aux_Compl (Some x) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if y < x then proper_interval ao (Some y) \<or> set_less_aux_Compl (Some y) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else proper_interval ao (Some y) else proper_interval ao (Some x) \<or> set_less_aux_Compl (Some x) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in proper_interval ao (Some y) \<or> set_less_aux_Compl (Some y) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else proper_interval ao None)
[PROOF STEP]
by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma Compl_set_less_aux_fusion_code:
  "Compl_set_less_aux_fusion g1 g2 ao s1 s2 \<longleftrightarrow>
   list.has_next g1 s1 \<and> list.has_next g2 s2 \<and>
  (let (x, s1') = list.next g1 s1;
       (y, s2') = list.next g2 s2
   in if x < y then \<not> proper_interval ao (Some x) \<and> Compl_set_less_aux_fusion g1 g2 (Some x) s1' s2
      else if y < x then \<not> proper_interval ao (Some y) \<and> Compl_set_less_aux_fusion g1 g2 (Some y) s1 s2'
      else \<not> proper_interval ao (Some y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_aux_fusion g1 g2 ao s1 s2 = (list.has_next g1 s1 \<and> list.has_next g2 s2 \<and> (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then \<not> proper_interval ao (Some x) \<and> Compl_set_less_aux_fusion g1 g2 (Some x) s1' s2 else if y < x then \<not> proper_interval ao (Some y) \<and> Compl_set_less_aux_fusion g1 g2 (Some y) s1 s2' else \<not> proper_interval ao (Some y)))
[PROOF STEP]
unfolding Compl_set_less_aux_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2) = (list.has_next g1 s1 \<and> list.has_next g2 s2 \<and> (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then \<not> proper_interval ao (Some x) \<and> Compl_set_less_aux (Some x) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if y < x then \<not> proper_interval ao (Some y) \<and> Compl_set_less_aux (Some y) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else \<not> proper_interval ao (Some y)))
[PROOF STEP]
by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma exhaustive_above_fusion_code:
  "exhaustive_above_fusion g y s \<longleftrightarrow>
  (if list.has_next g s then
     let (x, s') = list.next g s
     in \<not> proper_interval (Some y) (Some x) \<and> exhaustive_above_fusion g x s'
   else \<not> proper_interval (Some y) None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustive_above_fusion g y s = (if list.has_next g s then let (x, s') = list.next g s in \<not> proper_interval (Some y) (Some x) \<and> exhaustive_above_fusion g x s' else \<not> proper_interval (Some y) None)
[PROOF STEP]
unfolding exhaustive_above_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustive_above y (list.unfoldr g s) = (if list.has_next g s then let (x, s') = list.next g s in \<not> proper_interval (Some y) (Some x) \<and> exhaustive_above x (list.unfoldr g s') else \<not> proper_interval (Some y) None)
[PROOF STEP]
by(subst list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma exhaustive_fusion_code:
  "exhaustive_fusion g s =
  (list.has_next g s \<and>
   (let (x, s') = list.next g s
    in \<not> proper_interval None (Some x) \<and> exhaustive_above_fusion g x s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustive_fusion g s = (list.has_next g s \<and> (let (x, s') = list.next g s in \<not> proper_interval None (Some x) \<and> exhaustive_above_fusion g x s'))
[PROOF STEP]
unfolding exhaustive_fusion_def exhaustive_above_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustive (list.unfoldr g s) = (list.has_next g s \<and> (let (x, s') = list.next g s in \<not> proper_interval None (Some x) \<and> exhaustive_above x (list.unfoldr g s')))
[PROOF STEP]
by(subst (1) list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma proper_interval_set_aux_fusion_code:
  "proper_interval_set_aux_fusion g1 g2 s1 s2 \<longleftrightarrow>
   list.has_next g2 s2 \<and>
  (let (y, s2') = list.next g2 s2
   in if list.has_next g1 s1 then
        let (x, s1') = list.next g1 s1
        in if x < y then False
           else if y < x then proper_interval (Some y) (Some x) \<or> list.has_next g2 s2' \<or> \<not> exhaustive_above_fusion g1 x s1'
           else proper_interval_set_aux_fusion g1 g2 s1' s2'
      else list.has_next g2 s2' \<or> proper_interval (Some y) None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_aux_fusion g1 g2 s1 s2 = (list.has_next g2 s2 \<and> (let (y, s2') = list.next g2 s2 in if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if x < y then False else if y < x then proper_interval (Some y) (Some x) \<or> list.has_next g2 s2' \<or> \<not> exhaustive_above_fusion g1 x s1' else proper_interval_set_aux_fusion g1 g2 s1' s2' else list.has_next g2 s2' \<or> proper_interval (Some y) None))
[PROOF STEP]
unfolding proper_interval_set_aux_fusion_def exhaustive_above_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_aux (list.unfoldr g1 s1) (list.unfoldr g2 s2) = (list.has_next g2 s2 \<and> (let (y, s2') = list.next g2 s2 in if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if x < y then False else if y < x then proper_interval (Some y) (Some x) \<or> list.has_next g2 s2' \<or> \<not> exhaustive_above x (list.unfoldr g1 s1') else proper_interval_set_aux (list.unfoldr g1 s1') (list.unfoldr g2 s2') else list.has_next g2 s2' \<or> proper_interval (Some y) None))
[PROOF STEP]
by(subst (1 2) list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma proper_interval_set_Compl_aux_fusion_code:
  "proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 \<longleftrightarrow>
  (if list.has_next g1 s1 then
     let (x, s1') = list.next g1 s1
     in if list.has_next g2 s2 then
          let (y, s2') = list.next g2 s2
          in if x < y then
               proper_interval ao (Some x) \<or>
               proper_interval_set_Compl_aux_fusion g1 g2 (Some x) (n + 1) s1' s2
             else if y < x then
               proper_interval ao (Some y) \<or>
               proper_interval_set_Compl_aux_fusion g1 g2 (Some y) (n + 1) s1 s2'
             else
               proper_interval ao (Some x) \<and>
               (let m = CARD('a) - n
                in m - length_fusion g2 s2' \<noteq> 2 \<or> m - length_fusion g1 s1' \<noteq> 2)
        else
          let m = CARD('a) - n; (len_x, x') = length_last_fusion g1 s1
          in m \<noteq> len_x \<and> (m = len_x + 1 \<longrightarrow> \<not> proper_interval (Some x') None)

   else if list.has_next g2 s2 then
     let (y, s2') = list.next g2 s2;
         m = CARD('a) - n;
         (len_y, y') = length_last_fusion g2 s2
     in m \<noteq> len_y \<and> (m = len_y + 1 \<longrightarrow> \<not> proper_interval (Some y') None)
   else CARD('a) > n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \<or> proper_interval_set_Compl_aux_fusion g1 g2 (Some x) (n + 1) s1' s2 else if y < x then proper_interval ao (Some y) \<or> proper_interval_set_Compl_aux_fusion g1 g2 (Some y) (n + 1) s1 s2' else proper_interval ao (Some x) \<and> (let m = CARD('a) - n in m - length_fusion g2 s2' \<noteq> 2 \<or> m - length_fusion g1 s1' \<noteq> 2) else let m = CARD('a) - n; (len_x, x') = length_last_fusion g1 s1 in m \<noteq> len_x \<and> (m = len_x + 1 \<longrightarrow> \<not> proper_interval (Some x') None) else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2; m = CARD('a) - n; (len_y, y') = length_last_fusion g2 s2 in m \<noteq> len_y \<and> (m = len_y + 1 \<longrightarrow> \<not> proper_interval (Some y') None) else n + 1 < CARD('a))
[PROOF STEP]
unfolding proper_interval_set_Compl_aux_fusion_def length_last_fusion_def length_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_Compl_aux ao n (list.unfoldr g1 s1) (list.unfoldr g2 s2) = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \<or> proper_interval_set_Compl_aux (Some x) (n + 1) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if y < x then proper_interval ao (Some y) \<or> proper_interval_set_Compl_aux (Some y) (n + 1) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else proper_interval ao (Some x) \<and> (let m = CARD('a) - n in m - length (list.unfoldr g2 s2') \<noteq> 2 \<or> m - length (list.unfoldr g1 s1') \<noteq> 2) else let m = CARD('a) - n; (len_x, x') = length_last (list.unfoldr g1 s1) in m \<noteq> len_x \<and> (m = len_x + 1 \<longrightarrow> \<not> proper_interval (Some x') None) else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2; m = CARD('a) - n; (len_y, y') = length_last (list.unfoldr g2 s2) in m \<noteq> len_y \<and> (m = len_y + 1 \<longrightarrow> \<not> proper_interval (Some y') None) else n + 1 < CARD('a))
[PROOF STEP]
by(subst (1 2 4 5 9 10) list.unfoldr.simps)(simp add: split_beta)


[STATEMENT]
lemma proper_interval_Compl_set_aux_fusion_code:
  "proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 \<longleftrightarrow>
   list.has_next g1 s1 \<and> list.has_next g2 s2 \<and>
   (let (x, s1') = list.next g1 s1;
        (y, s2') = list.next g2 s2
    in if x < y then
         \<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux_fusion g1 g2 (Some x) s1' s2
       else if y < x then
         \<not> proper_interval ao (Some y) \<and> proper_interval_Compl_set_aux_fusion g1 g2 (Some y) s1 s2'
       else \<not> proper_interval ao (Some x) \<and> (list.has_next g2 s2' \<or> list.has_next g1 s1'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 = (list.has_next g1 s1 \<and> list.has_next g2 s2 \<and> (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then \<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux_fusion g1 g2 (Some x) s1' s2 else if y < x then \<not> proper_interval ao (Some y) \<and> proper_interval_Compl_set_aux_fusion g1 g2 (Some y) s1 s2' else \<not> proper_interval ao (Some x) \<and> (list.has_next g2 s2' \<or> list.has_next g1 s1')))
[PROOF STEP]
unfolding proper_interval_Compl_set_aux_fusion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2) = (list.has_next g1 s1 \<and> list.has_next g2 s2 \<and> (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then \<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) (list.unfoldr g1 s1') (list.unfoldr g2 s2) else if y < x then \<not> proper_interval ao (Some y) \<and> proper_interval_Compl_set_aux (Some y) (list.unfoldr g1 s1) (list.unfoldr g2 s2') else \<not> proper_interval ao (Some x) \<and> (list.has_next g2 s2' \<or> list.has_next g1 s1')))
[PROOF STEP]
by(subst (1 2 4 5) list.unfoldr.simps)(auto simp add: split_beta)


[STATEMENT]
lemma is_factorization_of_factor_complex_main:
  assumes "factor_complex_main p = fctrs"
  shows   "is_factorization_of fctrs p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_factorization_of fctrs p
[PROOF STEP]
unfolding is_factorization_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interp_factorization fctrs = p \<and> distinct (map fst (snd fctrs))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. interp_factorization fctrs = p
 2. distinct (map fst (snd fctrs))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
factor_complex_main p = fctrs
[PROOF STEP]
have "p = Polynomial.smult (fst fctrs) (\<Prod>(x, i)\<leftarrow>snd fctrs. [:- x, 1:] ^ Suc i)"
[PROOF STATE]
proof (prove)
using this:
factor_complex_main p = fctrs

goal (1 subgoal):
 1. p = smult (fst fctrs) (\<Prod>(x, i)\<leftarrow>snd fctrs. [:- x, 1:] ^ Suc i)
[PROOF STEP]
by (intro factor_complex_main) simp_all
[PROOF STATE]
proof (state)
this:
p = smult (fst fctrs) (\<Prod>(x, i)\<leftarrow>snd fctrs. [:- x, 1:] ^ Suc i)

goal (2 subgoals):
 1. interp_factorization fctrs = p
 2. distinct (map fst (snd fctrs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p = smult (fst fctrs) (\<Prod>(x, i)\<leftarrow>snd fctrs. [:- x, 1:] ^ Suc i)

goal (2 subgoals):
 1. interp_factorization fctrs = p
 2. distinct (map fst (snd fctrs))
[PROOF STEP]
have "\<dots> = interp_factorization fctrs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smult (fst fctrs) (\<Prod>(x, i)\<leftarrow>snd fctrs. [:- x, 1:] ^ Suc i) = interp_factorization fctrs
[PROOF STEP]
by (simp add: interp_factorization_def case_prod_unfold)
[PROOF STATE]
proof (state)
this:
smult (fst fctrs) (\<Prod>(x, i)\<leftarrow>snd fctrs. [:- x, 1:] ^ Suc i) = interp_factorization fctrs

goal (2 subgoals):
 1. interp_factorization fctrs = p
 2. distinct (map fst (snd fctrs))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p = interp_factorization fctrs
[PROOF STEP]
show "interp_factorization fctrs = p"
[PROOF STATE]
proof (prove)
using this:
p = interp_factorization fctrs

goal (1 subgoal):
 1. interp_factorization fctrs = p
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
interp_factorization fctrs = p

goal (1 subgoal):
 1. distinct (map fst (snd fctrs))
[PROOF STEP]
show "distinct (map fst (snd fctrs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (snd fctrs))
[PROOF STEP]
unfolding assms[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (snd (factor_complex_main p)))
[PROOF STEP]
by (rule distinct_factor_complex_main)
[PROOF STATE]
proof (state)
this:
distinct (map fst (snd fctrs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solve_ratfps:
  assumes "solve_ratfps f = sol"
  shows   "Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
define p and q where "p = fst (quot_of_ratfps f)" and "q = snd (quot_of_ratfps f)"
[PROOF STATE]
proof (state)
this:
p = fst (quot_of_ratfps f)
q = snd (quot_of_ratfps f)

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
solve_ratfps f = sol
p = fst (quot_of_ratfps f)
q = snd (quot_of_ratfps f)
[PROOF STEP]
obtain fctrs where fctrs: "factor_complex_main (reflect_poly q) = fctrs"
[PROOF STATE]
proof (prove)
using this:
solve_ratfps f = sol
p = fst (quot_of_ratfps f)
q = snd (quot_of_ratfps f)

goal (1 subgoal):
 1. (\<And>fctrs. factor_complex_main (reflect_poly q) = fctrs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: solve_ratfps_def p_def q_def case_prod_unfold split: if_splits)
[PROOF STATE]
proof (state)
this:
factor_complex_main (reflect_poly q) = fctrs

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
have q: "coeff q 0 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_term q \<noteq> 0
[PROOF STEP]
by (simp add: q_def)
[PROOF STATE]
proof (state)
this:
constant_term q \<noteq> 0

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
hence [simp]: "q \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
constant_term q \<noteq> 0

goal (1 subgoal):
 1. q \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<noteq> 0

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
from fctrs
[PROOF STATE]
proof (chain)
picking this:
factor_complex_main (reflect_poly q) = fctrs
[PROOF STEP]
have "is_factorization_of fctrs (reflect_poly q)"
[PROOF STATE]
proof (prove)
using this:
factor_complex_main (reflect_poly q) = fctrs

goal (1 subgoal):
 1. is_factorization_of fctrs (reflect_poly q)
[PROOF STEP]
by (rule is_factorization_of_factor_complex_main)
[PROOF STATE]
proof (state)
this:
is_factorization_of fctrs (reflect_poly q)

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
solve_ratfps f = sol
is_factorization_of fctrs (reflect_poly q)
[PROOF STEP]
have "is_alt_factorization_of fctrs (reflect_poly (reflect_poly q))"
[PROOF STATE]
proof (prove)
using this:
solve_ratfps f = sol
is_factorization_of fctrs (reflect_poly q)

goal (1 subgoal):
 1. is_alt_factorization_of fctrs (reflect_poly (reflect_poly q))
[PROOF STEP]
by (intro reflect_factorization) simp_all
[PROOF STATE]
proof (state)
this:
is_alt_factorization_of fctrs (reflect_poly (reflect_poly q))

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
hence "is_alt_factorization_of fctrs q"
[PROOF STATE]
proof (prove)
using this:
is_alt_factorization_of fctrs (reflect_poly (reflect_poly q))

goal (1 subgoal):
 1. is_alt_factorization_of fctrs q
[PROOF STEP]
by (simp add: q)
[PROOF STATE]
proof (state)
this:
is_alt_factorization_of fctrs q

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
with fctrs q
[PROOF STATE]
proof (chain)
picking this:
factor_complex_main (reflect_poly q) = fctrs
constant_term q \<noteq> 0
is_alt_factorization_of fctrs q
[PROOF STEP]
have "Abs_fps (interp_ratfps_solution (solve_factored_ratfps' p fctrs)) =
            fps_of_poly p / fps_of_poly q"
[PROOF STATE]
proof (prove)
using this:
factor_complex_main (reflect_poly q) = fctrs
constant_term q \<noteq> 0
is_alt_factorization_of fctrs q

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution (solve_factored_ratfps' p fctrs)) = fps_of_poly p / fps_of_poly q
[PROOF STEP]
by (intro solve_factored_ratfps') (simp_all)
[PROOF STATE]
proof (state)
this:
Abs_fps (interp_ratfps_solution (solve_factored_ratfps' p fctrs)) = fps_of_poly p / fps_of_poly q

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_fps (interp_ratfps_solution (solve_factored_ratfps' p fctrs)) = fps_of_poly p / fps_of_poly q

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
from fctrs assms
[PROOF STATE]
proof (chain)
picking this:
factor_complex_main (reflect_poly q) = fctrs
solve_ratfps f = sol
[PROOF STEP]
have "solve_factored_ratfps' p fctrs = sol"
[PROOF STATE]
proof (prove)
using this:
factor_complex_main (reflect_poly q) = fctrs
solve_ratfps f = sol

goal (1 subgoal):
 1. solve_factored_ratfps' p fctrs = sol
[PROOF STEP]
by (simp add: solve_ratfps_def p_def q_def case_prod_unfold split: if_splits)
[PROOF STATE]
proof (state)
this:
solve_factored_ratfps' p fctrs = sol

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Abs_fps (interp_ratfps_solution sol) = fps_of_poly p / fps_of_poly q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Abs_fps (interp_ratfps_solution sol) = fps_of_poly p / fps_of_poly q

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f
[PROOF STEP]
by (simp add: fps_of_ratfps_altdef case_prod_unfold p_def q_def)
[PROOF STATE]
proof (state)
this:
Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solve_lhr:
  assumes "linear_homogenous_recurrence f cs fs"
  assumes "Some sol = solve_lhr cs fs"
  shows   "f = interp_ratfps_solution sol"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
obtain fctrs where
      fctrs: "factor_complex_main (lr_fps_denominator' cs) = fctrs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>fctrs. factor_complex_main (lr_fps_denominator' cs) = fctrs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
factor_complex_main (lr_fps_denominator' cs) = fctrs

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
from is_factorization_of_factor_complex_main[OF this]
[PROOF STATE]
proof (chain)
picking this:
is_factorization_of fctrs (lr_fps_denominator' cs)
[PROOF STEP]
have factorization: "is_factorization_of fctrs (lr_fps_denominator' cs)"
[PROOF STATE]
proof (prove)
using this:
is_factorization_of fctrs (lr_fps_denominator' cs)

goal (1 subgoal):
 1. is_factorization_of fctrs (lr_fps_denominator' cs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_factorization_of fctrs (lr_fps_denominator' cs)

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
have "f = interp_ratfps_solution (solve_factored_ratfps' (lhr_fps_numerator
              (length fs + 1 - length cs) cs ((!) fs)) fctrs)"
    (is "_ = interp_ratfps_solution ?sol")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = interp_ratfps_solution (solve_factored_ratfps' (lhr_fps_numerator (length fs + 1 - length cs) cs ((!) fs)) fctrs)
[PROOF STEP]
by (intro solve_lhr_aux) fact+
[PROOF STATE]
proof (state)
this:
f = interp_ratfps_solution (solve_factored_ratfps' (lhr_fps_numerator (length fs + 1 - length cs) cs ((!) fs)) fctrs)

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f = interp_ratfps_solution (solve_factored_ratfps' (lhr_fps_numerator (length fs + 1 - length cs) cs ((!) fs)) fctrs)

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
Some sol = solve_lhr cs fs
[PROOF STEP]
have "?sol = sol"
[PROOF STATE]
proof (prove)
using this:
Some sol = solve_lhr cs fs

goal (1 subgoal):
 1. solve_factored_ratfps' (lhr_fps_numerator (length fs + 1 - length cs) cs ((!) fs)) fctrs = sol
[PROOF STEP]
by (auto simp: solve_lhr_def Let_def case_prod_unfold fctrs split: if_splits)
[PROOF STATE]
proof (state)
this:
solve_factored_ratfps' (lhr_fps_numerator (length fs + 1 - length cs) cs ((!) fs)) fctrs = sol

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f = interp_ratfps_solution sol
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f = interp_ratfps_solution sol

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f = interp_ratfps_solution sol

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solve_lir:
  assumes "linear_inhomogenous_recurrence f (eval_polyexp g) cs fs"
  assumes "solve_lir cs fs g = Some sol"
  shows   "f = interp_ratfps_solution sol"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
from lir_fps_correct[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
map_option fps_of_ratfps (lir_fps cs fs g) = Some (Abs_fps f)
[PROOF STEP]
obtain fps
    where fps: "lir_fps cs fs g = Some fps" "fps_of_ratfps fps = Abs_fps f"
[PROOF STATE]
proof (prove)
using this:
map_option fps_of_ratfps (lir_fps cs fs g) = Some (Abs_fps f)

goal (1 subgoal):
 1. (\<And>fps. \<lbrakk>lir_fps cs fs g = Some fps; fps_of_ratfps fps = Abs_fps f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lir_fps cs fs g = Some fps
fps_of_ratfps fps = Abs_fps f

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
solve_lir cs fs g = Some sol
[PROOF STEP]
have "solve_ratfps fps = sol"
[PROOF STATE]
proof (prove)
using this:
solve_lir cs fs g = Some sol

goal (1 subgoal):
 1. solve_ratfps fps = sol
[PROOF STEP]
by (simp add: solve_lir_def fps case_prod_unfold)
[PROOF STATE]
proof (state)
this:
solve_ratfps fps = sol

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
from solve_ratfps[OF this]
[PROOF STATE]
proof (chain)
picking this:
Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps fps
[PROOF STEP]
have "Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps fps"
[PROOF STATE]
proof (prove)
using this:
Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps fps

goal (1 subgoal):
 1. Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps fps
[PROOF STEP]
by (simp add: case_prod_unfold fps_of_ratfps_altdef)
[PROOF STATE]
proof (state)
this:
Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps fps

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
with fps
[PROOF STATE]
proof (chain)
picking this:
lir_fps cs fs g = Some fps
fps_of_ratfps fps = Abs_fps f
Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps fps
[PROOF STEP]
have "Abs_fps f = Abs_fps (interp_ratfps_solution sol)"
[PROOF STATE]
proof (prove)
using this:
lir_fps cs fs g = Some fps
fps_of_ratfps fps = Abs_fps f
Abs_fps (interp_ratfps_solution sol) = fps_of_ratfps fps

goal (1 subgoal):
 1. Abs_fps f = Abs_fps (interp_ratfps_solution sol)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Abs_fps f = Abs_fps (interp_ratfps_solution sol)

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Abs_fps f = Abs_fps (interp_ratfps_solution sol)

goal (1 subgoal):
 1. f = interp_ratfps_solution sol
[PROOF STEP]
by (simp add: fun_eq_iff fps_eq_iff)
[PROOF STATE]
proof (state)
this:
f = interp_ratfps_solution sol

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comPurge_simps:
  "comPurge ca = comSendServerReq uID p aID reqInfo \<longleftrightarrow> (\<exists>p'. ca = comSendServerReq uID p' aID reqInfo \<and> p = emptyPass)"
  "comPurge ca = comReceiveClientReq aID reqInfo \<longleftrightarrow> ca = comReceiveClientReq aID reqInfo"
  "comPurge ca = comConnectClient uID p aID sp \<longleftrightarrow> (\<exists>p'. ca = comConnectClient uID p' aID sp \<and> p = emptyPass)"
  "comPurge ca = comConnectServer aID sp \<longleftrightarrow> ca = comConnectServer aID sp"
  "comPurge ca = comReceivePost aID sp nID nt uID v \<longleftrightarrow> ca = comReceivePost aID sp nID nt uID v"
  "comPurge ca = comSendPost uID p aID nID \<longleftrightarrow> (\<exists>p'. ca = comSendPost uID p' aID nID \<and> p = emptyPass)"
  "comPurge ca = comSendCreateOFriend uID p aID uID' \<longleftrightarrow> (\<exists>p'. ca = comSendCreateOFriend uID p' aID uID' \<and> p = emptyPass)"
  "comPurge ca = comReceiveCreateOFriend aID cp uID uID'
\<longleftrightarrow> (\<exists>uid''. (ca = comReceiveCreateOFriend aID cp uID uid'' \<or> ca = comReceiveDeleteOFriend aID cp uID uid'') \<and> aID = AID \<and> uID = UID \<and> uid'' \<notin> UIDs AID' \<and> uID' = emptyUserID)
    \<or> (ca = comReceiveCreateOFriend aID cp uID uID' \<and> \<not>(aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID'))"
  "comPurge ca = comSendDeleteOFriend uID p aID uID' \<longleftrightarrow> (\<exists>p'. ca = comSendDeleteOFriend uID p' aID uID' \<and> p = emptyPass)"
  "comPurge ca = comReceiveDeleteOFriend aID cp uID uID' \<longleftrightarrow> ca = comReceiveDeleteOFriend aID cp uID uID' \<and> \<not>(aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((comPurge ca = comSendServerReq uID p aID reqInfo) = (\<exists>p'. ca = comSendServerReq uID p' aID reqInfo \<and> p = emptyPass) &&& (comPurge ca = comReceiveClientReq aID reqInfo) = (ca = comReceiveClientReq aID reqInfo)) &&& (comPurge ca = comConnectClient uID p aID sp) = (\<exists>p'. ca = comConnectClient uID p' aID sp \<and> p = emptyPass) &&& (comPurge ca = comConnectServer aID sp) = (ca = comConnectServer aID sp) &&& (comPurge ca = comReceivePost aID sp nID nt uID v) = (ca = comReceivePost aID sp nID nt uID v)) &&& ((comPurge ca = comSendPost uID p aID nID) = (\<exists>p'. ca = comSendPost uID p' aID nID \<and> p = emptyPass) &&& (comPurge ca = comSendCreateOFriend uID p aID uID') = (\<exists>p'. ca = comSendCreateOFriend uID p' aID uID' \<and> p = emptyPass)) &&& (comPurge ca = comReceiveCreateOFriend aID cp uID uID') = ((\<exists>uid''. (ca = comReceiveCreateOFriend aID cp uID uid'' \<or> ca = comReceiveDeleteOFriend aID cp uID uid'') \<and> aID = AID \<and> uID = UID \<and> uid'' \<notin> UIDs AID' \<and> uID' = emptyUserID) \<or> ca = comReceiveCreateOFriend aID cp uID uID' \<and> \<not> (aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID')) &&& (comPurge ca = comSendDeleteOFriend uID p aID uID') = (\<exists>p'. ca = comSendDeleteOFriend uID p' aID uID' \<and> p = emptyPass) &&& (comPurge ca = comReceiveDeleteOFriend aID cp uID uID') = (ca = comReceiveDeleteOFriend aID cp uID uID' \<and> \<not> (aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID'))
[PROOF STEP]
by (cases ca; auto)+


[STATEMENT]
lemma g_simps:
  "g (Trans s a ou s') = (COMact (comSendServerReq uID p aID reqInfo), ou')
\<longleftrightarrow> (\<exists>p'. a = COMact (comSendServerReq uID p' aID reqInfo) \<and> p = emptyPass \<and> ou = ou')"
  "g (Trans s a ou s') = (COMact (comReceiveClientReq aID reqInfo), ou')
\<longleftrightarrow> a = COMact (comReceiveClientReq aID reqInfo) \<and> ou = ou'"
  "g (Trans s a ou s') = (COMact (comConnectClient uID p aID sp), ou')
\<longleftrightarrow> (\<exists>p'. a = COMact (comConnectClient uID p' aID sp) \<and> p = emptyPass \<and> ou = ou')"
  "g (Trans s a ou s') = (COMact (comConnectServer aID sp), ou')
\<longleftrightarrow> a = COMact (comConnectServer aID sp) \<and> ou = ou'"
  "g (Trans s a ou s') = (COMact (comReceivePost aID sp nID nt uID v), ou')
\<longleftrightarrow> a = COMact (comReceivePost aID sp nID nt uID v) \<and> ou = ou'"
  "g (Trans s a ou s') = (COMact (comSendPost uID p aID nID), ou')
\<longleftrightarrow> (\<exists>p'. a = COMact (comSendPost uID p' aID nID) \<and> p = emptyPass \<and> ou = ou')"
  "g (Trans s a ou s') = (COMact (comSendCreateOFriend uID p aID uID'), ou')
\<longleftrightarrow> (\<exists>p'. a = COMact (comSendCreateOFriend uID p' aID uID') \<and> p = emptyPass \<and> ou = ou')"
  "g (Trans s a ou s') = (COMact (comReceiveCreateOFriend aID cp uID uID'), ou')
\<longleftrightarrow> (((\<exists>uid''. (a = COMact (comReceiveCreateOFriend aID cp uID uid'') \<or> a = COMact (comReceiveDeleteOFriend aID cp uID uid'')) \<and> aID = AID \<and> uID = UID \<and> uid'' \<notin> UIDs AID' \<and> uID' = emptyUserID)
    \<or> (a = COMact (comReceiveCreateOFriend aID cp uID uID') \<and> \<not>(aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID')))
    \<and> ou = ou')"
  "g (Trans s a ou s') = (COMact (comSendDeleteOFriend uID p aID uID'), ou')
\<longleftrightarrow> (\<exists>p'. a = COMact (comSendDeleteOFriend uID p' aID uID') \<and> p = emptyPass \<and> ou = ou')"
  "g (Trans s a ou s') = (COMact (comReceiveDeleteOFriend aID cp uID uID'), ou')
\<longleftrightarrow> a = COMact (comReceiveDeleteOFriend aID cp uID uID') \<and> \<not>(aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID') \<and> ou = ou'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((g (Trans s a ou s') = (COMact (comSendServerReq uID p aID reqInfo), ou')) = (\<exists>p'. a = COMact (comSendServerReq uID p' aID reqInfo) \<and> p = emptyPass \<and> ou = ou') &&& (g (Trans s a ou s') = (COMact (comReceiveClientReq aID reqInfo), ou')) = (a = COMact (comReceiveClientReq aID reqInfo) \<and> ou = ou')) &&& (g (Trans s a ou s') = (COMact (comConnectClient uID p aID sp), ou')) = (\<exists>p'. a = COMact (comConnectClient uID p' aID sp) \<and> p = emptyPass \<and> ou = ou') &&& (g (Trans s a ou s') = (COMact (comConnectServer aID sp), ou')) = (a = COMact (comConnectServer aID sp) \<and> ou = ou') &&& (g (Trans s a ou s') = (COMact (comReceivePost aID sp nID nt uID v), ou')) = (a = COMact (comReceivePost aID sp nID nt uID v) \<and> ou = ou')) &&& ((g (Trans s a ou s') = (COMact (comSendPost uID p aID nID), ou')) = (\<exists>p'. a = COMact (comSendPost uID p' aID nID) \<and> p = emptyPass \<and> ou = ou') &&& (g (Trans s a ou s') = (COMact (comSendCreateOFriend uID p aID uID'), ou')) = (\<exists>p'. a = COMact (comSendCreateOFriend uID p' aID uID') \<and> p = emptyPass \<and> ou = ou')) &&& (g (Trans s a ou s') = (COMact (comReceiveCreateOFriend aID cp uID uID'), ou')) = (((\<exists>uid''. (a = COMact (comReceiveCreateOFriend aID cp uID uid'') \<or> a = COMact (comReceiveDeleteOFriend aID cp uID uid'')) \<and> aID = AID \<and> uID = UID \<and> uid'' \<notin> UIDs AID' \<and> uID' = emptyUserID) \<or> a = COMact (comReceiveCreateOFriend aID cp uID uID') \<and> \<not> (aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID')) \<and> ou = ou') &&& (g (Trans s a ou s') = (COMact (comSendDeleteOFriend uID p aID uID'), ou')) = (\<exists>p'. a = COMact (comSendDeleteOFriend uID p' aID uID') \<and> p = emptyPass \<and> ou = ou') &&& (g (Trans s a ou s') = (COMact (comReceiveDeleteOFriend aID cp uID uID'), ou')) = (a = COMact (comReceiveDeleteOFriend aID cp uID uID') \<and> \<not> (aID = AID \<and> uID = UID \<and> uID' \<notin> UIDs AID') \<and> ou = ou')
[PROOF STEP]
by (cases a; auto simp: comPurge_simps)+


[STATEMENT]
lemma pi_lmi[proper_it]:
  "proper_it' foldli foldli"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' foldli foldli
[PROOF STEP]
by (intro proper_it'I icf_proper_iteratorI)


[STATEMENT]
lemma lmi_from_list_dj_correct:
  assumes [simp]: "distinct (map fst l)"
  shows "lmi.\<alpha> (lmi_from_list_dj l) = map_of l"
        "lmi.invar (lmi_from_list_dj l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmi.\<alpha> (lmi_from_list_dj l) = map_of l &&& lmi.invar (lmi_from_list_dj l)
[PROOF STEP]
by (auto simp add: lmi_from_list_dj_def icf_rec_unf lmi_\<alpha>_def lmi_invar_def)


[STATEMENT]
lemma N_gt0[simp, intro!]: "0<N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < N
[PROOF STEP]
by (cases N) auto


[STATEMENT]
lemma never_blocked: "A.can_step l s \<longleftrightarrow> l<N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.can_step l s = (l < N)
[PROOF STEP]
apply (cases s; cases "tts s l"; simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>s = (a, b, c); c l = INIT\<rbrakk> \<Longrightarrow> A.can_step l (a, b, c) = (l < N)
 2. \<And>a b c x2. \<lbrakk>s = (a, b, c); c l = WAIT x2\<rbrakk> \<Longrightarrow> A.can_step l (a, b, c) = (l < N)
 3. \<And>a b c x3. \<lbrakk>s = (a, b, c); c l = HOLD x3\<rbrakk> \<Longrightarrow> A.can_step l (a, b, c) = (l < N)
 4. \<And>a b c x4. \<lbrakk>s = (a, b, c); c l = REL x4\<rbrakk> \<Longrightarrow> A.can_step l (a, b, c) = (l < N)
[PROOF STEP]
unfolding A.can_step_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>s = (a, b, c); c l = INIT\<rbrakk> \<Longrightarrow> (\<exists>s'. alstep l (a, b, c) s') = (l < N)
 2. \<And>a b c x2. \<lbrakk>s = (a, b, c); c l = WAIT x2\<rbrakk> \<Longrightarrow> (\<exists>s'. alstep l (a, b, c) s') = (l < N)
 3. \<And>a b c x3. \<lbrakk>s = (a, b, c); c l = HOLD x3\<rbrakk> \<Longrightarrow> (\<exists>s'. alstep l (a, b, c) s') = (l < N)
 4. \<And>a b c x4. \<lbrakk>s = (a, b, c); c l = REL x4\<rbrakk> \<Longrightarrow> (\<exists>s'. alstep l (a, b, c) s') = (l < N)
[PROOF STEP]
apply (clarsimp simp: alstep.simps astep_sng.simps; blast)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma has_ticket_simps[simp]:
    "\<not>has_ticket INIT k"
    "has_ticket (WAIT k) k'\<longleftrightarrow> k'=k"
    "has_ticket (HOLD k) k'\<longleftrightarrow> k'=k"
    "has_ticket (REL k) k'\<longleftrightarrow> k'=k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> has_ticket INIT k &&& has_ticket (WAIT k) k' = (k' = k)) &&& has_ticket (HOLD k) k' = (k' = k) &&& has_ticket (REL k) k' = (k' = k)
[PROOF STEP]
unfolding has_ticket_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (INIT = WAIT k \<or> INIT = HOLD k \<or> INIT = REL k) &&& (WAIT k = WAIT k' \<or> WAIT k = HOLD k' \<or> WAIT k = REL k') = (k' = k)) &&& (HOLD k = WAIT k' \<or> HOLD k = HOLD k' \<or> HOLD k = REL k') = (k' = k) &&& (REL k = WAIT k' \<or> REL k = HOLD k' \<or> REL k = REL k') = (k' = k)
[PROOF STEP]
by auto


[STATEMENT]
lemma locks_ticket_simps[simp]:
    "\<not>locks_ticket INIT k"
    "\<not>locks_ticket (WAIT k) k'"
    "locks_ticket (HOLD k) k'\<longleftrightarrow> k'=k"
    "locks_ticket (REL k) k'\<longleftrightarrow> k'=k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> locks_ticket INIT k &&& \<not> locks_ticket (WAIT k) k') &&& locks_ticket (HOLD k) k' = (k' = k) &&& locks_ticket (REL k) k' = (k' = k)
[PROOF STEP]
unfolding locks_ticket_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (INIT = HOLD k \<or> INIT = REL k) &&& \<not> (WAIT k = HOLD k' \<or> WAIT k = REL k')) &&& (HOLD k = HOLD k' \<or> HOLD k = REL k') = (k' = k) &&& (REL k = HOLD k' \<or> REL k = REL k') = (k' = k)
[PROOF STEP]
by auto


[STATEMENT]
lemma holds_imp_uses: "locks_ticket s k \<Longrightarrow> has_ticket s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locks_ticket s k \<Longrightarrow> has_ticket s k
[PROOF STEP]
unfolding locks_ticket_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = HOLD k \<or> s = REL k \<Longrightarrow> has_ticket s k
[PROOF STEP]
by auto


[STATEMENT]
lemma is_invar1: "A.is_invar invar1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.is_invar invar1
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invar1 as\<^sub>0
 2. \<And>s s'. \<lbrakk>A.reachable s; invar1 s; A.step s s'\<rbrakk> \<Longrightarrow> invar1 s'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar1 as\<^sub>0
[PROOF STEP]
by (auto simp: invar1_def as\<^sub>0_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>A.reachable s; invar1 s; A.step s s'\<rbrakk> \<Longrightarrow> invar1 s'
[PROOF STEP]
subgoal for s s'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable s; invar1 s; A.step s s'\<rbrakk> \<Longrightarrow> invar1 s'
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>A.reachable s; invar1 s; alstep l s s'\<rbrakk> \<Longrightarrow> invar1 s'
[PROOF STEP]
apply (erule alstep.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l c n ts c' n' s'a. \<lbrakk>A.reachable s; invar1 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; astep_sng (c, n, ts l) (c', n', s'a)\<rbrakk> \<Longrightarrow> invar1 s'
[PROOF STEP]
apply (erule astep_sng.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>l c n ts c' n' s'a ca na. \<lbrakk>A.reachable s; invar1 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, INIT); (c', n', s'a) = (ca, na + 1, WAIT na)\<rbrakk> \<Longrightarrow> invar1 s'
 2. \<And>l c n ts c' n' s'a ca k na. \<lbrakk>A.reachable s; invar1 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT k); (c', n', s'a) = (ca, na, WAIT k); ca \<noteq> k\<rbrakk> \<Longrightarrow> invar1 s'
 3. \<And>l c n ts c' n' s'a ca na. \<lbrakk>A.reachable s; invar1 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, WAIT ca); (c', n', s'a) = (ca, na, HOLD ca)\<rbrakk> \<Longrightarrow> invar1 s'
 4. \<And>l c n ts c' n' s'a ca na k. \<lbrakk>A.reachable s; invar1 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, HOLD k); (c', n', s'a) = (ca, na, REL k)\<rbrakk> \<Longrightarrow> invar1 s'
 5. \<And>l c n ts c' n' s'a ca na k. \<lbrakk>A.reachable s; invar1 s; s = (c, n, ts); s' = (c', n', ts(l := s'a)); l < N; (c, n, ts l) = (ca, na, REL k); (c', n', s'a) = (k + 1, na, INIT)\<rbrakk> \<Longrightarrow> invar1 s'
[PROOF STEP]
apply (clarsimp_all simp: invar1_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>l c n ts t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, Suc n, ts(l := WAIT n)); l < N; ts l = INIT; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> n \<noteq> k'))) \<and> (t \<noteq> l \<longrightarrow> (\<forall>k. t < N \<and> has_ticket (ts t) k \<longrightarrow> k < Suc n \<and> k \<noteq> n \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 2. \<And>l c n ts k t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := WAIT k)); l < N; ts l = WAIT k; c \<noteq> k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> k \<noteq> k'))) \<and> (t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> ka \<noteq> k \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 3. \<And>l c n ts t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := HOLD c)); l < N; ts l = WAIT c; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> c \<noteq> k'))) \<and> (t \<noteq> l \<longrightarrow> (\<forall>k. t < N \<and> has_ticket (ts t) k \<longrightarrow> k \<noteq> c \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 4. \<And>l c n ts k t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := REL k)); l < N; ts l = HOLD k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> k \<noteq> k')) \<and> (\<forall>ka. ka \<noteq> c \<longrightarrow> ka \<noteq> k)) \<and> (t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> ka \<noteq> k \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 5. \<And>l c n ts k. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (Suc k, n, ts(l := INIT)); l < N; ts l = REL k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> Suc k \<le> n \<and> (\<forall>t. t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> Suc k \<le> ka \<and> (\<forall>ka. ka \<noteq> Suc k \<longrightarrow> \<not> locks_ticket (ts t) ka)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>l c n ts k t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := WAIT k)); l < N; ts l = WAIT k; c \<noteq> k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> k \<noteq> k'))) \<and> (t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> ka \<noteq> k \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 2. \<And>l c n ts t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := HOLD c)); l < N; ts l = WAIT c; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> c \<noteq> k'))) \<and> (t \<noteq> l \<longrightarrow> (\<forall>k. t < N \<and> has_ticket (ts t) k \<longrightarrow> k \<noteq> c \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 3. \<And>l c n ts k t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := REL k)); l < N; ts l = HOLD k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> k \<noteq> k')) \<and> (\<forall>ka. ka \<noteq> c \<longrightarrow> ka \<noteq> k)) \<and> (t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> ka \<noteq> k \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 4. \<And>l c n ts k. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (Suc k, n, ts(l := INIT)); l < N; ts l = REL k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> Suc k \<le> n \<and> (\<forall>t. t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> Suc k \<le> ka \<and> (\<forall>ka. ka \<noteq> Suc k \<longrightarrow> \<not> locks_ticket (ts t) ka)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l c n ts t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := HOLD c)); l < N; ts l = WAIT c; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> c \<noteq> k'))) \<and> (t \<noteq> l \<longrightarrow> (\<forall>k. t < N \<and> has_ticket (ts t) k \<longrightarrow> k \<noteq> c \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 2. \<And>l c n ts k t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := REL k)); l < N; ts l = HOLD k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> k \<noteq> k')) \<and> (\<forall>ka. ka \<noteq> c \<longrightarrow> ka \<noteq> k)) \<and> (t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> ka \<noteq> k \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 3. \<And>l c n ts k. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (Suc k, n, ts(l := INIT)); l < N; ts l = REL k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> Suc k \<le> n \<and> (\<forall>t. t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> Suc k \<le> ka \<and> (\<forall>ka. ka \<noteq> Suc k \<longrightarrow> \<not> locks_ticket (ts t) ka)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l c n ts k t. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (c, n, ts(l := REL k)); l < N; ts l = HOLD k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> (t = l \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t'. t' \<noteq> l \<longrightarrow> (\<forall>k'. t' < N \<and> has_ticket (ts t') k' \<longrightarrow> k \<noteq> k')) \<and> (\<forall>ka. ka \<noteq> c \<longrightarrow> ka \<noteq> k)) \<and> (t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> ka \<noteq> k \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)))
 2. \<And>l c n ts k. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (Suc k, n, ts(l := INIT)); l < N; ts l = REL k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> Suc k \<le> n \<and> (\<forall>t. t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> Suc k \<le> ka \<and> (\<forall>ka. ka \<noteq> Suc k \<longrightarrow> \<not> locks_ticket (ts t) ka)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l c n ts k. \<lbrakk>A.reachable (c, n, ts); s = (c, n, ts); s' = (Suc k, n, ts(l := INIT)); l < N; ts l = REL k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> Suc k \<le> n \<and> (\<forall>t. t \<noteq> l \<longrightarrow> (\<forall>ka. t < N \<and> has_ticket (ts t) ka \<longrightarrow> Suc k \<le> ka \<and> (\<forall>ka. ka \<noteq> Suc k \<longrightarrow> \<not> locks_ticket (ts t) ka)))
[PROOF STEP]
by (metis Suc_le_eq holds_imp_uses locks_ticket_def le_neq_implies_less)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem mutual_exclusion: "\<lbrakk>A.reachable s;
      t<N; t'<N; t\<noteq>t'; is_HOLD (tts s t); is_HOLD (tts s t')
    \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; is_HOLD (tts s t); is_HOLD (tts s t')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases "tts s t"; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; is_HOLD (tts s t'); tts s t = HOLD x3\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases "tts s t'"; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x3 x3a. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tts s t = HOLD x3; tts s t' = HOLD x3a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using A.invar_reachable[OF is_invar1, of s]
[PROOF STATE]
proof (prove)
using this:
A.reachable s \<Longrightarrow> invar1 s

goal (1 subgoal):
 1. \<And>x3 x3a. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tts s t = HOLD x3; tts s t' = HOLD x3a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp: invar1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x3 x3a x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = HOLD x3; b t' = HOLD x3a; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> has_ticket (b t) k \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> has_ticket (b t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> locks_ticket (b t) k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis locks_ticket_simps(3) has_ticket_simps(3))


[STATEMENT]
lemma mutual_exclusion': "\<lbrakk>A.reachable s;
      t<N; t'<N; t\<noteq>t';
      locks_ticket (tts s t) tk; locks_ticket (tts s t') tk'
    \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; locks_ticket (tts s t) tk; locks_ticket (tts s t') tk'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases "tts s t"; simp; cases "tts s t'"; simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x3 x3a. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x3; tk' = x3a; tts s t = HOLD x3; tts s t' = HOLD x3a\<rbrakk> \<Longrightarrow> False
 2. \<And>x3 x4. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x3; tk' = x4; tts s t = HOLD x3; tts s t' = REL x4\<rbrakk> \<Longrightarrow> False
 3. \<And>x4 x3. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x4; tk' = x3; tts s t = REL x4; tts s t' = HOLD x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x4 x4a. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x4; tk' = x4a; tts s t = REL x4; tts s t' = REL x4a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases "tts s t'"; simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x3 x3a x3b. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x3; tk' = x3a; tts s t = HOLD x3; x3b = x3a; tts s t' = HOLD x3a\<rbrakk> \<Longrightarrow> False
 2. \<And>x3 x4. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x3; tk' = x4; tts s t = HOLD x3; tts s t' = REL x4\<rbrakk> \<Longrightarrow> False
 3. \<And>x4 x3. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x4; tk' = x3; tts s t = REL x4; tts s t' = HOLD x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x4 x4a. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x4; tk' = x4a; tts s t = REL x4; tts s t' = REL x4a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using A.invar_reachable[OF is_invar1, of s]
[PROOF STATE]
proof (prove)
using this:
A.reachable s \<Longrightarrow> invar1 s

goal (4 subgoals):
 1. \<And>x3 x3a x3b. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x3; tk' = x3a; tts s t = HOLD x3; x3b = x3a; tts s t' = HOLD x3a\<rbrakk> \<Longrightarrow> False
 2. \<And>x3 x4. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x3; tk' = x4; tts s t = HOLD x3; tts s t' = REL x4\<rbrakk> \<Longrightarrow> False
 3. \<And>x4 x3. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x4; tk' = x3; tts s t = REL x4; tts s t' = HOLD x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x4 x4a. \<lbrakk>A.reachable s; t < N; t' < N; t \<noteq> t'; tk = x4; tk' = x4a; tts s t = REL x4; tts s t' = REL x4a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp_all simp: invar1_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = HOLD tk; b t' = HOLD tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> has_ticket (b t) k \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> has_ticket (b t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> locks_ticket (b t) k)\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = HOLD tk; b t' = REL tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> has_ticket (b t) k \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> has_ticket (b t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> locks_ticket (b t) k)\<rbrakk> \<Longrightarrow> False
 3. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = REL tk; b t' = HOLD tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> has_ticket (b t) k \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> has_ticket (b t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> locks_ticket (b t) k)\<rbrakk> \<Longrightarrow> False
 4. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = REL tk; b t' = REL tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> has_ticket (b t) k \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> has_ticket (b t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> locks_ticket (b t) k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding locks_ticket_def has_ticket_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = HOLD tk; b t' = HOLD tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> (b t = WAIT k \<or> b t = HOLD k \<or> b t = REL k) \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> (b t' = WAIT k' \<or> b t' = HOLD k' \<or> b t' = REL k') \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> (b t = HOLD k \<or> b t = REL k))\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = HOLD tk; b t' = REL tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> (b t = WAIT k \<or> b t = HOLD k \<or> b t = REL k) \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> (b t' = WAIT k' \<or> b t' = HOLD k' \<or> b t' = REL k') \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> (b t = HOLD k \<or> b t = REL k))\<rbrakk> \<Longrightarrow> False
 3. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = REL tk; b t' = HOLD tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> (b t = WAIT k \<or> b t = HOLD k \<or> b t = REL k) \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> (b t' = WAIT k' \<or> b t' = HOLD k' \<or> b t' = REL k') \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> (b t = HOLD k \<or> b t = REL k))\<rbrakk> \<Longrightarrow> False
 4. \<And>x a b. \<lbrakk>A.reachable (x, a, b); t < N; t' < N; t \<noteq> t'; b t = REL tk; b t' = REL tk'; s = (x, a, b); x \<le> a; \<forall>t k. t < N \<and> (b t = WAIT k \<or> b t = HOLD k \<or> b t = REL k) \<longrightarrow> x \<le> k \<and> k < a \<and> (\<forall>t' k'. t' < N \<and> (b t' = WAIT k' \<or> b t' = HOLD k' \<or> b t' = REL k') \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> x \<longrightarrow> \<not> (b t = HOLD k \<or> b t = REL k))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply metis+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fair_aux:
    assumes R: "A.is_run s"
    assumes A: "i<j" "cc (s i) \<le> k" "k < cc (s j)" "t<N" "tts (s i) t=WAIT k"
    shows "\<exists>l. i\<le>l \<and> l<j \<and> tts (s l) t = HOLD k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
interpret A: run as\<^sub>0 alstep s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DF_System.run as\<^sub>0 alstep s
[PROOF STEP]
by unfold_locales fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
proof (induction "j-i" arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = j - i
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (2 subgoals):
 1. \<And>i. \<lbrakk>0 = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = j - i
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 = j - i
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case (Suc i')
[PROOF STATE]
proof (state)
this:
\<lbrakk>i' = j - ?i; ?i < j; cc (s ?i) \<le> k; k < cc (s j); t < N; tts (s ?i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>?i. l < j \<and> tts (s l) t = HOLD k
Suc i' = j - i
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
hence [simp]: "i'=j - Suc i"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i' = j - ?i; ?i < j; cc (s ?i) \<le> k; k < cc (s j); t < N; tts (s ?i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>?i. l < j \<and> tts (s l) t = HOLD k
Suc i' = j - i
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. i' = j - Suc i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' = j - Suc i

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
note IH=Suc.hyps(1)[OF this]
[PROOF STATE]
proof (state)
this:
\<lbrakk>Suc i < j; cc (s (Suc i)) \<le> k; k < cc (s j); t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
obtain t' where "alstep t' (s i) (s (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t'. alstep t' (s i) (s (Suc i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule A.stepE)
[PROOF STATE]
proof (state)
this:
alstep t' (s i) (s (Suc i))

goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<And>i. \<lbrakk>x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k; Suc x = j - i; i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alstep t' (s i) (s (Suc i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
alstep t' (s i) (s (Suc i))

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
alstep t' (s i) (s (Suc i))
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c n ts c' n' s'. \<lbrakk>i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; astep_sng (c, n, ts t') (c', n', s')\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case (1 c n ts c' n' s')
[PROOF STATE]
proof (state)
this:
s i = (c, n, ts)
s (Suc i) = (c', n', ts(t' := s'))
t' < N
astep_sng (c, n, ts t') (c', n', s')

goal (1 subgoal):
 1. \<And>c n ts c' n' s'. \<lbrakk>i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; astep_sng (c, n, ts t') (c', n', s')\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
note [simp] = "1"(1,2,3)
[PROOF STATE]
proof (state)
this:
s i = (c, n, ts)
s (Suc i) = (c', n', ts(t' := s'))
t' < N

goal (1 subgoal):
 1. \<And>c n ts c' n' s'. \<lbrakk>i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; astep_sng (c, n, ts t') (c', n', s')\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
from A.run_invar[OF is_invar1, of i]
[PROOF STATE]
proof (chain)
picking this:
invar1 (s i)
[PROOF STEP]
have "invar1 (c,n,ts)"
[PROOF STATE]
proof (prove)
using this:
invar1 (s i)

goal (1 subgoal):
 1. invar1 (c, n, ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invar1 (c, n, ts)

goal (1 subgoal):
 1. \<And>c n ts c' n' s'. \<lbrakk>i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; astep_sng (c, n, ts t') (c', n', s')\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
note I1 = this[unfolded invar1_def, simplified]
[PROOF STATE]
proof (state)
this:
c \<le> n \<and> (\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k))

goal (1 subgoal):
 1. \<And>c n ts c' n' s'. \<lbrakk>i < j; cc (s i) \<le> k; k < cc (s j); t < N; tts (s i) t = WAIT k; s i = (c, n, ts); s (Suc i) = (c', n', ts(t' := s')); t' < N; astep_sng (c, n, ts t') (c', n', s')\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
from "1"(4)
[PROOF STATE]
proof (chain)
picking this:
astep_sng (c, n, ts t') (c', n', s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
astep_sng (c, n, ts t') (c', n', s')

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
proof (cases rule: astep_sng.cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>ts t' = INIT; c' = c; n' = n + 1; s' = WAIT n\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = WAIT ka; c' = c; n' = n; s' = WAIT ka; c \<noteq> ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 4. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 5. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case enter_wait
[PROOF STATE]
proof (state)
this:
ts t' = INIT
c' = c
n' = n + 1
s' = WAIT n

goal (5 subgoals):
 1. \<lbrakk>ts t' = INIT; c' = c; n' = n + 1; s' = WAIT n\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = WAIT ka; c' = c; n' = n; s' = WAIT ka; c \<noteq> ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 4. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 5. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts t' = INIT
c' = c
n' = n + 1
s' = WAIT n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ts t' = INIT
c' = c
n' = n + 1
s' = WAIT n

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
using IH Suc.prems
[PROOF STATE]
proof (prove)
using this:
ts t' = INIT
c' = c
n' = n + 1
s' = WAIT n
\<lbrakk>Suc i < j; cc (s (Suc i)) \<le> k; k < cc (s j); t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = INIT; c' = c; n' = Suc n; s' = WAIT n; \<lbrakk>Suc i < j; (if t = t' then WAIT n else ts t) = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k; i < j; c \<le> k; k < cc (s j); t < N; ts t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
by (metis "1"(2) Suc_leD Suc_lessI fst_conv leD thread.distinct(1))
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal (4 subgoals):
 1. \<And>ka. \<lbrakk>ts t' = WAIT ka; c' = c; n' = n; s' = WAIT ka; c \<noteq> ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 4. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ka. \<lbrakk>ts t' = WAIT ka; c' = c; n' = n; s' = WAIT ka; c \<noteq> ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 4. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case (loop_wait k)
[PROOF STATE]
proof (state)
this:
ts t' = WAIT k
c' = c
n' = n
s' = WAIT k
c \<noteq> k

goal (4 subgoals):
 1. \<And>ka. \<lbrakk>ts t' = WAIT ka; c' = c; n' = n; s' = WAIT ka; c \<noteq> ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 4. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts t' = WAIT k
c' = c
n' = n
s' = WAIT k
c \<noteq> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ts t' = WAIT k
c' = c
n' = n
s' = WAIT k
c \<noteq> k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
using IH Suc.prems
[PROOF STATE]
proof (prove)
using this:
ts t' = WAIT k
c' = c
n' = n
s' = WAIT k
c \<noteq> k
\<lbrakk>Suc i < j; cc (s (Suc i)) \<le> k; k < cc (s j); t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = WAIT k; c' = c; n' = n; s' = WAIT k; c \<noteq> k; \<lbrakk>Suc i < j; (if t = t' then WAIT k else ts t) = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k; i < j; c \<le> k; k < cc (s j); t < N; ts t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
by (metis "1"(2) Suc_leD Suc_lessI fst_conv leD)
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal (3 subgoals):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case exit_wait
[PROOF STATE]
proof (state)
this:
ts t' = WAIT c
c' = c
n' = n
s' = HOLD c

goal (3 subgoals):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 3. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts t' = WAIT c
c' = c
n' = n
s' = HOLD c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ts t' = WAIT c
c' = c
n' = n
s' = HOLD c

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply (cases "t'=t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' = t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' = t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' = t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t = WAIT k; c' = k; n' = n; s' = HOLD k; t' = t; i < j; k < cc (s j); t < N; c = k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
by (metis "1"(2) Suc_leD Suc_lessI fst_conv fun_upd_same leD
                less_or_eq_imp_le snd_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
using Suc.prems IH
[PROOF STATE]
proof (prove)
using this:
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k
\<lbrakk>Suc i < j; cc (s (Suc i)) \<le> k; k < cc (s j); t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k

goal (1 subgoal):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = WAIT c; c' = c; n' = n; s' = HOLD c; t' \<noteq> t; i < j; c \<le> k; k < cc (s j); t < N; ts t = WAIT k; Suc i < j \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
by (metis "1"(2) Suc_leD Suc_lessI fst_conv leD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case (start_release k)
[PROOF STATE]
proof (state)
this:
ts t' = HOLD k
c' = c
n' = n
s' = REL k

goal (2 subgoals):
 1. \<And>ka. \<lbrakk>ts t' = HOLD ka; c' = c; n' = n; s' = REL ka\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts t' = HOLD k
c' = c
n' = n
s' = REL k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ts t' = HOLD k
c' = c
n' = n
s' = REL k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
using IH Suc.prems
[PROOF STATE]
proof (prove)
using this:
ts t' = HOLD k
c' = c
n' = n
s' = REL k
\<lbrakk>Suc i < j; cc (s (Suc i)) \<le> k; k < cc (s j); t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = HOLD k; c' = c; n' = n; s' = REL k; \<lbrakk>Suc i < j; (if t = t' then REL k else ts t) = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k; i < j; c \<le> k; k < cc (s j); t < N; ts t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
by (metis "1"(2) Suc_leD Suc_lessI fst_conv leD thread.distinct(7))
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal (1 subgoal):
 1. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
case (release k)
[PROOF STATE]
proof (state)
this:
ts t' = REL k
c' = k + 1
n' = n
s' = INIT

goal (1 subgoal):
 1. \<And>ka. \<lbrakk>ts t' = REL ka; c' = ka + 1; n' = n; s' = INIT\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts t' = REL k
c' = k + 1
n' = n
s' = INIT
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ts t' = REL k
c' = k + 1
n' = n
s' = INIT

goal (1 subgoal):
 1. \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply (cases "t'=t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ts t' = REL k; c' = k + 1; n' = n; s' = INIT; t' = t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<lbrakk>ts t' = REL k; c' = k + 1; n' = n; s' = INIT; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
using I1 IH Suc.prems
[PROOF STATE]
proof (prove)
using this:
c \<le> n \<and> (\<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k))
\<lbrakk>Suc i < j; cc (s (Suc i)) \<le> k; k < cc (s j); t < N; tts (s (Suc i)) t = WAIT k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k
i < j
cc (s i) \<le> k
k < cc (s j)
t < N
tts (s i) t = WAIT k

goal (2 subgoals):
 1. \<lbrakk>ts t' = REL k; c' = k + 1; n' = n; s' = INIT; t' = t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
 2. \<lbrakk>ts t' = REL k; c' = k + 1; n' = n; s' = INIT; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts t' = REL k; c' = Suc k; n' = n; s' = INIT; t' \<noteq> t; \<lbrakk>Suc i < j; Suc k \<le> k\<rbrakk> \<Longrightarrow> \<exists>l\<ge>Suc i. l < j \<and> tts (s l) t = HOLD k; i < j; c \<le> k; k < cc (s j); t < N; ts t = WAIT k; c \<le> n; \<forall>t k. t < N \<and> has_ticket (ts t) k \<longrightarrow> c \<le> k \<and> k < n \<and> (\<forall>t' k'. t' < N \<and> has_ticket (ts t') k' \<and> t \<noteq> t' \<longrightarrow> k \<noteq> k') \<and> (\<forall>k. k \<noteq> c \<longrightarrow> \<not> locks_ticket (ts t) k)\<rbrakk> \<Longrightarrow> \<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k
[PROOF STEP]
by (metis "1"(2) "1"(3) Suc_leD Suc_leI Suc_lessI fst_conv
              locks_ticket_simps(4) le_antisym not_less_eq_eq
              has_ticket_simps(2) has_ticket_simps(4))
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>l\<ge>i. l < j \<and> tts (s l) t = HOLD k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s_case_expand:
    "(case s of (c, n, ts) \<Rightarrow> P c n ts) = P (cc s) (nn s) (tts s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case s of (c, n, ts) \<Rightarrow> P c n ts) = P (cc s) (nn s) (tts s)
[PROOF STEP]
by (auto split: prod.splits)