[STATEMENT]
lemma foldl_echelon_form_column_k_eq:
  fixes A::"'a::{bezout_ring}^'cols::{mod_type}^'rows::{mod_type}"
  assumes k: "k<ncols A"
  shows matrix_to_iarray_echelon_form_of_upt_k[code_unfold]:
  "matrix_to_iarray (echelon_form_of_upt_k A k bezout)
  = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout"
  and fst_foldl_ef_k_eq: "fst (snd (foldl echelon_form_of_column_k_iarrays
  (matrix_to_iarray A,0,bezout) [0..<Suc k]))
  = snd (foldl (echelon_form_of_column_k bezout) (A,0) [0..<Suc k])"
  and fst_foldl_ef_k_less:
  "snd (foldl (echelon_form_of_column_k bezout) (A,0) [0..<Suc k]) \<le> nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout &&& fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) &&& snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k < ncols A

goal (1 subgoal):
 1. matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout &&& fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) &&& snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. 0 < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A 0 bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) 0 bezout
 2. 0 < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc 0])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0])
 3. 0 < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0]) \<le> nrows A
 4. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 5. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 6. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
show "matrix_to_iarray (echelon_form_of_upt_k A 0 bezout)
    = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) 0 bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (echelon_form_of_upt_k A 0 bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) 0 bezout
[PROOF STEP]
unfolding echelon_form_of_upt_k_def echelon_form_of_upt_k_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0])) = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc 0])
[PROOF STEP]
by (simp, metis le0 matrix_to_iarray_echelon_form_of_column_k ncols_not_0 neq0_conv)
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (echelon_form_of_upt_k A 0 bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) 0 bezout

goal (5 subgoals):
 1. 0 < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc 0])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0])
 2. 0 < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0]) \<le> nrows A
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 4. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 5. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
show "fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc 0]))
    = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc 0])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0])
[PROOF STEP]
by (simp, metis le0 ncols_not_0 not_gr0 snd_matrix_to_iarray_echelon_form_of_column_k)
[PROOF STATE]
proof (state)
this:
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc 0])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0])

goal (4 subgoals):
 1. 0 < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0]) \<le> nrows A
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 4. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
show "snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0]) \<le> nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0]) \<le> nrows A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (echelon_form_of_column_k bezout (A, 0) 0) \<le> nrows A
[PROOF STEP]
unfolding echelon_form_of_column_k_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (case (A, 0) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat 0 = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat 0 = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat 0 \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat 0) bezout, i + 1)) \<le> nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (case (A, 0) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat 0 = (0::'a)) \<or> i = CARD('rows) then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat 0 = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat 0 \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (CARD('rows) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat 0) bezout, i + 1)) \<le> CARD('rows)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc 0]) \<le> nrows A

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
assume "(k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout)
    = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout)"
    and  "(k < ncols A \<Longrightarrow>
    fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) =
    snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))"
    and hyp3: "(k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A)"
    and Suc_k_less_card: "Suc k < ncols A"
[PROOF STATE]
proof (state)
this:
k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout
k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])
k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
Suc k < ncols A

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
hence hyp1: "matrix_to_iarray (echelon_form_of_upt_k A k bezout)
    = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout"
    and hyp2: "fst (snd (foldl echelon_form_of_column_k_iarrays
    (matrix_to_iarray A, 0, bezout) [0..<Suc k]))
    = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])"
    and hyp3: "snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A"
[PROOF STATE]
proof (prove)
using this:
k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout
k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])
k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
Suc k < ncols A

goal (1 subgoal):
 1. matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout &&& fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) &&& snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
hence hyp1_unfolded: "matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A,0) [0..<Suc k]))
    = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A,0,bezout) [0..<Suc k])"
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A

goal (1 subgoal):
 1. matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])
[PROOF STEP]
using hyp1
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout

goal (1 subgoal):
 1. matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])
[PROOF STEP]
unfolding echelon_form_of_upt_k_def echelon_form_of_upt_k_iarrays_def
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])

goal (1 subgoal):
 1. matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) = fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
have upt_rw: "[0..<Suc (Suc k)] = [0..<Suc k] @ [(Suc k)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
let ?f = "foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
let ?f2 = "foldl (echelon_form_of_column_k bezout) (A,0) [0..<(Suc k)]"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
have fold_rw: "?f = (fst ?f, fst (snd ?f), snd (snd ?f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k] = (fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k] = (fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
have fold_rw': "?f2 = (fst ?f2, snd ?f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k] = (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k] = (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
have rw: "snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])
    = fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) = fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))
[PROOF STEP]
using hyp2
[PROOF STATE]
proof (prove)
using this:
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])

goal (1 subgoal):
 1. snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) = fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) = fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))

goal (3 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
 3. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
show "fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout)
    [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])
[PROOF STEP]
unfolding upt_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl echelon_form_of_column_k_iarrays (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]) [Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) [Suc k])
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (echelon_form_of_column_k_iarrays (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]) (Suc k))) = snd (echelon_form_of_column_k bezout (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) (Suc k))
[PROOF STEP]
apply (subst fold_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (echelon_form_of_column_k_iarrays (fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))) = snd (echelon_form_of_column_k bezout (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) (Suc k))
[PROOF STEP]
apply (subst fold_rw')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (echelon_form_of_column_k_iarrays (fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))) = snd (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) (Suc k))
[PROOF STEP]
unfolding hyp2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (echelon_form_of_column_k_iarrays (fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))) = snd (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) (Suc k))
[PROOF STEP]
unfolding hyp1_unfolded[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))) = snd (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) (Suc k))
[PROOF STEP]
unfolding rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))) = snd (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))
[PROOF STEP]
unfolding snd_snd_foldl_echelon_form_of_column_k_iarrays
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), bezout) (Suc k))) = snd (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))
[PROOF STEP]
proof (rule fst_snd_matrix_to_iarray_echelon_form_of_column_k [symmetric])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
 2. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
show "Suc k < ncols (fst ?f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
using Suc_k_less_card
[PROOF STATE]
proof (prove)
using this:
Suc k < ncols A

goal (1 subgoal):
 1. Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
unfolding ncols_def
[PROOF STATE]
proof (prove)
using this:
Suc k < CARD('cols)

goal (1 subgoal):
 1. Suc k < CARD('cols)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))

goal (1 subgoal):
 1. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
show "fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))
    \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
by (metis hyp2 hyp3 nrows_def)
[PROOF STATE]
proof (state)
this:
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc (Suc k)])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)])

goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
 2. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
show "matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout)
    = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout
[PROOF STEP]
unfolding echelon_form_of_upt_k_def echelon_form_of_upt_k_iarrays_def
      upt_rw foldl_append List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) (Suc k))) = fst (echelon_form_of_column_k_iarrays (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]) (Suc k))
[PROOF STEP]
apply (subst fold_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) (Suc k))) = fst (echelon_form_of_column_k_iarrays (fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))
[PROOF STEP]
apply (subst fold_rw')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) (Suc k))) = fst (echelon_form_of_column_k_iarrays (fst (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))
[PROOF STEP]
unfolding hyp2 hyp1_unfolded[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) (Suc k))) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))
[PROOF STEP]
unfolding rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))
[PROOF STEP]
unfolding snd_snd_foldl_echelon_form_of_column_k_iarrays
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))) (Suc k))) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])), fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])), bezout) (Suc k))
[PROOF STEP]
proof (rule matrix_to_iarray_echelon_form_of_column_k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
 2. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
show "Suc k < ncols (fst ?f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
using Suc_k_less_card
[PROOF STATE]
proof (prove)
using this:
Suc k < ncols A

goal (1 subgoal):
 1. Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
unfolding ncols_def
[PROOF STATE]
proof (prove)
using this:
Suc k < CARD('cols)

goal (1 subgoal):
 1. Suc k < CARD('cols)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Suc k < ncols (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))

goal (1 subgoal):
 1. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
show "fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k]))
    \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))
[PROOF STEP]
by (metis hyp2 hyp3 nrows_def)
[PROOF STATE]
proof (state)
this:
fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) \<le> nrows (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (echelon_form_of_upt_k A (Suc k) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (Suc k) bezout

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < ncols A \<Longrightarrow> matrix_to_iarray (echelon_form_of_upt_k A k bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) k bezout; k < ncols A \<Longrightarrow> fst (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]); k < ncols A \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A; Suc k < ncols A\<rbrakk> \<Longrightarrow> snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
show "snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
using [[unfold_abs_def = false]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A
[PROOF STEP]
unfolding upt_rw foldl_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (foldl (echelon_form_of_column_k bezout) (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) [Suc k]) \<le> nrows A
[PROOF STEP]
unfolding List.foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (echelon_form_of_column_k bezout (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) (Suc k)) \<le> nrows A
[PROOF STEP]
apply (subst fold_rw')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (echelon_form_of_column_k bezout (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) (Suc k)) \<le> nrows A
[PROOF STEP]
unfolding echelon_form_of_column_k_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (case (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat (Suc k) = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat (Suc k) = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat (Suc k) \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat (Suc k)) bezout, i + 1)) \<le> nrows A
[PROOF STEP]
using hyp3 le_antisym not_less_eq_eq
[PROOF STATE]
proof (prove)
using this:
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> nrows A
\<lbrakk>?m \<le> ?n; ?n \<le> ?m\<rbrakk> \<Longrightarrow> ?m = ?n
(\<not> ?m \<le> ?n) = (Suc ?n \<le> ?m)

goal (1 subgoal):
 1. snd (case (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat (Suc k) = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat (Suc k) = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat (Suc k) \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat (Suc k)) bezout, i + 1)) \<le> nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]) \<le> CARD('rows)
\<lbrakk>?m \<le> ?n; ?n \<le> ?m\<rbrakk> \<Longrightarrow> ?m = ?n
(\<not> ?m \<le> ?n) = (Suc ?n \<le> ?m)

goal (1 subgoal):
 1. snd (case (fst (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k]), snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc k])) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat (Suc k) = (0::'a)) \<or> i = CARD('rows) then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat (Suc k) = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat (Suc k) \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (CARD('rows) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat (Suc k)) bezout, i + 1)) \<le> CARD('rows)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
snd (foldl (echelon_form_of_column_k bezout) (A, 0) [0..<Suc (Suc k)]) \<le> nrows A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_echelon_form_of[code_unfold]:
  "matrix_to_iarray (echelon_form_of A bezout)
    = echelon_form_of_iarrays (matrix_to_iarray A) bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (echelon_form_of A bezout) = echelon_form_of_iarrays (matrix_to_iarray A) bezout
[PROOF STEP]
unfolding echelon_form_of_def echelon_form_of_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (echelon_form_of_upt_k A (ncols A - 1) bezout) = echelon_form_of_upt_k_iarrays (matrix_to_iarray A) (ncols_iarray (matrix_to_iarray A) - 1) bezout
[PROOF STEP]
by (metis (poly_guards_query) One_nat_def diff_less lessI matrix_to_iarray_echelon_form_of_upt_k
    ncols_def ncols_eq_card_columns zero_less_card_finite)


[STATEMENT]
lemma resNil:
  fixes x :: name

  shows "\<lparr>\<nu>x\<rparr>\<zero> \<sim> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<zero>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<zero>
[PROOF STEP]
have "(\<lparr>\<nu>x\<rparr>\<zero>, \<zero>) \<in> {(\<lparr>\<nu>x\<rparr>\<zero>, \<zero>), (\<zero>, \<lparr>\<nu>x\<rparr>\<zero>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lparr>\<nu>x\<rparr>\<zero>, \<zero>) \<in> {(\<lparr>\<nu>x\<rparr>\<zero>, \<zero>), (\<zero>, \<lparr>\<nu>x\<rparr>\<zero>)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lparr>\<nu>x\<rparr>\<zero>, \<zero>) \<in> {(\<lparr>\<nu>x\<rparr>\<zero>, \<zero>), (\<zero>, \<lparr>\<nu>x\<rparr>\<zero>)}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<zero>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lparr>\<nu>x\<rparr>\<zero>, \<zero>) \<in> {(\<lparr>\<nu>x\<rparr>\<zero>, \<zero>), (\<zero>, \<lparr>\<nu>x\<rparr>\<zero>)}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<zero>
[PROOF STEP]
by(coinduct rule: bisimCoinduct)
      (auto intro: resNilLeft resNilRight)
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>\<zero> \<sim> \<zero>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scopeExt:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x \<sharp> P"

  shows "\<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
let ?X = "{(\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) | x P Q. x \<sharp> P} \<union> {(P \<parallel> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<parallel> Q)) | x P Q. x \<sharp> P}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> P
[PROOF STEP]
have "(\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P

goal (1 subgoal):
 1. (\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) |x P Q. x \<sharp> P} \<union> {(P \<parallel> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<parallel> Q)) |x P Q. x \<sharp> P}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) |x P Q. x \<sharp> P} \<union> {(P \<parallel> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<parallel> Q)) |x P Q. x \<sharp> P}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<parallel> Q), P \<parallel> \<lparr>\<nu>x\<rparr>Q) |x P Q. x \<sharp> P} \<union> {(P \<parallel> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<parallel> Q)) |x P Q. x \<sharp> P}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (force intro: scopeExtLeft scopeExtRight)+
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumComm:
  fixes P :: ccs
  and   Q :: ccs

  shows "P \<oplus> Q \<sim> Q \<oplus> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<sim> Q \<oplus> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> Q \<sim> Q \<oplus> P
[PROOF STEP]
have "(P \<oplus> Q, Q \<oplus> P) \<in> {(P \<oplus> Q, Q \<oplus> P), (Q \<oplus> P, P \<oplus> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q, Q \<oplus> P) \<in> {(P \<oplus> Q, Q \<oplus> P), (Q \<oplus> P, P \<oplus> Q)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q, Q \<oplus> P) \<in> {(P \<oplus> Q, Q \<oplus> P), (Q \<oplus> P, P \<oplus> Q)}

goal (1 subgoal):
 1. P \<oplus> Q \<sim> Q \<oplus> P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> Q, Q \<oplus> P) \<in> {(P \<oplus> Q, Q \<oplus> P), (Q \<oplus> P, P \<oplus> Q)}

goal (1 subgoal):
 1. P \<oplus> Q \<sim> Q \<oplus> P
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: sumComm reflexive)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<sim> Q \<oplus> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumAssoc:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  shows "(P \<oplus> Q) \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> Q \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)
[PROOF STEP]
have "((P \<oplus> Q) \<oplus> R, P \<oplus> (Q \<oplus> R)) \<in> {((P \<oplus> Q) \<oplus> R, P \<oplus> (Q \<oplus> R)), (P \<oplus> (Q \<oplus> R), (P \<oplus> Q) \<oplus> R)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q \<oplus> R, P \<oplus> (Q \<oplus> R)) \<in> {(P \<oplus> Q \<oplus> R, P \<oplus> (Q \<oplus> R)), (P \<oplus> (Q \<oplus> R), P \<oplus> Q \<oplus> R)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q \<oplus> R, P \<oplus> (Q \<oplus> R)) \<in> {(P \<oplus> Q \<oplus> R, P \<oplus> (Q \<oplus> R)), (P \<oplus> (Q \<oplus> R), P \<oplus> Q \<oplus> R)}

goal (1 subgoal):
 1. P \<oplus> Q \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> Q \<oplus> R, P \<oplus> (Q \<oplus> R)) \<in> {(P \<oplus> Q \<oplus> R, P \<oplus> (Q \<oplus> R)), (P \<oplus> (Q \<oplus> R), P \<oplus> Q \<oplus> R)}

goal (1 subgoal):
 1. P \<oplus> Q \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: sumAssocLeft sumAssocRight reflexive)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumId:
  fixes P :: ccs

  shows "P \<oplus> \<zero> \<sim> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> \<zero> \<sim> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> \<zero> \<sim> P
[PROOF STEP]
have "(P \<oplus> \<zero>, P) \<in> {(P \<oplus> \<zero>, P), (P, P \<oplus> \<zero>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> \<zero>, P) \<in> {(P \<oplus> \<zero>, P), (P, P \<oplus> \<zero>)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P \<oplus> \<zero>, P) \<in> {(P \<oplus> \<zero>, P), (P, P \<oplus> \<zero>)}

goal (1 subgoal):
 1. P \<oplus> \<zero> \<sim> P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> \<zero>, P) \<in> {(P \<oplus> \<zero>, P), (P, P \<oplus> \<zero>)}

goal (1 subgoal):
 1. P \<oplus> \<zero> \<sim> P
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: sumIdLeft sumIdRight reflexive)
[PROOF STATE]
proof (state)
this:
P \<oplus> \<zero> \<sim> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parComm:
  fixes P :: ccs
  and   Q :: ccs

  shows "P \<parallel> Q \<sim> Q \<parallel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<sim> Q \<parallel> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> Q \<sim> Q \<parallel> P
[PROOF STEP]
have "(P \<parallel> Q, Q \<parallel> P) \<in> {(P \<parallel> Q, Q \<parallel> P) | P Q. True} \<union> {(Q \<parallel> P, P \<parallel> Q) | P Q. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<parallel> Q, Q \<parallel> P) \<in> {(P \<parallel> Q, Q \<parallel> P) |P Q. True} \<union> {(Q \<parallel> P, P \<parallel> Q) |P Q. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(P \<parallel> Q, Q \<parallel> P) \<in> {(P \<parallel> Q, Q \<parallel> P) |P Q. True} \<union> {(Q \<parallel> P, P \<parallel> Q) |P Q. True}

goal (1 subgoal):
 1. P \<parallel> Q \<sim> Q \<parallel> P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<parallel> Q, Q \<parallel> P) \<in> {(P \<parallel> Q, Q \<parallel> P) |P Q. True} \<union> {(Q \<parallel> P, P \<parallel> Q) |P Q. True}

goal (1 subgoal):
 1. P \<parallel> Q \<sim> Q \<parallel> P
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: parComm)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<sim> Q \<parallel> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parAssoc:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  shows "(P \<parallel> Q) \<parallel> R \<sim> P \<parallel> (Q \<parallel> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<parallel> R \<sim> P \<parallel> (Q \<parallel> R)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> Q \<parallel> R \<sim> P \<parallel> (Q \<parallel> R)
[PROOF STEP]
have "((P \<parallel> Q) \<parallel> R, P \<parallel> (Q \<parallel> R)) \<in> {((P \<parallel> Q) \<parallel> R, P \<parallel> (Q \<parallel> R)) | P Q R. True} \<union>
                                     {(P \<parallel> (Q \<parallel> R), (P \<parallel> Q) \<parallel> R) | P Q R. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<parallel> Q \<parallel> R, P \<parallel> (Q \<parallel> R)) \<in> {(P \<parallel> Q \<parallel> R, P \<parallel> (Q \<parallel> R)) |P Q R. True} \<union> {(P \<parallel> (Q \<parallel> R), P \<parallel> Q \<parallel> R) |P Q R. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(P \<parallel> Q \<parallel> R, P \<parallel> (Q \<parallel> R)) \<in> {(P \<parallel> Q \<parallel> R, P \<parallel> (Q \<parallel> R)) |P Q R. True} \<union> {(P \<parallel> (Q \<parallel> R), P \<parallel> Q \<parallel> R) |P Q R. True}

goal (1 subgoal):
 1. P \<parallel> Q \<parallel> R \<sim> P \<parallel> (Q \<parallel> R)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<parallel> Q \<parallel> R, P \<parallel> (Q \<parallel> R)) \<in> {(P \<parallel> Q \<parallel> R, P \<parallel> (Q \<parallel> R)) |P Q R. True} \<union> {(P \<parallel> (Q \<parallel> R), P \<parallel> Q \<parallel> R) |P Q R. True}

goal (1 subgoal):
 1. P \<parallel> Q \<parallel> R \<sim> P \<parallel> (Q \<parallel> R)
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (force intro: parAssocLeft parAssocRight)+
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<parallel> R \<sim> P \<parallel> (Q \<parallel> R)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parId:
  fixes P :: ccs

  shows "P \<parallel> \<zero> \<sim> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> \<zero> \<sim> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> \<zero> \<sim> P
[PROOF STEP]
have "(P \<parallel> \<zero>, P) \<in> {(P \<parallel> \<zero>, P) | P. True} \<union> {(P, P \<parallel> \<zero>) | P. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<parallel> \<zero>, P) \<in> {(P \<parallel> \<zero>, P) |P. True} \<union> {(P, P \<parallel> \<zero>) |P. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P \<parallel> \<zero>, P) \<in> {(P \<parallel> \<zero>, P) |P. True} \<union> {(P, P \<parallel> \<zero>) |P. True}

goal (1 subgoal):
 1. P \<parallel> \<zero> \<sim> P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<parallel> \<zero>, P) \<in> {(P \<parallel> \<zero>, P) |P. True} \<union> {(P, P \<parallel> \<zero>) |P. True}

goal (1 subgoal):
 1. P \<parallel> \<zero> \<sim> P
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: parIdLeft parIdRight)
[PROOF STATE]
proof (state)
this:
P \<parallel> \<zero> \<sim> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scopeFresh:
  fixes x :: name
  and   P :: ccs

  assumes "x \<sharp> P"

  shows "\<lparr>\<nu>x\<rparr>P \<sim> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have "\<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>P \<parallel> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>P \<parallel> \<zero>
[PROOF STEP]
by(rule parId[THEN symmetric])
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>P \<parallel> \<zero>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>P \<parallel> \<zero>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have "\<lparr>\<nu>x\<rparr>P \<parallel> \<zero> \<sim> \<zero> \<parallel> \<lparr>\<nu>x\<rparr>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<parallel> \<zero> \<sim> \<zero> \<parallel> \<lparr>\<nu>x\<rparr>P
[PROOF STEP]
by(rule parComm)
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>P \<parallel> \<zero> \<sim> \<zero> \<parallel> \<lparr>\<nu>x\<rparr>P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>P \<parallel> \<zero> \<sim> \<zero> \<parallel> \<lparr>\<nu>x\<rparr>P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have "\<zero> \<parallel> \<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<parallel> \<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P)
[PROOF STEP]
by(rule scopeExt[THEN symmetric]) auto
[PROOF STATE]
proof (state)
this:
\<zero> \<parallel> \<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P)

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<zero> \<parallel> \<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P)

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have "\<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P) \<sim> \<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P) \<sim> \<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>)
[PROOF STEP]
by(rule resPres[OF parComm])
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P) \<sim> \<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>)

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P) \<sim> \<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>)

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
from \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> P
[PROOF STEP]
have "\<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>\<zero>"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>\<zero>
[PROOF STEP]
by(rule scopeExt)
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>\<zero>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>\<zero>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have  "P \<parallel> \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<lparr>\<nu>x\<rparr>\<zero> \<parallel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<lparr>\<nu>x\<rparr>\<zero> \<parallel> P
[PROOF STEP]
by(rule parComm)
[PROOF STATE]
proof (state)
this:
P \<parallel> \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<lparr>\<nu>x\<rparr>\<zero> \<parallel> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<lparr>\<nu>x\<rparr>\<zero> \<parallel> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have "\<lparr>\<nu>x\<rparr>\<zero> \<parallel> P \<sim> \<zero> \<parallel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<zero> \<parallel> P \<sim> \<zero> \<parallel> P
[PROOF STEP]
by(rule parPres[OF resNil])
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>\<zero> \<parallel> P \<sim> \<zero> \<parallel> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>\<zero> \<parallel> P \<sim> \<zero> \<parallel> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have "\<zero> \<parallel> P \<sim> P \<parallel> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<parallel> P \<sim> P \<parallel> \<zero>
[PROOF STEP]
by(rule parComm)
[PROOF STATE]
proof (state)
this:
\<zero> \<parallel> P \<sim> P \<parallel> \<zero>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<zero> \<parallel> P \<sim> P \<parallel> \<zero>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
have "P \<parallel> \<zero> \<sim> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> \<zero> \<sim> P
[PROOF STEP]
by(rule parId)
[PROOF STATE]
proof (state)
this:
P \<parallel> \<zero> \<sim> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>P \<parallel> \<zero>
\<lparr>\<nu>x\<rparr>P \<parallel> \<zero> \<sim> \<zero> \<parallel> \<lparr>\<nu>x\<rparr>P
\<zero> \<parallel> \<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P)
\<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P) \<sim> \<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>)
\<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>\<zero>
P \<parallel> \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<lparr>\<nu>x\<rparr>\<zero> \<parallel> P
\<lparr>\<nu>x\<rparr>\<zero> \<parallel> P \<sim> \<zero> \<parallel> P
\<zero> \<parallel> P \<sim> P \<parallel> \<zero>
P \<parallel> \<zero> \<sim> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>P \<parallel> \<zero>
\<lparr>\<nu>x\<rparr>P \<parallel> \<zero> \<sim> \<zero> \<parallel> \<lparr>\<nu>x\<rparr>P
\<zero> \<parallel> \<lparr>\<nu>x\<rparr>P \<sim> \<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P)
\<lparr>\<nu>x\<rparr>(\<zero> \<parallel> P) \<sim> \<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>)
\<lparr>\<nu>x\<rparr>(P \<parallel> \<zero>) \<sim> P \<parallel> \<lparr>\<nu>x\<rparr>\<zero>
P \<parallel> \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<lparr>\<nu>x\<rparr>\<zero> \<parallel> P
\<lparr>\<nu>x\<rparr>\<zero> \<parallel> P \<sim> \<zero> \<parallel> P
\<zero> \<parallel> P \<sim> P \<parallel> \<zero>
P \<parallel> \<zero> \<sim> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<sim> P
[PROOF STEP]
by(metis transitive)
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>P \<sim> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scopeExtSum:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x \<sharp> P"

  shows "\<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<sim> P \<oplus> \<lparr>\<nu>x\<rparr>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<sim> P \<oplus> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<sim> P \<oplus> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
have "(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q), (P \<oplus> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<oplus> Q))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q), (P \<oplus> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<oplus> Q))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q), (P \<oplus> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<oplus> Q))}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<sim> P \<oplus> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q), (P \<oplus> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<oplus> Q))}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<sim> P \<oplus> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
using \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q) \<in> {(\<lparr>\<nu>x\<rparr>(P \<oplus> Q), P \<oplus> \<lparr>\<nu>x\<rparr>Q), (P \<oplus> \<lparr>\<nu>x\<rparr>Q, \<lparr>\<nu>x\<rparr>(P \<oplus> Q))}
x \<sharp> P

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<sim> P \<oplus> \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct)
      (auto intro: scopeExtSumLeft scopeExtSumRight reflexive scopeFresh scopeFresh[THEN symmetric])
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<sim> P \<oplus> \<lparr>\<nu>x\<rparr>Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resAct:
  fixes x :: name
  and   \<alpha> :: act
  and   P :: ccs

  assumes "x \<sharp> \<alpha>"

  shows "\<lparr>\<nu>x\<rparr>(\<alpha>.(P)) \<sim> \<alpha>.(\<lparr>\<nu>x\<rparr>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<alpha>.P \<sim> \<alpha>.(\<lparr>\<nu>x\<rparr>P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<alpha>.P \<sim> \<alpha>.(\<lparr>\<nu>x\<rparr>P)
[PROOF STEP]
have "(\<lparr>\<nu>x\<rparr>(\<alpha>.(P)), \<alpha>.(\<lparr>\<nu>x\<rparr>P)) \<in> {(\<lparr>\<nu>x\<rparr>(\<alpha>.(P)), \<alpha>.(\<lparr>\<nu>x\<rparr>P)), (\<alpha>.(\<lparr>\<nu>x\<rparr>P), \<lparr>\<nu>x\<rparr>(\<alpha>.(P)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)) \<in> {(\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)), (\<alpha>.(\<lparr>\<nu>x\<rparr>P), \<lparr>\<nu>x\<rparr>\<alpha>.P)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)) \<in> {(\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)), (\<alpha>.(\<lparr>\<nu>x\<rparr>P), \<lparr>\<nu>x\<rparr>\<alpha>.P)}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<alpha>.P \<sim> \<alpha>.(\<lparr>\<nu>x\<rparr>P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)) \<in> {(\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)), (\<alpha>.(\<lparr>\<nu>x\<rparr>P), \<lparr>\<nu>x\<rparr>\<alpha>.P)}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<alpha>.P \<sim> \<alpha>.(\<lparr>\<nu>x\<rparr>P)
[PROOF STEP]
using \<open>x \<sharp> \<alpha>\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)) \<in> {(\<lparr>\<nu>x\<rparr>\<alpha>.P, \<alpha>.(\<lparr>\<nu>x\<rparr>P)), (\<alpha>.(\<lparr>\<nu>x\<rparr>P), \<lparr>\<nu>x\<rparr>\<alpha>.P)}
x \<sharp> \<alpha>

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<alpha>.P \<sim> \<alpha>.(\<lparr>\<nu>x\<rparr>P)
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: resActLeft resActRight reflexive)
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>\<alpha>.P \<sim> \<alpha>.(\<lparr>\<nu>x\<rparr>P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resComm:
  fixes x :: name
  and   y :: name
  and   P :: ccs

  shows "\<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>P) \<sim> \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P \<sim> \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P \<sim> \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
have "(\<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>P), \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>P)) \<in> {(\<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>P), \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>P)) | x y P. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P, \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P) \<in> {(\<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P, \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P) |x y P. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P, \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P) \<in> {(\<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P, \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P) |x y P. True}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P \<sim> \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P, \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P) \<in> {(\<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P, \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P) |x y P. True}

goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P \<sim> \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: resComm)
[PROOF STATE]
proof (state)
this:
\<lparr>\<nu>x\<rparr>\<lparr>\<nu>y\<rparr>P \<sim> \<lparr>\<nu>y\<rparr>\<lparr>\<nu>x\<rparr>P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bangUnfold:
  fixes P

  shows "!P \<sim> P \<parallel> !P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<sim> P \<parallel> !P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. !P \<sim> P \<parallel> !P
[PROOF STEP]
have "(!P, P \<parallel> !P) \<in> {(!P, P \<parallel> !P), (P \<parallel> !P, !P)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!P, P \<parallel> !P) \<in> {(!P, P \<parallel> !P), (P \<parallel> !P, !P)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(!P, P \<parallel> !P) \<in> {(!P, P \<parallel> !P), (P \<parallel> !P, !P)}

goal (1 subgoal):
 1. !P \<sim> P \<parallel> !P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(!P, P \<parallel> !P) \<in> {(!P, P \<parallel> !P), (P \<parallel> !P, !P)}

goal (1 subgoal):
 1. !P \<sim> P \<parallel> !P
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: bangUnfoldLeft bangUnfoldRight reflexive)
[PROOF STATE]
proof (state)
this:
!P \<sim> P \<parallel> !P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bisimStructCong:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P \<equiv>\<^sub>s Q"

  shows "P \<sim> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sim> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<equiv>\<^sub>s Q

goal (1 subgoal):
 1. P \<sim> Q
[PROOF STEP]
apply(nominal_induct rule: Struct_Cong.strong_induct)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>P. P \<sim> P
 2. \<And>P Q. \<lbrakk>P \<equiv>\<^sub>s Q; P \<sim> Q\<rbrakk> \<Longrightarrow> Q \<sim> P
 3. \<And>P Q R. \<lbrakk>P \<equiv>\<^sub>s Q; P \<sim> Q; Q \<equiv>\<^sub>s R; Q \<sim> R\<rbrakk> \<Longrightarrow> P \<sim> R
 4. \<And>P Q. P \<parallel> Q \<sim> Q \<parallel> P
 5. \<And>P Q R. P \<parallel> Q \<parallel> R \<sim> P \<parallel> (Q \<parallel> R)
 6. \<And>P. P \<parallel> \<zero> \<sim> P
 7. \<And>P Q. P \<oplus> Q \<sim> Q \<oplus> P
 8. \<And>P Q R. P \<oplus> Q \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)
 9. \<And>P. P \<oplus> \<zero> \<sim> P
 10. \<And>x. \<lparr>\<nu>x\<rparr>\<zero> \<sim> \<zero>
A total of 15 subgoals...
[PROOF STEP]
by(auto intro: reflexive symmetric transitive parComm parAssoc parId sumComm
   sumAssoc sumId resNil scopeExt scopeExtSum resAct resComm bangUnfold)


[STATEMENT]
lemma succ_as_E: "set (succ x) = E_of_succ succ `` {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (succ x) = E_of_succ succ `` {x}
[PROOF STEP]
unfolding E_of_succ_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (succ x) = {(u, v). v \<in> set (succ u)} `` {x}
[PROOF STEP]
by auto


[STATEMENT]
lemma card_decreases: "
   \<lbrakk>finite V; y \<notin> V; dfs_reachable_invar D V (Set.insert y W) brk \<rbrakk>
   \<Longrightarrow> card (E\<^sup>* `` W\<^sub>0 - Set.insert y V) < card (E\<^sup>* `` W\<^sub>0 - V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite V; y \<notin> V; local.dfs_reachable_invar D V (insert y W) brk\<rbrakk> \<Longrightarrow> card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - insert y V) < card ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)
[PROOF STEP]
apply (rule psubset_card_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite V; y \<notin> V; local.dfs_reachable_invar D V (insert y W) brk\<rbrakk> \<Longrightarrow> finite ((E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V)
 2. \<lbrakk>finite V; y \<notin> V; local.dfs_reachable_invar D V (insert y W) brk\<rbrakk> \<Longrightarrow> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 - insert y V \<subset> (E_of_succ succ)\<^sup>* `` set w\<^sub>0 - V
[PROOF STEP]
apply (auto simp: dfs_reachable_invar_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma all_neq_Cons_is_Nil[simp]: (* Odd term remaining in goal \<dots> *)
  "(\<forall>y ys. x2 \<noteq> y # ys) \<longleftrightarrow> x2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y ys. x2 \<noteq> y # ys) = (x2 = [])
[PROOF STEP]
by (cases x2) auto