[STATEMENT]
lemma offs_enum_pred [rule_format]:
  assumes A: "index_less index key"
  shows "(\<forall>x \<in> set xs. key x \<in> {mi..ma}) \<longrightarrow>
    offs_pred (offs (enum xs index key n mi ma) k) (length xs + k)
      xs index key mi ma"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set xs. key x \<in> {mi..ma}) \<longrightarrow> offs_pred (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma
[PROOF STEP]
proof (induction xs, simp add: offs_pred_def offs_num_def,
 simp add: Let_def offs_pred_def offs_length enum_length, rule impI, (erule conjE)+,
 simp, rule allI, rule impI, erule allE, drule mp, assumption)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; i < n; offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i\<rbrakk> \<Longrightarrow> offs_num n (a # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k) (Suc (length xs + k)) (a # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k ! i
[PROOF STEP]
fix x xs i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; i < n; offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i\<rbrakk> \<Longrightarrow> offs_num n (a # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k) (Suc (length xs + k)) (a # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k ! i
[PROOF STEP]
let ?i' = "index key x n mi ma"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; i < n; offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i\<rbrakk> \<Longrightarrow> offs_num n (a # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k) (Suc (length xs + k)) (a # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k ! i
[PROOF STEP]
let ?ns = "enum xs index key n mi ma"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; i < n; offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i\<rbrakk> \<Longrightarrow> offs_num n (a # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k) (Suc (length xs + k)) (a # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k ! i
[PROOF STEP]
let ?ns' = "?ns[?i' := Suc (?ns ! ?i')]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; i < n; offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i\<rbrakk> \<Longrightarrow> offs_num n (a # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k) (Suc (length xs + k)) (a # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k ! i
[PROOF STEP]
assume
    B: "\<forall>x \<in> set xs. mi \<le> key x \<and> key x \<le> ma" and
    C: "i < n" and
    D: "offs_num n xs index key mi ma i \<le>
      offs_next (offs ?ns k) (length xs + k) xs index key mi ma i - offs ?ns k ! i"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma
i < n
offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i

goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; i < n; offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i\<rbrakk> \<Longrightarrow> offs_num n (a # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k) (Suc (length xs + k)) (a # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k ! i
[PROOF STEP]
have E: "(if i < ?i' then (\<le>) else (<))
    (offs_next (offs ?ns k) (length xs + k) xs index key mi ma i)
    (offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < index key x n mi ma then (\<le>) else (<)) (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) (offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i)
[PROOF STEP]
using A and B
[PROOF STATE]
proof (prove)
using this:
index_less index key
\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma

goal (1 subgoal):
 1. (if i < index key x n mi ma then (\<le>) else (<)) (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) (offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i)
[PROOF STEP]
by (subst offs_enum_next_cons, simp_all)
[PROOF STATE]
proof (state)
this:
(if i < index key x n mi ma then (\<le>) else (<)) (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) (offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>mi \<le> key a; key a \<le> ma; \<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma; i < n; offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i\<rbrakk> \<Longrightarrow> offs_num n (a # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k) (Suc (length xs + k)) (a # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key a n mi ma := Suc (enum xs index key n mi ma ! index key a n mi ma)]) k ! i
[PROOF STEP]
show "offs_num n (x # xs) index key mi ma i \<le>
    offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma i -
      offs ?ns' k ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offs_num n (x # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! i
[PROOF STEP]
proof (subst offs_update, simp add: enum_length C, rule linorder_cases [of i ?i'],
   simp_all add: offs_num_cons)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i < index key x n mi ma \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs (enum xs index key n mi ma) k ! i
 2. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 3. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
assume "i < ?i'"
[PROOF STATE]
proof (state)
this:
i < index key x n mi ma

goal (3 subgoals):
 1. i < index key x n mi ma \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs (enum xs index key n mi ma) k ! i
 2. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 3. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
hence "offs_next (offs ?ns k) (length xs + k) xs index key mi ma i \<le>
      offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
using this:
i < index key x n mi ma

goal (1 subgoal):
 1. offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
i < index key x n mi ma
(if i < index key x n mi ma then (\<le>) else (<)) (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) (offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i

goal (3 subgoals):
 1. i < index key x n mi ma \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs (enum xs index key n mi ma) k ! i
 2. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 3. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
thus "offs_num n xs index key mi ma i \<le>
      offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma i -
        offs ?ns k ! i"
[PROOF STATE]
proof (prove)
using this:
offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i

goal (1 subgoal):
 1. offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs (enum xs index key n mi ma) k ! i
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i
offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i

goal (1 subgoal):
 1. offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs (enum xs index key n mi ma) k ! i
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs (enum xs index key n mi ma) k ! i

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
assume F: "i = ?i'"
[PROOF STATE]
proof (state)
this:
i = index key x n mi ma

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
hence "Suc (offs_num n xs index key mi ma ?i') \<le>
      Suc (offs_next (offs ?ns k) (length xs + k) xs index key mi ma ?i' -
        offs ?ns k ! ?i')"
[PROOF STATE]
proof (prove)
using this:
i = index key x n mi ma

goal (1 subgoal):
 1. Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma)
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
i = index key x n mi ma
offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i

goal (1 subgoal):
 1. Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma)

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma)

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
from A and B and C and F
[PROOF STATE]
proof (chain)
picking this:
index_less index key
\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma
i < n
i = index key x n mi ma
[PROOF STEP]
have "\<dots> =
      Suc (offs_next (offs ?ns k) (length xs + k) xs index key mi ma ?i') -
        offs ?ns k ! ?i'"
[PROOF STATE]
proof (prove)
using this:
index_less index key
\<forall>x\<in>set xs. mi \<le> key x \<and> key x \<le> ma
i < n
i = index key x n mi ma

goal (1 subgoal):
 1. Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma) = Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma
[PROOF STEP]
by (rule_tac Suc_diff_le [symmetric], rule_tac offs_enum_next_ge, simp_all)
[PROOF STATE]
proof (state)
this:
Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma) = Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma
[PROOF STEP]
have "Suc (offs_num n xs index key mi ma ?i') \<le>
      Suc (offs_next (offs ?ns k) (length xs + k) xs index key mi ma ?i') -
        offs ?ns k ! ?i'"
[PROOF STATE]
proof (prove)
using this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma

goal (1 subgoal):
 1. Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
have
     "Suc (offs_next (offs ?ns k) (length xs + k) xs index key mi ma ?i') \<le>
      offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma ?i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma)
[PROOF STEP]
using E and F
[PROOF STATE]
proof (prove)
using this:
(if i < index key x n mi ma then (\<le>) else (<)) (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) (offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i)
i = index key x n mi ma

goal (1 subgoal):
 1. Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma)

goal (2 subgoals):
 1. i = index key x n mi ma \<Longrightarrow> Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
 2. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma
Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma)
[PROOF STEP]
show "Suc (offs_num n xs index key mi ma ?i') \<le>
      offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma ?i' -
        offs ?ns k ! ?i'"
[PROOF STATE]
proof (prove)
using this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) - offs (enum xs index key n mi ma) k ! index key x n mi ma
Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma)

goal (1 subgoal):
 1. Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
Suc (offs_num n xs index key mi ma (index key x n mi ma)) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma (index key x n mi ma) - offs (enum xs index key n mi ma) k ! index key x n mi ma

goal (1 subgoal):
 1. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
assume "?i' < i"
[PROOF STATE]
proof (state)
this:
index key x n mi ma < i

goal (1 subgoal):
 1. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
hence "Suc (offs_next (offs ?ns k) (length xs + k) xs index key mi ma i) \<le>
      offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma i"
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma < i

goal (1 subgoal):
 1. Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
index key x n mi ma < i
(if i < index key x n mi ma then (\<le>) else (<)) (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) (offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i)

goal (1 subgoal):
 1. Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i

goal (1 subgoal):
 1. index key x n mi ma < i \<Longrightarrow> offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
thus "offs_num n xs index key mi ma i \<le>
      offs_next (offs ?ns' k) (Suc (length xs + k)) (x # xs) index key mi ma i -
        Suc (offs ?ns k ! i)"
[PROOF STATE]
proof (prove)
using this:
Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i

goal (1 subgoal):
 1. offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Suc (offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i) \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i
offs_num n xs index key mi ma i \<le> offs_next (offs (enum xs index key n mi ma) k) (length xs + k) xs index key mi ma i - offs (enum xs index key n mi ma) k ! i

goal (1 subgoal):
 1. offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
offs_num n xs index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - Suc (offs (enum xs index key n mi ma) k ! i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
offs_num n (x # xs) index key mi ma i \<le> offs_next (offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k) (Suc (length xs + k)) (x # xs) index key mi ma i - offs ((enum xs index key n mi ma)[index key x n mi ma := Suc (enum xs index key n mi ma ! index key x n mi ma)]) k ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fill_offs_enum_count_item [rule_format]:
 "\<lbrakk>index_less index key; \<forall>x \<in> set xs. key x \<in> {mi..ma}; 0 < n\<rbrakk> \<Longrightarrow>
    count (mset (map the (fill xs (offs (enum xs index key n mi ma) 0)
      index key (length xs) mi ma))) x =
    count (mset xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>index_less index key; \<forall>x\<in>set xs. key x \<in> {mi..ma}; 0 < n\<rbrakk> \<Longrightarrow> count (mset (map the (fill xs (offs (enum xs index key n mi ma) 0) index key (length xs) mi ma))) x = count (mset xs) x
[PROOF STEP]
by (subst fill_count_item, simp_all, simp only: length_greater_0_conv [symmetric]
 offs_length enum_length, insert offs_enum_pred [of index key xs mi ma n 0], simp)


[STATEMENT]
lemma nths_count:
 "count (mset (nths xs A)) x =
    count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}
[PROOF STEP]
proof (induction xs arbitrary: A, simp_all add: nths_Cons)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
fix v xs A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
let ?B = "{i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
let ?C = "\<lambda>v. {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
have A: "\<And>v. ?C v = ?C v \<inter> {0} \<union> ?C v \<inter> {i. \<exists>j. i = Suc j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} = {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} \<inter> {0} \<union> {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j}
[PROOF STEP]
by (subst Int_Un_distrib [symmetric], auto, arith)
[PROOF STATE]
proof (state)
this:
{i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} = {i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {0} \<union> {i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j}

goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
have "\<And>v. card (?C v) = card (?C v \<inter> {0}) + card (?C v \<inter> {i. \<exists>j. i = Suc j})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} \<inter> {0}) + card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})
[PROOF STEP]
by (subst A, rule card_Un_disjoint, simp_all, blast)
[PROOF STATE]
proof (state)
this:
card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {0}) + card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})

goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {0}) + card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})

goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
have "\<And>v. card ?B = card (?C v \<inter> {i. \<exists>j. i = Suc j})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})
[PROOF STEP]
by (rule bij_betw_same_card [of Suc], auto)
[PROOF STATE]
proof (state)
this:
card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})

goal (1 subgoal):
 1. \<And>a xs A. (\<And>A. count (mset (nths xs A)) x = count (mset xs) x - card {i. i < length xs \<and> i \<notin> A \<and> xs ! i = x}) \<Longrightarrow> (0 \<in> A \<longrightarrow> (a = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (a = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (a \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (a # xs) ! i = x}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {0}) + card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})
card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})
[PROOF STEP]
show
   "(0 \<in> A \<longrightarrow>
      (v = x \<longrightarrow> Suc (count (mset xs) x - card ?B) =
        Suc (count (mset xs) x) - card (?C x)) \<and>
      (v \<noteq> x \<longrightarrow> count (mset xs) x - card ?B =
        count (mset xs) x - card (?C v))) \<and>
    (0 \<notin> A \<longrightarrow>
      (v = x \<longrightarrow> count (mset xs) x - card ?B =
        Suc (count (mset xs) x) - card (?C x)) \<and>
      (v \<noteq> x \<longrightarrow> count (mset xs) x - card ?B =
        count (mset xs) x - card (?C v)))"
[PROOF STATE]
proof (prove)
using this:
card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {0}) + card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})
card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (?v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})

goal (1 subgoal):
 1. (0 \<in> A \<longrightarrow> (v = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (v \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (v = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (v \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x}))
[PROOF STEP]
proof ((rule_tac [!] conjI, rule_tac [!] impI)+, simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 \<in> A; v = x; \<And>v. card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} = card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}; \<And>v. card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})\<rbrakk> \<Longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}
[PROOF STEP]
have "card ?B \<le> count (mset xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} \<le> count (mset xs) x
[PROOF STEP]
by (simp add: count_mset length_filter_conv_card, rule card_mono,
       simp, blast)
[PROOF STATE]
proof (state)
this:
card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} \<le> count (mset xs) x

goal (1 subgoal):
 1. \<lbrakk>0 \<in> A; v = x; \<And>v. card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} = card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}; \<And>v. card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = card ({i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x} \<inter> {i. \<exists>j. i = Suc j})\<rbrakk> \<Longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}
[PROOF STEP]
thus "Suc (count (mset xs) x - card ?B) = Suc (count (mset xs) x) - card ?B"
[PROOF STATE]
proof (prove)
using this:
card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} \<le> count (mset xs) x

goal (1 subgoal):
 1. Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}
[PROOF STEP]
by (rule Suc_diff_le [symmetric])
[PROOF STATE]
proof (state)
this:
Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(0 \<in> A \<longrightarrow> (v = x \<longrightarrow> Suc (count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x}) = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (v \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x})) \<and> (0 \<notin> A \<longrightarrow> (v = x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = Suc (count (mset xs) x) - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (x # xs) ! i = x}) \<and> (v \<noteq> x \<longrightarrow> count (mset xs) x - card {i. i < length xs \<and> Suc i \<notin> A \<and> xs ! i = x} = count (mset xs) x - card {i. i < Suc (length xs) \<and> i \<notin> A \<and> (v # xs) ! i = x}))

goal:
No subgoals!
[PROOF STEP]
qed