[STATEMENT]
lemma small_mixed_integer_solution: fixes A\<^sub>1 :: "'a mat"
  assumes db: "is_det_bound db"
    and A1: "A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n"
    and A2: "A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n"
    and b1: "b\<^sub>1 \<in> carrier_vec nr\<^sub>1"
    and b2: "b\<^sub>2 \<in> carrier_vec nr\<^sub>2"
    and A1Bnd: "A\<^sub>1 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)"
    and b1Bnd: "b\<^sub>1 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)"
    and A2Bnd: "A\<^sub>2 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)"
    and b2Bnd: "b\<^sub>2 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)"
    and x: "x \<in> carrier_vec n"
    and xI: "x \<in> indexed_Ints_vec I"
    and sol_nonstrict: "A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1"
    and sol_strict: "A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2"
    and non_degenerate: "nr\<^sub>1 \<noteq> 0 \<or> nr\<^sub>2 \<noteq> 0 \<or> Bnd \<ge> 0"
  shows "\<exists> x.
  x \<in> carrier_vec n \<and>
  x \<in> indexed_Ints_vec I \<and>
  A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and>
  A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and>
  x \<in> Bounded_vec (of_int (int (n+1) * db n Bnd))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
proof (cases "Bnd \<ge> 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
 2. \<not> 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
1 \<le> Bnd

goal (2 subgoals):
 1. 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
 2. \<not> 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
hence "max 1 Bnd = Bnd"
[PROOF STATE]
proof (prove)
using this:
1 \<le> Bnd

goal (1 subgoal):
 1. max 1 Bnd = Bnd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max 1 Bnd = Bnd

goal (2 subgoals):
 1. 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
 2. \<not> 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
with small_mixed_integer_solution_main[OF assms(1-13)] True
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
1 \<le> Bnd
max 1 Bnd = Bnd
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n (max 1 Bnd)))
1 \<le> Bnd
max 1 Bnd = Bnd

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))

goal (1 subgoal):
 1. \<not> 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
case trivial: False
[PROOF STATE]
proof (state)
this:
\<not> 1 \<le> Bnd

goal (1 subgoal):
 1. \<not> 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?oi = "of_int :: int \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 1 \<le> Bnd \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
 2. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
 2. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier_vec n
n = 0
[PROOF STEP]
have "x \<in> Bounded_vec b" for b
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec n
n = 0

goal (1 subgoal):
 1. x \<in> Bounded_vec b
[PROOF STEP]
unfolding Bounded_vec_def
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec n
n = 0

goal (1 subgoal):
 1. x \<in> {x. \<forall>i<dim_vec x. \<bar>x $ i\<bar> \<le> b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> Bounded_vec ?b4

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
 2. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
with xI x sol_nonstrict sol_strict
[PROOF STATE]
proof (chain)
picking this:
x \<in> indexed_Ints_vec I
x \<in> carrier_vec n
A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1
A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2
x \<in> Bounded_vec ?b4
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> indexed_Ints_vec I
x \<in> carrier_vec n
A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1
A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2
x \<in> Bounded_vec ?b4

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
case n: False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
fix A nr
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
assume A: "A \<in> carrier_mat nr n" and Bnd: "A \<in> \<int>\<^sub>m \<inter> Bounded_mat (?oi Bnd)"
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat nr n
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat nr n
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
assume "i < nr" "j < n"
[PROOF STATE]
proof (state)
this:
i < nr
j < n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
with Bnd A
[PROOF STATE]
proof (chain)
picking this:
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A \<in> carrier_mat nr n
i < nr
j < n
[PROOF STEP]
have *: "A $$ (i,j) \<in> \<int>" "abs (A $$ (i,j)) \<le> ?oi Bnd"
[PROOF STATE]
proof (prove)
using this:
A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
A \<in> carrier_mat nr n
i < nr
j < n

goal (1 subgoal):
 1. A $$ (i, j) \<in> \<int> &&& \<bar>A $$ (i, j)\<bar> \<le> of_int Bnd
[PROOF STEP]
unfolding Bounded_mat_def Ints_mat_def
[PROOF STATE]
proof (prove)
using this:
A \<in> {A. \<forall>i<dim_row A. \<forall>j<dim_col A. A $$ (i, j) \<in> \<int>} \<inter> {A. \<forall>i<dim_row A. \<forall>j<dim_col A. \<bar>A $$ (i, j)\<bar> \<le> of_int Bnd}
A \<in> carrier_mat nr n
i < nr
j < n

goal (1 subgoal):
 1. A $$ (i, j) \<in> \<int> &&& \<bar>A $$ (i, j)\<bar> \<le> of_int Bnd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (i, j) \<in> \<int>
\<bar>A $$ (i, j)\<bar> \<le> of_int Bnd

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from Ints_nonzero_abs_less1[OF *(1)] *(2) trivial
[PROOF STATE]
proof (chain)
picking this:
\<bar>A $$ (i, j)\<bar> < (1::'a) \<Longrightarrow> A $$ (i, j) = (0::'a)
\<bar>A $$ (i, j)\<bar> \<le> of_int Bnd
\<not> 1 \<le> Bnd
[PROOF STEP]
have "A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>A $$ (i, j)\<bar> < (1::'a) \<Longrightarrow> A $$ (i, j) = (0::'a)
\<bar>A $$ (i, j)\<bar> \<le> of_int Bnd
\<not> 1 \<le> Bnd

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
by (meson add_le_less_mono int_one_le_iff_zero_less less_add_same_cancel2 of_int_0_less_iff zero_less_abs_iff)
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
with *(2)
[PROOF STATE]
proof (chain)
picking this:
\<bar>A $$ (i, j)\<bar> \<le> of_int Bnd
A $$ (i, j) = (0::'a)
[PROOF STEP]
have "Bnd \<ge> 0" "A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>A $$ (i, j)\<bar> \<le> of_int Bnd
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. 0 \<le> Bnd &&& A $$ (i, j) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> Bnd
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i6 < nr; ?j6 < n\<rbrakk> \<Longrightarrow> 0 \<le> Bnd
\<lbrakk>?i6 < nr; ?j6 < n\<rbrakk> \<Longrightarrow> A $$ (?i6, ?j6) = (0::'a)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i6 < nr; ?j6 < n\<rbrakk> \<Longrightarrow> 0 \<le> Bnd
\<lbrakk>?i6 < nr; ?j6 < n\<rbrakk> \<Longrightarrow> A $$ (?i6, ?j6) = (0::'a)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
have A0: "A = 0\<^sub>m nr n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = 0\<^sub>m nr n
[PROOF STEP]
by (intro eq_matI, insert main A, auto)
[PROOF STATE]
proof (state)
this:
A = 0\<^sub>m nr n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
have "nr \<noteq> 0 \<Longrightarrow> Bnd \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nr \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd
[PROOF STEP]
using main[of 0 0] n
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < nr; 0 < n\<rbrakk> \<Longrightarrow> 0 \<le> Bnd
\<lbrakk>0 < nr; 0 < n\<rbrakk> \<Longrightarrow> A $$ (0, 0) = (0::'a)
n \<noteq> 0

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

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
note A0 this
[PROOF STATE]
proof (state)
this:
A = 0\<^sub>m nr n
nr \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A6 \<in> carrier_mat ?nr6 n; ?A6 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)\<rbrakk> \<Longrightarrow> ?A6 = 0\<^sub>m ?nr6 n
\<lbrakk>?A6 \<in> carrier_mat ?nr6 n; ?A6 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd); ?nr6 \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> Bnd

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A6 \<in> carrier_mat ?nr6 n; ?A6 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)\<rbrakk> \<Longrightarrow> ?A6 = 0\<^sub>m ?nr6 n
\<lbrakk>?A6 \<in> carrier_mat ?nr6 n; ?A6 \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd); ?nr6 \<noteq> 0\<rbrakk> \<Longrightarrow> 0 \<le> Bnd

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from main[OF A1 A1Bnd]
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>1 = 0\<^sub>m nr\<^sub>1 n
nr\<^sub>1 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd
[PROOF STEP]
have A1: "A\<^sub>1 = 0\<^sub>m nr\<^sub>1 n" and nr1: "nr\<^sub>1 \<noteq> 0 \<Longrightarrow> Bnd \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 = 0\<^sub>m nr\<^sub>1 n
nr\<^sub>1 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd

goal (1 subgoal):
 1. A\<^sub>1 = 0\<^sub>m nr\<^sub>1 n &&& (nr\<^sub>1 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A\<^sub>1 = 0\<^sub>m nr\<^sub>1 n
nr\<^sub>1 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from main[OF A2 A2Bnd]
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>2 = 0\<^sub>m nr\<^sub>2 n
nr\<^sub>2 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd
[PROOF STEP]
have A2: "A\<^sub>2 = 0\<^sub>m nr\<^sub>2 n" and nr2: "nr\<^sub>2 \<noteq> 0 \<Longrightarrow> Bnd \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 = 0\<^sub>m nr\<^sub>2 n
nr\<^sub>2 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd

goal (1 subgoal):
 1. A\<^sub>2 = 0\<^sub>m nr\<^sub>2 n &&& (nr\<^sub>2 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A\<^sub>2 = 0\<^sub>m nr\<^sub>2 n
nr\<^sub>2 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?x = "0\<^sub>v n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
proof (intro exI[of _ ?x] conjI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. 0\<^sub>v n \<in> carrier_vec n
 2. 0\<^sub>v n \<in> indexed_Ints_vec I
 3. A\<^sub>1 *\<^sub>v 0\<^sub>v n \<le> b\<^sub>1
 4. A\<^sub>2 *\<^sub>v 0\<^sub>v n <\<^sub>v b\<^sub>2
 5. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
show "A\<^sub>1 *\<^sub>v ?x \<le> b\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>1 *\<^sub>v 0\<^sub>v n \<le> b\<^sub>1
[PROOF STEP]
using sol_nonstrict x
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1
x \<in> carrier_vec n

goal (1 subgoal):
 1. A\<^sub>1 *\<^sub>v 0\<^sub>v n \<le> b\<^sub>1
[PROOF STEP]
unfolding A1
[PROOF STATE]
proof (prove)
using this:
0\<^sub>m nr\<^sub>1 n *\<^sub>v x \<le> b\<^sub>1
x \<in> carrier_vec n

goal (1 subgoal):
 1. 0\<^sub>m nr\<^sub>1 n *\<^sub>v 0\<^sub>v n \<le> b\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A\<^sub>1 *\<^sub>v 0\<^sub>v n \<le> b\<^sub>1

goal (4 subgoals):
 1. 0\<^sub>v n \<in> carrier_vec n
 2. 0\<^sub>v n \<in> indexed_Ints_vec I
 3. A\<^sub>2 *\<^sub>v 0\<^sub>v n <\<^sub>v b\<^sub>2
 4. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
show "A\<^sub>2 *\<^sub>v ?x <\<^sub>v b\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>2 *\<^sub>v 0\<^sub>v n <\<^sub>v b\<^sub>2
[PROOF STEP]
using sol_strict x
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2
x \<in> carrier_vec n

goal (1 subgoal):
 1. A\<^sub>2 *\<^sub>v 0\<^sub>v n <\<^sub>v b\<^sub>2
[PROOF STEP]
unfolding A2
[PROOF STATE]
proof (prove)
using this:
0\<^sub>m nr\<^sub>2 n *\<^sub>v x <\<^sub>v b\<^sub>2
x \<in> carrier_vec n

goal (1 subgoal):
 1. 0\<^sub>m nr\<^sub>2 n *\<^sub>v 0\<^sub>v n <\<^sub>v b\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A\<^sub>2 *\<^sub>v 0\<^sub>v n <\<^sub>v b\<^sub>2

goal (3 subgoals):
 1. 0\<^sub>v n \<in> carrier_vec n
 2. 0\<^sub>v n \<in> indexed_Ints_vec I
 3. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
show "?x \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0\<^sub>v n \<in> carrier_vec n

goal (2 subgoals):
 1. 0\<^sub>v n \<in> indexed_Ints_vec I
 2. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
show "?x \<in> indexed_Ints_vec I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n \<in> indexed_Ints_vec I
[PROOF STEP]
unfolding indexed_Ints_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n \<in> {x. \<forall>i<dim_vec x. i \<in> I \<longrightarrow> x $ i \<in> \<int>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0\<^sub>v n \<in> indexed_Ints_vec I

goal (1 subgoal):
 1. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from nr1 nr2 non_degenerate
[PROOF STATE]
proof (chain)
picking this:
nr\<^sub>1 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd
nr\<^sub>2 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd
nr\<^sub>1 \<noteq> 0 \<or> nr\<^sub>2 \<noteq> 0 \<or> 0 \<le> Bnd
[PROOF STEP]
have Bnd: "Bnd \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
nr\<^sub>1 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd
nr\<^sub>2 \<noteq> 0 \<Longrightarrow> 0 \<le> Bnd
nr\<^sub>1 \<noteq> 0 \<or> nr\<^sub>2 \<noteq> 0 \<or> 0 \<le> Bnd

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

goal (1 subgoal):
 1. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from is_det_bound_ge_zero[OF db Bnd]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> db ?n Bnd
[PROOF STEP]
have "db n Bnd \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> db ?n Bnd

goal (1 subgoal):
 1. 0 \<le> db n Bnd
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 \<le> db n Bnd

goal (1 subgoal):
 1. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
hence "?oi (of_nat (n + 1) * db n Bnd) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> db n Bnd

goal (1 subgoal):
 1. (0::'a) \<le> of_int (int (n + 1) * db n Bnd)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> of_int (int (n + 1) * db n Bnd)

goal (1 subgoal):
 1. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
thus "?x \<in> Bounded_vec (?oi (of_nat (n + 1) * db n Bnd))"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> of_int (int (n + 1) * db n Bnd)

goal (1 subgoal):
 1. 0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
by (auto simp: Bounded_vec_def)
[PROOF STATE]
proof (state)
this:
0\<^sub>v n \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Bounded_vec_of_int: assumes "v \<in> Bounded_vec bnd"
  shows "(map_vec of_int v :: 'a vec) \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int bnd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom v \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int bnd)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> Bounded_vec bnd

goal (1 subgoal):
 1. of_int_hom.vec_hom v \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int bnd)
[PROOF STEP]
apply (simp add: Ints_vec_vec_set Bounded_vec_vec_set Ints_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set\<^sub>v v. \<bar>x\<bar> \<le> bnd \<Longrightarrow> of_int ` set\<^sub>v v \<subseteq> range of_int \<and> (\<forall>x\<in>set\<^sub>v v. \<bar>of_int x\<bar> \<le> of_int bnd)
[PROOF STEP]
apply (intro conjI, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set\<^sub>v v. \<bar>x\<bar> \<le> bnd \<Longrightarrow> \<forall>x\<in>set\<^sub>v v. \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>set\<^sub>v v. \<bar>x\<bar> \<le> bnd; x \<in> set\<^sub>v v\<rbrakk> \<Longrightarrow> \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set\<^sub>v v. \<bar>x\<bar> \<le> bnd; x \<in> set\<^sub>v v\<rbrakk> \<Longrightarrow> \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
apply (elim ballE[of _ _ x], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set\<^sub>v v; \<bar>x\<bar> \<le> bnd\<rbrakk> \<Longrightarrow> \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
by (metis of_int_abs of_int_le_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Bounded_mat_of_int: assumes "A \<in> Bounded_mat bnd"
  shows "(map_mat of_int A :: 'a mat) \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int bnd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.mat_hom A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int bnd)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> Bounded_mat bnd

goal (1 subgoal):
 1. of_int_hom.mat_hom A \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int bnd)
[PROOF STEP]
apply (simp add: Ints_mat_elements_mat Bounded_mat_elements_mat Ints_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>elements_mat A. \<bar>x\<bar> \<le> bnd \<Longrightarrow> of_int ` elements_mat A \<subseteq> range of_int \<and> (\<forall>x\<in>elements_mat A. \<bar>of_int x\<bar> \<le> of_int bnd)
[PROOF STEP]
apply (intro conjI, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>elements_mat A. \<bar>x\<bar> \<le> bnd \<Longrightarrow> \<forall>x\<in>elements_mat A. \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>elements_mat A. \<bar>x\<bar> \<le> bnd; x \<in> elements_mat A\<rbrakk> \<Longrightarrow> \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>elements_mat A. \<bar>x\<bar> \<le> bnd; x \<in> elements_mat A\<rbrakk> \<Longrightarrow> \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
apply (elim ballE[of _ _ x], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> elements_mat A; \<bar>x\<bar> \<le> bnd\<rbrakk> \<Longrightarrow> \<bar>of_int x\<bar> \<le> of_int bnd
[PROOF STEP]
by (metis of_int_abs of_int_le_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma small_mixed_integer_solution_int_mat: fixes x :: "'a vec"
  assumes db: "is_det_bound db"
    and A1: "A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n"
    and A2: "A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n"
    and b1: "b\<^sub>1 \<in> carrier_vec nr\<^sub>1"
    and b2: "b\<^sub>2 \<in> carrier_vec nr\<^sub>2"
    and A1Bnd: "A\<^sub>1 \<in> Bounded_mat Bnd"
    and b1Bnd: "b\<^sub>1 \<in> Bounded_vec Bnd"
    and A2Bnd: "A\<^sub>2 \<in> Bounded_mat Bnd"
    and b2Bnd: "b\<^sub>2 \<in> Bounded_vec Bnd"
    and x: "x \<in> carrier_vec n"
    and xI: "x \<in> indexed_Ints_vec I"
    and sol_nonstrict: "map_mat of_int A\<^sub>1 *\<^sub>v x \<le> map_vec of_int b\<^sub>1"
    and sol_strict: "map_mat of_int A\<^sub>2 *\<^sub>v x <\<^sub>v map_vec of_int b\<^sub>2"
    and non_degenerate: "nr\<^sub>1 \<noteq> 0 \<or> nr\<^sub>2 \<noteq> 0 \<or> Bnd \<ge> 0"
  shows "\<exists> x :: 'a vec.
  x \<in> carrier_vec n \<and>
  x \<in> indexed_Ints_vec I \<and>
  map_mat of_int A\<^sub>1 *\<^sub>v x \<le> map_vec of_int b\<^sub>1 \<and>
  map_mat of_int A\<^sub>2 *\<^sub>v x <\<^sub>v map_vec of_int b\<^sub>2 \<and>
  x \<in> Bounded_vec (of_int (of_nat (n+1) * db n Bnd))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?oi = "of_int :: int \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?A1 = "map_mat ?oi A\<^sub>1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?A2 = "map_mat ?oi A\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?b1 = "map_vec ?oi b\<^sub>1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?b2 = "map_vec ?oi b\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
let ?Bnd = "?oi Bnd"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
[PROOF STEP]
have A1': "?A1 \<in> carrier_mat nr\<^sub>1 n"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n

goal (1 subgoal):
 1. of_int_hom.mat_hom A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_hom.mat_hom A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
[PROOF STEP]
have A2': "?A2 \<in> carrier_mat nr\<^sub>2 n"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. of_int_hom.mat_hom A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_hom.mat_hom A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from b1
[PROOF STATE]
proof (chain)
picking this:
b\<^sub>1 \<in> carrier_vec nr\<^sub>1
[PROOF STEP]
have b1': "?b1 \<in> carrier_vec nr\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
b\<^sub>1 \<in> carrier_vec nr\<^sub>1

goal (1 subgoal):
 1. of_int_hom.vec_hom b\<^sub>1 \<in> carrier_vec nr\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_hom.vec_hom b\<^sub>1 \<in> carrier_vec nr\<^sub>1

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from b2
[PROOF STATE]
proof (chain)
picking this:
b\<^sub>2 \<in> carrier_vec nr\<^sub>2
[PROOF STEP]
have b2': "?b2 \<in> carrier_vec nr\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
b\<^sub>2 \<in> carrier_vec nr\<^sub>2

goal (1 subgoal):
 1. of_int_hom.vec_hom b\<^sub>2 \<in> carrier_vec nr\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_hom.vec_hom b\<^sub>2 \<in> carrier_vec nr\<^sub>2

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
from small_mixed_integer_solution[OF db A1' A2' b1' b2'
     Bounded_mat_of_int[OF A1Bnd] Bounded_vec_of_int[OF b1Bnd]
     Bounded_mat_of_int[OF A2Bnd] Bounded_vec_of_int[OF b2Bnd]
     x xI sol_nonstrict sol_strict non_degenerate]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> indexed_Ints_vec I \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (of_int (int (n + 1) * db n Bnd))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_int_hom_le: "(of_int_hom.vec_hom v :: 'a :: linordered_field vec) \<le> of_int_hom.vec_hom w \<longleftrightarrow> v \<le> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_hom.vec_hom v \<le> of_int_hom.vec_hom w) = (v \<le> w)
[PROOF STEP]
unfolding less_eq_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dim_vec (of_int_hom.vec_hom v) = dim_vec (of_int_hom.vec_hom w) \<and> (\<forall>i<dim_vec (of_int_hom.vec_hom w). of_int_hom.vec_hom v $ i \<le> of_int_hom.vec_hom w $ i)) = (dim_vec v = dim_vec w \<and> (\<forall>i<dim_vec w. v $ i \<le> w $ i))
[PROOF STEP]
by auto


[STATEMENT]
lemma of_int_hom_less: "(of_int_hom.vec_hom v :: 'a :: linordered_field vec) <\<^sub>v of_int_hom.vec_hom w \<longleftrightarrow> v <\<^sub>v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_hom.vec_hom v <\<^sub>v of_int_hom.vec_hom w) = (v <\<^sub>v w)
[PROOF STEP]
unfolding less_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dim_vec (of_int_hom.vec_hom v) = dim_vec (of_int_hom.vec_hom w) \<and> (\<forall>i<dim_vec (of_int_hom.vec_hom w). of_int_hom.vec_hom v $ i < of_int_hom.vec_hom w $ i)) = (dim_vec v = dim_vec w \<and> (\<forall>i<dim_vec w. v $ i < w $ i))
[PROOF STEP]
by auto


[STATEMENT]
lemma Ints_vec_to_int_vec: assumes "v \<in> \<int>\<^sub>v"
  shows "\<exists> w. v = map_vec of_int w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>w. v = of_int_hom.vec_hom w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>w. v = of_int_hom.vec_hom w
[PROOF STEP]
have "\<forall> i. \<exists> x. i < dim_vec v \<longrightarrow> v $ i = of_int x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<exists>x. i < dim_vec v \<longrightarrow> v $ i = of_int x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> \<int>\<^sub>v

goal (1 subgoal):
 1. \<forall>i. \<exists>x. i < dim_vec v \<longrightarrow> v $ i = of_int x
[PROOF STEP]
unfolding Ints_vec_def Ints_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {x. \<forall>i<dim_vec x. x $ i \<in> range of_int}

goal (1 subgoal):
 1. \<forall>i. \<exists>x. i < dim_vec v \<longrightarrow> v $ i = of_int x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>x. i < dim_vec v \<longrightarrow> v $ i = of_int x

goal (1 subgoal):
 1. \<exists>w. v = of_int_hom.vec_hom w
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x<dim_vec v. v $ x = of_int (f x)
[PROOF STEP]
obtain x where "\<And> i. i < dim_vec v \<Longrightarrow> v $ i = of_int (x i)"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x<dim_vec v. v $ x = of_int (f x)

goal (1 subgoal):
 1. (\<And>x. (\<And>i. i < dim_vec v \<Longrightarrow> v $ i = of_int (x i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < dim_vec v \<Longrightarrow> v $ ?i = of_int (x ?i)

goal (1 subgoal):
 1. \<exists>w. v = of_int_hom.vec_hom w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?i < dim_vec v \<Longrightarrow> v $ ?i = of_int (x ?i)

goal (1 subgoal):
 1. \<exists>w. v = of_int_hom.vec_hom w
[PROOF STEP]
by (intro exI[of _ "vec (dim_vec v) x"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>w. v = of_int_hom.vec_hom w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_integer_solution: fixes A\<^sub>1 :: "int mat"
  assumes db: "is_det_bound db"
    and A1: "A\<^sub>1 \<in> carrier_mat nr\<^sub>1 n"
    and A2: "A\<^sub>2 \<in> carrier_mat nr\<^sub>2 n"
    and b1: "b\<^sub>1 \<in> carrier_vec nr\<^sub>1"
    and b2: "b\<^sub>2 \<in> carrier_vec nr\<^sub>2"
    and A1Bnd: "A\<^sub>1 \<in> Bounded_mat Bnd"
    and b1Bnd: "b\<^sub>1 \<in> Bounded_vec Bnd"
    and A2Bnd: "A\<^sub>2 \<in> Bounded_mat Bnd"
    and b2Bnd: "b\<^sub>2 \<in> Bounded_vec Bnd"
    and x: "x \<in> carrier_vec n"
    and sol_nonstrict: "A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1"
    and sol_strict: "A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2"
    and non_degenerate: "nr\<^sub>1 \<noteq> 0 \<or> nr\<^sub>2 \<noteq> 0 \<or> Bnd \<ge> 0"
  shows "\<exists> x.
    x \<in> carrier_vec n \<and>
    A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and>
    A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and>
    x \<in> Bounded_vec (of_nat (n+1) * db n Bnd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
let ?oi = rat_of_int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
let ?x = "map_vec ?oi x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
let ?oiM = "map_mat ?oi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
let ?oiv = "map_vec ?oi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier_vec n
[PROOF STEP]
have xx: "?x \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec n

goal (1 subgoal):
 1. of_int_hom.vec_hom x \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_hom.vec_hom x \<in> carrier_vec n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
have Int: "?x \<in> indexed_Ints_vec UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom x \<in> indexed_Ints_vec UNIV
[PROOF STEP]
unfolding indexed_Ints_vec_def Ints_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_hom.vec_hom x \<in> {x. \<forall>i<dim_vec x. i \<in> UNIV \<longrightarrow> x $ i \<in> range rat_of_int}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int_hom.vec_hom x \<in> indexed_Ints_vec UNIV

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
interpret gram_schmidt_floor n "TYPE(rat)"
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
from
    small_mixed_integer_solution_int_mat[OF db A1 A2 b1 b2 A1Bnd b1Bnd A2Bnd b2Bnd xx Int
      _ _ non_degenerate,
      folded of_int_hom.mult_mat_vec_hom[OF A1 x] of_int_hom.mult_mat_vec_hom[OF A2 x],
      unfolded of_int_hom_less of_int_hom_le, OF sol_nonstrict sol_strict, folded indexed_Ints_vec_UNIV]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> \<int>\<^sub>v \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (rat_of_int (int (n + 1) * db n Bnd))
[PROOF STEP]
obtain x where
    x: "x \<in> carrier_vec n" and
    xI: "x \<in> \<int>\<^sub>v" and
    le: "?oiM A\<^sub>1 *\<^sub>v x \<le> ?oiv b\<^sub>1" and
    less: "?oiM A\<^sub>2 *\<^sub>v x <\<^sub>v ?oiv b\<^sub>2" and
    Bnd: "x \<in> Bounded_vec (?oi (int (n + 1) * db n Bnd))"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> carrier_vec n \<and> x \<in> \<int>\<^sub>v \<and> of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1 \<and> of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2 \<and> x \<in> Bounded_vec (rat_of_int (int (n + 1) * db n Bnd))

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> carrier_vec n; x \<in> \<int>\<^sub>v; of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1; of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2; x \<in> Bounded_vec (rat_of_int (int (n + 1) * db n Bnd))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec n
x \<in> \<int>\<^sub>v
of_int_hom.mat_hom A\<^sub>1 *\<^sub>v x \<le> of_int_hom.vec_hom b\<^sub>1
of_int_hom.mat_hom A\<^sub>2 *\<^sub>v x <\<^sub>v of_int_hom.vec_hom b\<^sub>2
x \<in> Bounded_vec (rat_of_int (int (n + 1) * db n Bnd))

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
from Ints_vec_to_int_vec[OF xI]
[PROOF STATE]
proof (chain)
picking this:
\<exists>w. x = of_int_hom.vec_hom w
[PROOF STEP]
obtain xI where xI: "x = ?oiv xI"
[PROOF STATE]
proof (prove)
using this:
\<exists>w. x = of_int_hom.vec_hom w

goal (1 subgoal):
 1. (\<And>xI. x = of_int_hom.vec_hom xI \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = of_int_hom.vec_hom xI

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
from x[unfolded xI]
[PROOF STATE]
proof (chain)
picking this:
of_int_hom.vec_hom xI \<in> carrier_vec n
[PROOF STEP]
have x: "xI \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
of_int_hom.vec_hom xI \<in> carrier_vec n

goal (1 subgoal):
 1. xI \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xI \<in> carrier_vec n

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
from le[unfolded xI, folded of_int_hom.mult_mat_vec_hom[OF A1 x], unfolded of_int_hom_le]
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>1 *\<^sub>v xI \<le> b\<^sub>1
[PROOF STEP]
have le: "A\<^sub>1 *\<^sub>v xI \<le> b\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 *\<^sub>v xI \<le> b\<^sub>1

goal (1 subgoal):
 1. A\<^sub>1 *\<^sub>v xI \<le> b\<^sub>1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A\<^sub>1 *\<^sub>v xI \<le> b\<^sub>1

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
from less[unfolded xI, folded of_int_hom.mult_mat_vec_hom[OF A2 x], unfolded of_int_hom_less]
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>2 *\<^sub>v xI <\<^sub>v b\<^sub>2
[PROOF STEP]
have less: "A\<^sub>2 *\<^sub>v xI <\<^sub>v b\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 *\<^sub>v xI <\<^sub>v b\<^sub>2

goal (1 subgoal):
 1. A\<^sub>2 *\<^sub>v xI <\<^sub>v b\<^sub>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A\<^sub>2 *\<^sub>v xI <\<^sub>v b\<^sub>2

goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
proof (intro exI[of _ xI] conjI x le less)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xI \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
show "xI \<in> Bounded_vec (int (n + 1) * db n Bnd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xI \<in> Bounded_vec (int (n + 1) * db n Bnd)
[PROOF STEP]
unfolding Bounded_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xI \<in> {x. \<forall>i<dim_vec x. \<bar>x $ i\<bar> \<le> int (n + 1) * db n Bnd}
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec xI \<Longrightarrow> \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec xI \<Longrightarrow> \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
assume i: "i < dim_vec xI"
[PROOF STATE]
proof (state)
this:
i < dim_vec xI

goal (1 subgoal):
 1. \<And>i. i < dim_vec xI \<Longrightarrow> \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
with Bnd[unfolded Bounded_vec_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {x. \<forall>i<dim_vec x. \<bar>x $ i\<bar> \<le> rat_of_int (int (n + 1) * db n Bnd)}
i < dim_vec xI
[PROOF STEP]
have "\<bar>x $ i\<bar> \<le> ?oi (int (n + 1) * db n Bnd)"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. \<forall>i<dim_vec x. \<bar>x $ i\<bar> \<le> rat_of_int (int (n + 1) * db n Bnd)}
i < dim_vec xI

goal (1 subgoal):
 1. \<bar>x $ i\<bar> \<le> rat_of_int (int (n + 1) * db n Bnd)
[PROOF STEP]
by (auto simp: xI)
[PROOF STATE]
proof (state)
this:
\<bar>x $ i\<bar> \<le> rat_of_int (int (n + 1) * db n Bnd)

goal (1 subgoal):
 1. \<And>i. i < dim_vec xI \<Longrightarrow> \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x $ i\<bar> \<le> rat_of_int (int (n + 1) * db n Bnd)

goal (1 subgoal):
 1. \<And>i. i < dim_vec xI \<Longrightarrow> \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
have "\<bar>x $ i\<bar> = ?oi (\<bar>xI $ i\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x $ i\<bar> = rat_of_int \<bar>xI $ i\<bar>
[PROOF STEP]
unfolding xI
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>of_int_hom.vec_hom xI $ i\<bar> = rat_of_int \<bar>xI $ i\<bar>
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < dim_vec xI

goal (1 subgoal):
 1. \<bar>of_int_hom.vec_hom xI $ i\<bar> = rat_of_int \<bar>xI $ i\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>x $ i\<bar> = rat_of_int \<bar>xI $ i\<bar>

goal (1 subgoal):
 1. \<And>i. i < dim_vec xI \<Longrightarrow> \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rat_of_int \<bar>xI $ i\<bar> \<le> rat_of_int (int (n + 1) * db n Bnd)
[PROOF STEP]
show "\<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd"
[PROOF STATE]
proof (prove)
using this:
rat_of_int \<bar>xI $ i\<bar> \<le> rat_of_int (int (n + 1) * db n Bnd)

goal (1 subgoal):
 1. \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
unfolding of_int_le_iff
[PROOF STATE]
proof (prove)
using this:
\<bar>xI $ i\<bar> \<le> int (n + 1) * db n Bnd

goal (1 subgoal):
 1. \<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>xI $ i\<bar> \<le> (1 + int n) * db n Bnd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xI \<in> Bounded_vec (int (n + 1) * db n Bnd)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> carrier_vec n \<and> A\<^sub>1 *\<^sub>v x \<le> b\<^sub>1 \<and> A\<^sub>2 *\<^sub>v x <\<^sub>v b\<^sub>2 \<and> x \<in> Bounded_vec (int (n + 1) * db n Bnd)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_suc_sem: \<open>step (n,\<sigma>) = (suc n \<sigma>, sem n \<sigma>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.step (n, \<sigma>) = (suc n \<sigma>, sem n \<sigma>)
[PROOF STEP]
unfolding suc_def sem_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.step (n, \<sigma>) = (fst (local.step (n, \<sigma>)), snd (local.step (n, \<sigma>)))
[PROOF STEP]
by auto


[STATEMENT]
lemma icd_uniq: assumes  \<open>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> \<open> m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'\<close> shows \<open>n = n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = n'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = n'
[PROOF STEP]
fix n n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = n'
[PROOF STEP]
assume *: \<open>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> \<open> m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'\<close> \<open>n < n'\<close>
[PROOF STATE]
proof (state)
this:
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
n < n'

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
have \<open>n'<m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' < m
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
n < n'

goal (1 subgoal):
 1. n' < m
[PROOF STEP]
unfolding is_icdi_def is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> (is_path \<pi> \<and> n < m \<and> \<pi> m \<noteq> local.return \<and> (\<forall>j\<in>{n..m}. \<pi> j \<noteq> ipd (\<pi> n))) \<and> (\<forall>ma\<in>{n<..<m}. \<not> (is_path \<pi> \<and> ma < m \<and> \<pi> m \<noteq> local.return \<and> (\<forall>j\<in>{ma..m}. \<pi> j \<noteq> ipd (\<pi> ma))))
is_path \<pi> \<and> (is_path \<pi> \<and> n' < m \<and> \<pi> m \<noteq> local.return \<and> (\<forall>j\<in>{n'..m}. \<pi> j \<noteq> ipd (\<pi> n'))) \<and> (\<forall>ma\<in>{n'<..<m}. \<not> (is_path \<pi> \<and> ma < m \<and> \<pi> m \<noteq> local.return \<and> (\<forall>j\<in>{ma..m}. \<pi> j \<noteq> ipd (\<pi> ma))))
n < n'

goal (1 subgoal):
 1. n' < m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n' < m

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
hence \<open>\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (prove)
using this:
n' < m

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
n' < m
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
n < n'

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
[PROOF STEP]
unfolding is_icdi_def
[PROOF STATE]
proof (prove)
using this:
n' < m
is_path \<pi> \<and> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n \<and> (\<forall>ma\<in>{n<..<m}. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> ma)
is_path \<pi> \<and> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<and> (\<forall>ma\<in>{n'<..<m}. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> ma)
n < n'

goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
with *(2)
[PROOF STATE]
proof (chain)
picking this:
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
[PROOF STEP]
have \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'
\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_icdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n' \<and> (\<forall>ma\<in>{n'<..<m}. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> ma)
\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?na3; m icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?n'a3; ?na3 < ?n'a3\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?na3; m icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?n'a3; ?na3 < ?n'a3\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?na3; m icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?n'a3; ?na3 < ?n'a3\<rbrakk> \<Longrightarrow> False
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
by (metis linorder_neqE_nat)
[PROOF STATE]
proof (state)
this:
n = n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma option_neq_cases: assumes \<open>x \<noteq> y\<close> obtains (none1) a where \<open>x = None\<close> \<open>y = Some a\<close> | (none2) a where \<open>x = Some a\<close> \<open>y = None\<close> | (some) a b where \<open>x = Some a\<close> \<open>y = Some b\<close> \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. \<lbrakk>x = None; y = Some a\<rbrakk> \<Longrightarrow> thesis; \<And>a. \<lbrakk>x = Some a; y = None\<rbrakk> \<Longrightarrow> thesis; \<And>a b. \<lbrakk>x = Some a; y = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. \<lbrakk>\<And>a. \<lbrakk>x = None; y = Some a\<rbrakk> \<Longrightarrow> thesis; \<And>a. \<lbrakk>x = Some a; y = None\<rbrakk> \<Longrightarrow> thesis; \<And>a b. \<lbrakk>x = Some a; y = Some b; a \<noteq> b\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by fastforce


[STATEMENT]
lemma mod_bound_instance: assumes \<open>j < (i::nat)\<close> obtains j' where \<open>k < j'\<close> and \<open>j' mod i = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>k < j'; j' mod i = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>k < j'; j' mod i = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>k < Suc k * i + j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < Suc k * i + j
[PROOF STEP]
using assms less_imp_Suc_add
[PROOF STATE]
proof (prove)
using this:
j < i
?m < ?n \<Longrightarrow> \<exists>k. ?n = Suc (?m + k)

goal (1 subgoal):
 1. k < Suc k * i + j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
k < Suc k * i + j

goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>k < j'; j' mod i = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < Suc k * i + j

goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>k < j'; j' mod i = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>(Suc k * i + j) mod i = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Suc k * i + j) mod i = j
[PROOF STEP]
by (metis assms mod_less mod_mult_self3)
[PROOF STATE]
proof (state)
this:
(Suc k * i + j) mod i = j

goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>k < j'; j' mod i = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < Suc k * i + j
(Suc k * i + j) mod i = j
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
k < Suc k * i + j
(Suc k * i + j) mod i = j

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k < Suc k * i + j
(Suc k * i + j) mod i = j
\<lbrakk>k < ?j'; ?j' mod i = j\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_neq_prefix_cases: assumes \<open>ls \<noteq> ls'\<close> and \<open>ls \<noteq> Nil\<close> and \<open>ls' \<noteq> Nil\<close>
  obtains (diverge) xs x x' ys ys' where \<open>ls = xs@[x]@ys\<close> \<open>ls' = xs@[x']@ys'\<close> \<open>x \<noteq> x'\<close> |
   (prefix1) xs where \<open>ls = ls'@xs\<close> and \<open>xs \<noteq> Nil\<close> |
   (prefix2) xs where \<open>ls@xs = ls'\<close> and \<open>xs \<noteq> Nil\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>ls = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ls \<noteq> ls'
ls \<noteq> []
ls' \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>ls = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof (induct \<open>length ls\<close> arbitrary: \<open>ls\<close> \<open>ls'\<close> rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ls ls'. \<lbrakk>\<And>lsa ls'. \<lbrakk>length lsa < length ls; \<And>xs x ys x' ys'. \<lbrakk>lsa = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>lsa = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>lsa @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; lsa \<noteq> ls'; lsa \<noteq> []; ls' \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs x ys x' ys'. \<lbrakk>ls = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; ls \<noteq> ls'; ls \<noteq> []; ls' \<noteq> []\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (less ls ls')
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?ls < length ls; \<And>xs x ys x' ys'. \<lbrakk>?ls = xs @ [x] @ ys; ?ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>?ls = ?ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>?ls @ xs = ?ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; ?ls \<noteq> ?ls'; ?ls \<noteq> []; ?ls' \<noteq> []\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>ls = ?xs @ [?x] @ ?ys; ls' = ?xs @ [?x'] @ ?ys'; ?x \<noteq> ?x'\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>ls = ls' @ ?xs; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>ls @ ?xs = ls'; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis
ls \<noteq> ls'
ls \<noteq> []
ls' \<noteq> []

goal (1 subgoal):
 1. \<And>ls ls'. \<lbrakk>\<And>lsa ls'. \<lbrakk>length lsa < length ls; \<And>xs x ys x' ys'. \<lbrakk>lsa = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>lsa = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>lsa @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; lsa \<noteq> ls'; lsa \<noteq> []; ls' \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs x ys x' ys'. \<lbrakk>ls = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; ls \<noteq> ls'; ls \<noteq> []; ls' \<noteq> []\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain z zs z' zs' where
  lz: \<open>ls = z#zs\<close> \<open>ls' = z'#zs'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z zs z' zs'. \<lbrakk>ls = z # zs; ls' = z' # zs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis list.exhaust less(6,7))
[PROOF STATE]
proof (state)
this:
ls = z # zs
ls' = z' # zs'

goal (1 subgoal):
 1. \<And>ls ls'. \<lbrakk>\<And>lsa ls'. \<lbrakk>length lsa < length ls; \<And>xs x ys x' ys'. \<lbrakk>lsa = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>lsa = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>lsa @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; lsa \<noteq> ls'; lsa \<noteq> []; ls' \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs x ys x' ys'. \<lbrakk>ls = xs @ [x] @ ys; ls' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls = ls' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>ls @ xs = ls'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; ls \<noteq> ls'; ls \<noteq> []; ls' \<noteq> []\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
assume zz: \<open>z = z'\<close>
[PROOF STATE]
proof (state)
this:
z = z'

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
hence zsz: \<open>zs \<noteq> zs'\<close>
[PROOF STATE]
proof (prove)
using this:
z = z'

goal (1 subgoal):
 1. zs \<noteq> zs'
[PROOF STEP]
using less(5) lz
[PROOF STATE]
proof (prove)
using this:
z = z'
ls \<noteq> ls'
ls = z # zs
ls' = z' # zs'

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
have lenz: \<open>length zs < length ls\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length zs < length ls
[PROOF STEP]
using lz
[PROOF STATE]
proof (prove)
using this:
ls = z # zs
ls' = z' # zs'

goal (1 subgoal):
 1. length zs < length ls
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length zs < length ls

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof(cases \<open>zs = Nil\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zs = [] \<Longrightarrow> thesis
 2. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
assume zs: \<open>zs = Nil\<close>
[PROOF STATE]
proof (state)
this:
zs = []

goal (2 subgoals):
 1. zs = [] \<Longrightarrow> thesis
 2. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>zs' \<noteq> Nil\<close>
[PROOF STATE]
proof (prove)
using this:
zs = []

goal (1 subgoal):
 1. zs' \<noteq> []
[PROOF STEP]
using zsz
[PROOF STATE]
proof (prove)
using this:
zs = []
zs \<noteq> zs'

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

goal (2 subgoals):
 1. zs = [] \<Longrightarrow> thesis
 2. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
zs' \<noteq> []

goal (2 subgoals):
 1. zs = [] \<Longrightarrow> thesis
 2. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
have \<open>ls@zs' = ls'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls @ zs' = ls'
[PROOF STEP]
using zs lz zz
[PROOF STATE]
proof (prove)
using this:
zs = []
ls = z # zs
ls' = z' # zs'
z = z'

goal (1 subgoal):
 1. ls @ zs' = ls'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls @ zs' = ls'

goal (2 subgoals):
 1. zs = [] \<Longrightarrow> thesis
 2. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
zs' \<noteq> []
ls @ zs' = ls'
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
zs' \<noteq> []
ls @ zs' = ls'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using less(4)
[PROOF STATE]
proof (prove)
using this:
zs' \<noteq> []
ls @ zs' = ls'
\<lbrakk>ls @ ?xs = ls'; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
assume zs: \<open>zs \<noteq> Nil\<close>
[PROOF STATE]
proof (state)
this:
zs \<noteq> []

goal (1 subgoal):
 1. zs \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases \<open>zs' = Nil\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. zs' = [] \<Longrightarrow> thesis
 2. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>zs' = Nil\<close>
[PROOF STATE]
proof (state)
this:
zs' = []

goal (2 subgoals):
 1. zs' = [] \<Longrightarrow> thesis
 2. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>ls = ls'@zs\<close>
[PROOF STATE]
proof (prove)
using this:
zs' = []

goal (1 subgoal):
 1. ls = ls' @ zs
[PROOF STEP]
using lz zz
[PROOF STATE]
proof (prove)
using this:
zs' = []
ls = z # zs
ls' = z' # zs'
z = z'

goal (1 subgoal):
 1. ls = ls' @ zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = ls' @ zs

goal (2 subgoals):
 1. zs' = [] \<Longrightarrow> thesis
 2. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
ls = ls' @ zs

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using zs less(3)
[PROOF STATE]
proof (prove)
using this:
ls = ls' @ zs
zs \<noteq> []
\<lbrakk>ls = ls' @ ?xs; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
assume zs': \<open>zs' \<noteq> Nil\<close>
[PROOF STATE]
proof (state)
this:
zs' \<noteq> []

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
zs' \<noteq> []

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
fix xs x ys x' ys'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>zs = xs @ [x] @ ys\<close> \<open>zs' = xs @ [x'] @ ys'\<close> and xx: \<open>x \<noteq> x'\<close>
[PROOF STATE]
proof (state)
this:
zs = xs @ [x] @ ys
zs' = xs @ [x'] @ ys'
x \<noteq> x'

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>ls = (z#xs) @ [x] @ ys\<close> \<open>ls' = (z#xs) @ [x'] @ ys'\<close>
[PROOF STATE]
proof (prove)
using this:
zs = xs @ [x] @ ys
zs' = xs @ [x'] @ ys'
x \<noteq> x'

goal (1 subgoal):
 1. ls = (z # xs) @ [x] @ ys &&& ls' = (z # xs) @ [x'] @ ys'
[PROOF STEP]
using lz zz
[PROOF STATE]
proof (prove)
using this:
zs = xs @ [x] @ ys
zs' = xs @ [x'] @ ys'
x \<noteq> x'
ls = z # zs
ls' = z' # zs'
z = z'

goal (1 subgoal):
 1. ls = (z # xs) @ [x] @ ys &&& ls' = (z # xs) @ [x'] @ ys'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = (z # xs) @ [x] @ ys
ls' = (z # xs) @ [x'] @ ys'

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
ls = (z # xs) @ [x] @ ys
ls' = (z # xs) @ [x'] @ ys'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using less(2) xx
[PROOF STATE]
proof (prove)
using this:
ls = (z # xs) @ [x] @ ys
ls' = (z # xs) @ [x'] @ ys'
\<lbrakk>ls = ?xs @ [?x] @ ?ys; ls' = ?xs @ [?x'] @ ?ys'; ?x \<noteq> ?x'\<rbrakk> \<Longrightarrow> thesis
x \<noteq> x'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs = ?xs2 @ [?x2] @ ?ys2; zs' = ?xs2 @ [?x'2] @ ?ys'2; ?x2 \<noteq> ?x'2\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs = ?xs2 @ [?x2] @ ?ys2; zs' = ?xs2 @ [?x'2] @ ?ys'2; ?x2 \<noteq> ?x'2\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs = ?xs2 @ [?x2] @ ?ys2; zs' = ?xs2 @ [?x'2] @ ?ys'2; ?x2 \<noteq> ?x'2\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>zs = zs' @ xs\<close> and xs: \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (state)
this:
zs = zs' @ xs
xs \<noteq> []

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>ls = ls' @ xs\<close>
[PROOF STATE]
proof (prove)
using this:
zs = zs' @ xs
xs \<noteq> []

goal (1 subgoal):
 1. ls = ls' @ xs
[PROOF STEP]
using lz zz
[PROOF STATE]
proof (prove)
using this:
zs = zs' @ xs
xs \<noteq> []
ls = z # zs
ls' = z' # zs'
z = z'

goal (1 subgoal):
 1. ls = ls' @ xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = ls' @ xs

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
ls = ls' @ xs

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using xs less(3)
[PROOF STATE]
proof (prove)
using this:
ls = ls' @ xs
xs \<noteq> []
\<lbrakk>ls = ls' @ ?xs; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs = zs' @ ?xs2; ?xs2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
note ** = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs = zs' @ ?xs2; ?xs2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs = zs' @ ?xs2; ?xs2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>zs@xs = zs'\<close> and xs: \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (state)
this:
zs @ xs = zs'
xs \<noteq> []

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>ls@xs = ls'\<close>
[PROOF STATE]
proof (prove)
using this:
zs @ xs = zs'
xs \<noteq> []

goal (1 subgoal):
 1. ls @ xs = ls'
[PROOF STEP]
using lz zz
[PROOF STATE]
proof (prove)
using this:
zs @ xs = zs'
xs \<noteq> []
ls = z # zs
ls' = z' # zs'
z = z'

goal (1 subgoal):
 1. ls @ xs = ls'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls @ xs = ls'

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
ls @ xs = ls'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using xs less(4)
[PROOF STATE]
proof (prove)
using this:
ls @ xs = ls'
xs \<noteq> []
\<lbrakk>ls @ ?xs = ls'; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs @ ?xs2 = zs'; ?xs2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
note *** = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>zs @ ?xs2 = zs'; ?xs2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
have \<open>(\<And>xs x ys x' ys'. zs = xs @ [x] @ ys \<Longrightarrow> zs' = xs @ [x'] @ ys' \<Longrightarrow> x \<noteq> x' \<Longrightarrow> thesis) \<Longrightarrow>
              (\<And>xs. zs = zs' @ xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> thesis) \<Longrightarrow>
              (\<And>xs. zs @ xs = zs' \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>zs = xs @ [x] @ ys; zs' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs = zs' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs @ xs = zs'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using less(1)[OF lenz _ _ _ zsz zs zs' ]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>zs = xs @ [x] @ ys; zs' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs = zs' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs @ xs = zs'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>zs = xs @ [x] @ ys; zs' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs = zs' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs @ xs = zs'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>zs = xs @ [x] @ ys; zs' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs = zs' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs @ xs = zs'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. zs' \<noteq> [] \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>zs = xs @ [x] @ ys; zs' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs = zs' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs @ xs = zs'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using * ** ***
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xs x ys x' ys'. \<lbrakk>zs = xs @ [x] @ ys; zs' = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs = zs' @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis; \<And>xs. \<lbrakk>zs @ xs = zs'; xs \<noteq> []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>zs = ?xs2 @ [?x2] @ ?ys2; zs' = ?xs2 @ [?x'2] @ ?ys'2; ?x2 \<noteq> ?x'2\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>zs = zs' @ ?xs2; ?xs2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>zs @ ?xs2 = zs'; ?xs2 \<noteq> []\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. z \<noteq> z' \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> z' \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>z \<noteq> z'\<close>
[PROOF STATE]
proof (state)
this:
z \<noteq> z'

goal (1 subgoal):
 1. z \<noteq> z' \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z \<noteq> z'

goal (1 subgoal):
 1. z \<noteq> z' \<Longrightarrow> thesis
[PROOF STEP]
have \<open>ls = []@[z]@zs\<close> \<open>ls' = []@[z']@zs'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls = [] @ [z] @ zs &&& ls' = [] @ [z'] @ zs'
[PROOF STEP]
using lz
[PROOF STATE]
proof (prove)
using this:
ls = z # zs
ls' = z' # zs'

goal (1 subgoal):
 1. ls = [] @ [z] @ zs &&& ls' = [] @ [z'] @ zs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ls = [] @ [z] @ zs
ls' = [] @ [z'] @ zs'

goal (1 subgoal):
 1. z \<noteq> z' \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> z'
ls = [] @ [z] @ zs
ls' = [] @ [z'] @ zs'
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
z \<noteq> z'
ls = [] @ [z] @ zs
ls' = [] @ [z'] @ zs'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using less(2)
[PROOF STATE]
proof (prove)
using this:
z \<noteq> z'
ls = [] @ [z] @ zs
ls' = [] @ [z'] @ zs'
\<lbrakk>ls = ?xs @ [?x] @ ?ys; ls' = ?xs @ [?x'] @ ?ys'; ?x \<noteq> ?x'\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma three_cases: assumes \<open>A \<or> B \<or> C\<close> obtains \<open>A\<close> | \<open>B\<close> | \<open>C\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow> thesis; B \<Longrightarrow> thesis; C \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<or> B \<or> C

goal (1 subgoal):
 1. \<lbrakk>A \<Longrightarrow> thesis; B \<Longrightarrow> thesis; C \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma insort_greater: \<open>\<forall> x \<in> set ls. x < y \<Longrightarrow> insort y ls = ls@[y]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set ls. x < y \<Longrightarrow> insort y ls = ls @ [y]
[PROOF STEP]
by (induction \<open>ls\<close>,auto)


[STATEMENT]
lemma insort_append_first: assumes \<open>\<forall> y \<in> set ys. x \<le> y\<close> shows \<open>insort x (xs@ys) = insort x xs @ ys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insort x (xs @ ys) = insort x xs @ ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set ys. x \<le> y

goal (1 subgoal):
 1. insort x (xs @ ys) = insort x xs @ ys
[PROOF STEP]
by (induction \<open>xs\<close>,auto,metis insort_is_Cons)