[STATEMENT]
lemma vec_to_iarray_solve_consistent_rref:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
shows "vec_to_iarray (solve_consistent_rref A b) = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref A b) = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
proof(unfold iarray_exhaust2 list_eq_iff_nth_eq IArray.length_def[symmetric] IArray.sub_def[symmetric], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. IArray.length (vec_to_iarray (solve_consistent_rref A b)) = IArray.length (solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b))
 2. \<forall>i<IArray.length (vec_to_iarray (solve_consistent_rref A b)). vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
show "IArray.length (vec_to_iarray (solve_consistent_rref A b)) = IArray.length (solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (vec_to_iarray (solve_consistent_rref A b)) = IArray.length (solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b))
[PROOF STEP]
unfolding solve_consistent_rref_def solve_consistent_rref_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (vec_to_iarray (\<chi>j. if \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a)) then b $ (THE i. A $ i $ j = (1::'a)) else (0::'a))) = IArray.length (IArray.of_fun (\<lambda>j. if IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! j = (1::'a) \<and> j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) then vec_to_iarray b !! least_non_zero_position_of_vector (column_iarray j (matrix_to_iarray A)) else (0::'a)) (ncols_iarray (matrix_to_iarray A)))
[PROOF STEP]
unfolding ncols_iarray_def matrix_to_iarray_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (vec_to_iarray (\<chi>j. if \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a)) then b $ (THE i. A $ i $ j = (1::'a)) else (0::'a))) = IArray.length (IArray.of_fun (\<lambda>j. if IArray.exists (\<lambda>i. IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('rows)]) !! i !! j = (1::'a) \<and> j = least_non_zero_position_of_vector (row_iarray i (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('rows)])))) (IArray [0..<nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('rows)]))]) then vec_to_iarray b !! least_non_zero_position_of_vector (column_iarray j (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('rows)]))) else (0::'a)) (IArray.length (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('rows)]) !! 0)))
[PROOF STEP]
by (simp add: vec_to_iarray_def)
[PROOF STATE]
proof (state)
this:
IArray.length (vec_to_iarray (solve_consistent_rref A b)) = IArray.length (solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b))

goal (1 subgoal):
 1. \<forall>i<IArray.length (vec_to_iarray (solve_consistent_rref A b)). vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
show "\<forall>i<IArray.length (vec_to_iarray (solve_consistent_rref A b)). vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<IArray.length (vec_to_iarray (solve_consistent_rref A b)). vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < IArray.length (vec_to_iarray (solve_consistent_rref A b)) \<Longrightarrow> vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < IArray.length (vec_to_iarray (solve_consistent_rref A b)) \<Longrightarrow> vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
assume i: "i < IArray.length (vec_to_iarray (solve_consistent_rref A b))"
[PROOF STATE]
proof (state)
this:
i < IArray.length (vec_to_iarray (solve_consistent_rref A b))

goal (1 subgoal):
 1. \<And>i. i < IArray.length (vec_to_iarray (solve_consistent_rref A b)) \<Longrightarrow> vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
hence i_less_card: "i<CARD('cols)"
[PROOF STATE]
proof (prove)
using this:
i < IArray.length (vec_to_iarray (solve_consistent_rref A b))

goal (1 subgoal):
 1. i < CARD('cols)
[PROOF STEP]
unfolding vec_to_iarray_def
[PROOF STATE]
proof (prove)
using this:
i < IArray.length (IArray.of_fun (\<lambda>i. solve_consistent_rref A b $ mod_type_class.from_nat i) CARD('cols))

goal (1 subgoal):
 1. i < CARD('cols)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < CARD('cols)

goal (1 subgoal):
 1. \<And>i. i < IArray.length (vec_to_iarray (solve_consistent_rref A b)) \<Longrightarrow> vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
hence i_less_ncols: "i<(ncols_iarray (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
using this:
i < CARD('cols)

goal (1 subgoal):
 1. i < ncols_iarray (matrix_to_iarray A)
[PROOF STEP]
unfolding ncols_eq_card_columns
[PROOF STATE]
proof (prove)
using this:
i < CARD('cols)

goal (1 subgoal):
 1. i < CARD('cols)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i < ncols_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. \<And>i. i < IArray.length (vec_to_iarray (solve_consistent_rref A b)) \<Longrightarrow> vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
show "vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
unfolding vec_to_iarray_nth[OF i_less_card]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solve_consistent_rref A b $ mod_type_class.from_nat i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
unfolding solve_consistent_rref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>j. if \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a)) then b $ (THE i. A $ i $ j = (1::'a)) else (0::'a)) $ mod_type_class.from_nat i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
unfolding vec_lambda_beta
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then b $ (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a)) else (0::'a)) = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i
[PROOF STEP]
unfolding solve_consistent_rref_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then b $ (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a)) else (0::'a)) = IArray.of_fun (\<lambda>j. if IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! j = (1::'a) \<and> j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) then vec_to_iarray b !! least_non_zero_position_of_vector (column_iarray j (matrix_to_iarray A)) else (0::'a)) (ncols_iarray (matrix_to_iarray A)) !! i
[PROOF STEP]
unfolding of_fun_nth[OF i_less_ncols]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then b $ (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a)) else (0::'a)) = (if IArray.exists (\<lambda>ia. matrix_to_iarray A !! ia !! i = (1::'a) \<and> i = least_non_zero_position_of_vector (row_iarray ia (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) then vec_to_iarray b !! least_non_zero_position_of_vector (column_iarray i (matrix_to_iarray A)) else (0::'a))
[PROOF STEP]
unfolding exists_solve_consistent_rref[OF rref, of "from_nat i", symmetric, unfolded to_nat_from_nat_id[OF i_less_card]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then b $ (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a)) else (0::'a)) = (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then vec_to_iarray b !! least_non_zero_position_of_vector (column_iarray i (matrix_to_iarray A)) else (0::'a))
[PROOF STEP]
using to_nat_the_solve_consistent_rref[OF rref, of "from_nat i", symmetric, unfolded to_nat_from_nat_id[OF i_less_card]]
[PROOF STATE]
proof (prove)
using this:
\<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) \<Longrightarrow> least_non_zero_position_of_vector (column_iarray i (matrix_to_iarray A)) = mod_type_class.to_nat (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a))

goal (1 subgoal):
 1. (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then b $ (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a)) else (0::'a)) = (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then vec_to_iarray b !! least_non_zero_position_of_vector (column_iarray i (matrix_to_iarray A)) else (0::'a))
[PROOF STEP]
using vec_to_iarray_nth'
[PROOF STATE]
proof (prove)
using this:
\<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) \<Longrightarrow> least_non_zero_position_of_vector (column_iarray i (matrix_to_iarray A)) = mod_type_class.to_nat (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a))
vec_to_iarray ?A !! mod_type_class.to_nat ?i = ?A $ ?i

goal (1 subgoal):
 1. (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then b $ (THE ia. A $ ia $ mod_type_class.from_nat i = (1::'a)) else (0::'a)) = (if \<exists>ia. A $ ia $ mod_type_class.from_nat i = (1::'a) \<and> mod_type_class.from_nat i = (LEAST n. A $ ia $ n \<noteq> (0::'a)) then vec_to_iarray b !! least_non_zero_position_of_vector (column_iarray i (matrix_to_iarray A)) else (0::'a))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<IArray.length (vec_to_iarray (solve_consistent_rref A b)). vec_to_iarray (solve_consistent_rref A b) !! i = solve_consistent_rref_iarrays (matrix_to_iarray A) (vec_to_iarray b) !! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_independent_and_consistent[code]:
shows "independent_and_consistent A b = independent_and_consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. independent_and_consistent A b = independent_and_consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding independent_and_consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent A b \<and> vec.dim (solution_set A 0) = 0) = independent_and_consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding independent_and_consistent_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent A b \<and> vec.dim (solution_set A 0) = 0) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> dim_solution_set = 0)
[PROOF STEP]
unfolding dim_solution_set_homogeneous_eq_dim_null_space
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent A b \<and> vec.dim (null_space A) = 0) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> dim_solution_set = 0)
[PROOF STEP]
unfolding matrix_to_iarray_consistent
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b) \<and> vec.dim (null_space A) = 0) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> dim_solution_set = 0)
[PROOF STEP]
unfolding consistent_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> vec.dim (null_space A) = 0) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> dim_solution_set = 0)
[PROOF STEP]
unfolding dim_null_space_iarray
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> ncols_iarray (matrix_to_iarray A) - rank_iarray (matrix_to_iarray A) = 0) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> dim_solution_set = 0)
[PROOF STEP]
unfolding rank_iarrays_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray A)))) = 0) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> dim_solution_set = 0)
[PROOF STEP]
unfolding snd_Gauss_Jordan_iarrays_PA_eq[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) = 0) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> dim_solution_set = 0)
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) \<and> ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) = 0) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) \<and> ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) = 0)
[PROOF STEP]
..


[STATEMENT]
lemma matrix_to_iarray_dependent_and_consistent[code]:
shows "dependent_and_consistent A b = dependent_and_consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dependent_and_consistent A b = dependent_and_consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding dependent_and_consistent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent A b \<and> 0 < vec.dim (solution_set A 0)) = dependent_and_consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding dependent_and_consistent_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent A b \<and> 0 < vec.dim (solution_set A 0)) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> 0 < dim_solution_set)
[PROOF STEP]
unfolding dim_solution_set_homogeneous_eq_dim_null_space
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent A b \<and> 0 < vec.dim (null_space A)) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> 0 < dim_solution_set)
[PROOF STEP]
unfolding matrix_to_iarray_consistent
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b) \<and> 0 < vec.dim (null_space A)) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> 0 < dim_solution_set)
[PROOF STEP]
unfolding consistent_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> 0 < vec.dim (null_space A)) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> 0 < dim_solution_set)
[PROOF STEP]
unfolding dim_null_space_iarray
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> 0 < ncols_iarray (matrix_to_iarray A) - rank_iarray (matrix_to_iarray A)) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> 0 < dim_solution_set)
[PROOF STEP]
unfolding rank_iarrays_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> 0 < ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray A))))) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> 0 < dim_solution_set)
[PROOF STEP]
unfolding snd_Gauss_Jordan_iarrays_PA_eq[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A) \<and> 0 < ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))) = (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv vec_to_iarray b; consistent_A = (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A; dim_solution_set = ncols_iarray (matrix_to_iarray A) - rank_A in consistent_A \<and> 0 < dim_solution_set)
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) \<and> 0 < ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) \<and> 0 < ncols_iarray (matrix_to_iarray A) - length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))))
[PROOF STEP]
..


[STATEMENT]
lemma matrix_to_iarray_fst_solve_system: "matrix_to_iarray (fst (solve_system A b)) = fst (solve_system_iarrays (matrix_to_iarray A) (vec_to_iarray b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (solve_system A b)) = fst (solve_system_iarrays (matrix_to_iarray A) (vec_to_iarray b))
[PROOF STEP]
unfolding solve_system_def solve_system_iarrays_def Let_def fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (snd (Gauss_Jordan_PA A)) = snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))
[PROOF STEP]
by (metis matrix_to_iarray_snd_Gauss_Jordan_PA)


[STATEMENT]
lemma vec_to_iarray_snd_solve_system: "vec_to_iarray (snd (solve_system A b)) = snd (solve_system_iarrays (matrix_to_iarray A) (vec_to_iarray b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (snd (solve_system A b)) = snd (solve_system_iarrays (matrix_to_iarray A) (vec_to_iarray b))
[PROOF STEP]
unfolding solve_system_def solve_system_iarrays_def Let_def snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (fst (Gauss_Jordan_PA A) *v b) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b
[PROOF STEP]
by (metis matrix_to_iarray_fst_Gauss_Jordan_PA vec_to_iarray_matrix_matrix_mult)


[STATEMENT]
lemma pair_vec_vecset_solve[code_unfold]:
shows "pair_vec_vecset (solve A b) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair_vec_vecset (solve A b) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding pair_vec_vecset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if Option.is_none (solve A b) then None else Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b)))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Option.is_none (solve A b) \<Longrightarrow> None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
 2. \<not> Option.is_none (solve A b) \<Longrightarrow> Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
assume none_solve_Ab: "Option.is_none (solve A b)"
[PROOF STATE]
proof (state)
this:
Option.is_none (solve A b)

goal (2 subgoals):
 1. Option.is_none (solve A b) \<Longrightarrow> None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
 2. \<not> Option.is_none (solve A b) \<Longrightarrow> Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
show "None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define GJ_P where "GJ_P = Gauss_Jordan_iarrays_PA (matrix_to_iarray A)"
[PROOF STATE]
proof (state)
this:
GJ_P = Gauss_Jordan_iarrays_PA (matrix_to_iarray A)

goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define P_mult_b where "P_mult_b = fst GJ_P *iv vec_to_iarray b"
[PROOF STATE]
proof (state)
this:
P_mult_b = fst GJ_P *iv vec_to_iarray b

goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define rank_A where "rank_A = length [x\<leftarrow>IArray.list_of (snd GJ_P). \<not> is_zero_iarray x]"
[PROOF STATE]
proof (state)
this:
rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ_P)))

goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
have "\<not> consistent A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> consistent A b
[PROOF STEP]
using none_solve_Ab
[PROOF STATE]
proof (prove)
using this:
Option.is_none (solve A b)

goal (1 subgoal):
 1. \<not> consistent A b
[PROOF STEP]
unfolding solve_def
[PROOF STATE]
proof (prove)
using this:
Option.is_none (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None)

goal (1 subgoal):
 1. \<not> consistent A b
[PROOF STEP]
unfolding Option.is_none_def
[PROOF STATE]
proof (prove)
using this:
(if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None) = None

goal (1 subgoal):
 1. \<not> consistent A b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> consistent A b

goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
hence "\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
using this:
\<not> consistent A b

goal (1 subgoal):
 1. \<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
using matrix_to_iarray_consistent
[PROOF STATE]
proof (prove)
using this:
\<not> consistent A b
consistent ?A ?b = consistent_iarrays (matrix_to_iarray ?A) (vec_to_iarray ?b)

goal (1 subgoal):
 1. \<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
hence "\<not> (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A"
[PROOF STATE]
proof (prove)
using this:
\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal (1 subgoal):
 1. \<not> (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A
[PROOF STEP]
unfolding GJ_P_def P_mult_b_def rank_A_def
[PROOF STATE]
proof (prove)
using this:
\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal (1 subgoal):
 1. \<not> (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))
[PROOF STEP]
using consistent_iarrays_def
[PROOF STATE]
proof (prove)
using this:
\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
consistent_iarrays ?A ?b = (let GJ = Gauss_Jordan_iarrays_PA ?A; rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv ?b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A)

goal (1 subgoal):
 1. \<not> (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
using this:
\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
consistent_iarrays ?A ?b = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA ?A) *iv ?b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA ?A) *iv ?b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA ?A)))))

goal (1 subgoal):
 1. \<not> (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<not> (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A

goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A

goal (1 subgoal):
 1. None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding solve_iarrays_def Let_def
[PROOF STATE]
proof (prove)
using this:
\<not> (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A

goal (1 subgoal):
 1. None = (if (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) then Some (solve_consistent_rref_iarrays (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))) (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b), set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)])) else None)
[PROOF STEP]
unfolding GJ_P_def P_mult_b_def rank_A_def
[PROOF STATE]
proof (prove)
using this:
\<not> (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))

goal (1 subgoal):
 1. None = (if (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) then Some (solve_consistent_rref_iarrays (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))) (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b), set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)])) else None)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
None = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal (1 subgoal):
 1. \<not> Option.is_none (solve A b) \<Longrightarrow> Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Option.is_none (solve A b) \<Longrightarrow> Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
assume not_none: "\<not> Option.is_none (solve A b)"
[PROOF STATE]
proof (state)
this:
\<not> Option.is_none (solve A b)

goal (1 subgoal):
 1. \<not> Option.is_none (solve A b) \<Longrightarrow> Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
show "Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define GJ_P where "GJ_P = Gauss_Jordan_iarrays_PA (matrix_to_iarray A)"
[PROOF STATE]
proof (state)
this:
GJ_P = Gauss_Jordan_iarrays_PA (matrix_to_iarray A)

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define P_mult_b where "P_mult_b = fst GJ_P *iv vec_to_iarray b"
[PROOF STATE]
proof (state)
this:
P_mult_b = fst GJ_P *iv vec_to_iarray b

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define rank_A where "rank_A = length [x\<leftarrow>IArray.list_of (snd GJ_P) . \<not> is_zero_iarray x]"
[PROOF STATE]
proof (state)
this:
rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ_P)))

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define GJ_transpose where "GJ_transpose = Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))"
[PROOF STATE]
proof (state)
this:
GJ_transpose = Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define basis where "basis = set (map (\<lambda>i. row_iarray i (fst GJ_transpose)) [rank_A..<ncols_iarray (matrix_to_iarray A)])"
[PROOF STATE]
proof (state)
this:
basis = set (map (\<lambda>i. row_iarray i (fst GJ_transpose)) [rank_A..<ncols_iarray (matrix_to_iarray A)])

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
define P_mult_b where "P_mult_b = fst GJ_P *iv vec_to_iarray b"
[PROOF STATE]
proof (state)
this:
P_mult_b = fst GJ_P *iv vec_to_iarray b

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
have consistent_Ab: "consistent A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent A b
[PROOF STEP]
using not_none
[PROOF STATE]
proof (prove)
using this:
\<not> Option.is_none (solve A b)

goal (1 subgoal):
 1. consistent A b
[PROOF STEP]
unfolding solve_def
[PROOF STATE]
proof (prove)
using this:
\<not> Option.is_none (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None)

goal (1 subgoal):
 1. consistent A b
[PROOF STEP]
unfolding Option.is_none_def
[PROOF STATE]
proof (prove)
using this:
(if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None) \<noteq> None

goal (1 subgoal):
 1. consistent A b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
consistent A b

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
hence "consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
using this:
consistent A b

goal (1 subgoal):
 1. consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
using matrix_to_iarray_consistent
[PROOF STATE]
proof (prove)
using this:
consistent A b
consistent ?A ?b = consistent_iarrays (matrix_to_iarray ?A) (vec_to_iarray ?b)

goal (1 subgoal):
 1. consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
hence "(if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A"
[PROOF STATE]
proof (prove)
using this:
consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal (1 subgoal):
 1. (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A
[PROOF STEP]
unfolding GJ_P_def P_mult_b_def rank_A_def
[PROOF STATE]
proof (prove)
using this:
consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal (1 subgoal):
 1. (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))
[PROOF STEP]
using consistent_iarrays_def
[PROOF STATE]
proof (prove)
using this:
consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
consistent_iarrays ?A ?b = (let GJ = Gauss_Jordan_iarrays_PA ?A; rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))); P_mult_b = fst GJ *iv ?b in (if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A)

goal (1 subgoal):
 1. (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
using this:
consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
consistent_iarrays ?A ?b = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA ?A) *iv ?b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA ?A) *iv ?b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA ?A)))))

goal (1 subgoal):
 1. (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
hence solve_iarrays_rw: "solve_iarrays (matrix_to_iarray A) (vec_to_iarray b) = Some (solve_consistent_rref_iarrays (snd GJ_P) P_mult_b, basis)"
[PROOF STATE]
proof (prove)
using this:
(if \<not> is_zero_iarray P_mult_b then greatest_not_zero P_mult_b + 1 else 0) \<le> rank_A

goal (1 subgoal):
 1. solve_iarrays (matrix_to_iarray A) (vec_to_iarray b) = Some (solve_consistent_rref_iarrays (snd GJ_P) P_mult_b, basis)
[PROOF STEP]
unfolding solve_iarrays_def Let_def P_mult_b_def GJ_P_def rank_A_def basis_def GJ_transpose_def
[PROOF STATE]
proof (prove)
using this:
(if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))

goal (1 subgoal):
 1. (if (if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))) then Some (solve_consistent_rref_iarrays (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))) (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b), set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)])) else None) = Some (solve_consistent_rref_iarrays (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))) (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b), set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
solve_iarrays (matrix_to_iarray A) (vec_to_iarray b) = Some (solve_consistent_rref_iarrays (snd GJ_P) P_mult_b, basis)

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
have snd_rw: "vec_to_iarray ` basis_null_space A = basis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray ` basis_null_space A = basis
[PROOF STEP]
unfolding basis_def GJ_transpose_def rank_A_def GJ_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray ` basis_null_space A = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding vec_to_iarray_basis_null_space
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_null_space_iarrays (matrix_to_iarray A) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding basis_null_space_iarrays_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding snd_Gauss_Jordan_iarrays_PA_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (transpose_iarray (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray A))))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding rank_iarrays_code[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [rank_iarray (transpose_iarray (matrix_to_iarray A))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding matrix_to_iarray_transpose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [rank_iarray (matrix_to_iarray (Finite_Cartesian_Product.transpose A))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding matrix_to_iarray_rank[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [rank (Finite_Cartesian_Product.transpose A)..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [rank A..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding rank_transpose[symmetric, of A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [rank (Finite_Cartesian_Product.transpose A)..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [rank (Finite_Cartesian_Product.transpose A)..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
vec_to_iarray ` basis_null_space A = basis

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
have fst_rw: "vec_to_iarray (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b))) = solve_consistent_rref_iarrays (snd GJ_P) P_mult_b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b))) = solve_consistent_rref_iarrays (snd GJ_P) P_mult_b
[PROOF STEP]
using vec_to_iarray_solve_consistent_rref[OF rref_Gauss_Jordan, of A "fst (Gauss_Jordan_PA A) *v b"]
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b))

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b))) = solve_consistent_rref_iarrays (snd GJ_P) P_mult_b
[PROOF STEP]
unfolding solve_system_def Let_def fst_conv
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b))

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (snd (Gauss_Jordan_PA A)) (snd (snd (Gauss_Jordan_PA A), fst (Gauss_Jordan_PA A) *v b))) = solve_consistent_rref_iarrays (snd GJ_P) P_mult_b
[PROOF STEP]
unfolding Gauss_Jordan_PA_eq snd_conv
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b))

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (snd GJ_P) P_mult_b
[PROOF STEP]
unfolding GJ_P_def P_mult_b_def
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b))

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))) (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b)
[PROOF STEP]
unfolding vec_to_iarray_matrix_matrix_mult
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b)

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))) (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b)
[PROOF STEP]
unfolding matrix_to_iarray_fst_Gauss_Jordan_PA[symmetric]
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b)

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))) (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b)
[PROOF STEP]
unfolding matrix_to_iarray_snd_Gauss_Jordan_PA[symmetric]
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b)

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (snd (Gauss_Jordan_PA A))) (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b)
[PROOF STEP]
unfolding Gauss_Jordan_PA_eq
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b)

goal (1 subgoal):
 1. vec_to_iarray (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b)) = solve_consistent_rref_iarrays (matrix_to_iarray (Gauss_Jordan A)) (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vec_to_iarray (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b))) = solve_consistent_rref_iarrays (snd GJ_P) P_mult_b

goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding solve_iarrays_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = Some (solve_consistent_rref_iarrays (snd GJ_P) P_mult_b, basis)
[PROOF STEP]
unfolding solve_def if_P[OF consistent_Ab] option.sel fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (vec_to_iarray (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b))), vec_to_iarray ` basis_null_space A) = Some (solve_consistent_rref_iarrays (snd GJ_P) P_mult_b, basis)
[PROOF STEP]
unfolding fst_rw snd_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some (solve_consistent_rref_iarrays (snd GJ_P) P_mult_b, basis) = Some (solve_consistent_rref_iarrays (snd GJ_P) P_mult_b, basis)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Some (vec_to_iarray (fst (the (solve A b))), vec_to_iarray ` snd (the (solve A b))) = solve_iarrays (matrix_to_iarray A) (vec_to_iarray b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mem_snd_map: "(\<exists>x. (x, y) \<in> S) \<longleftrightarrow> y \<in> snd ` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. (x, y) \<in> S) = (y \<in> snd ` S)
[PROOF STEP]
by force


[STATEMENT]
lemma filter_upt: assumes "l \<le> m" "m < n" shows "filter ((\<le>) m) [l..<n] = [m..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter ((\<le>) m) [l..<n] = [m..<n]
[PROOF STEP]
proof(insert assms, induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>l \<le> m; m < 0\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<0] = [m..<0]
 2. \<And>n. \<lbrakk>\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]; l \<le> m; m < Suc n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<Suc n] = [m..<Suc n]
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
l \<le> m
m < 0

goal (2 subgoals):
 1. \<lbrakk>l \<le> m; m < 0\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<0] = [m..<0]
 2. \<And>n. \<lbrakk>\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]; l \<le> m; m < Suc n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<Suc n] = [m..<Suc n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<le> m
m < 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
l \<le> m
m < 0

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

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]; l \<le> m; m < Suc n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<Suc n] = [m..<Suc n]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]; l \<le> m; m < Suc n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<Suc n] = [m..<Suc n]
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]
l \<le> m
m < Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]; l \<le> m; m < Suc n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<Suc n] = [m..<Suc n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]
l \<le> m
m < Suc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>l \<le> m; m < n\<rbrakk> \<Longrightarrow> filter ((\<le>) m) [l..<n] = [m..<n]
l \<le> m
m < Suc n

goal (1 subgoal):
 1. filter ((\<le>) m) [l..<Suc n] = [m..<Suc n]
[PROOF STEP]
by (cases "m = n", auto)
[PROOF STATE]
proof (state)
this:
filter ((\<le>) m) [l..<Suc n] = [m..<Suc n]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upt_append: "i < j \<Longrightarrow> j < k \<Longrightarrow> [i..<j]@[j..<k] = [i..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j < k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<k] = [i..<k]
[PROOF STEP]
proof(induct k arbitrary: j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>i < j; j < 0\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<0] = [i..<0]
 2. \<And>k j. \<lbrakk>\<And>j. \<lbrakk>i < j; j < k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<k] = [i..<k]; i < j; j < Suc k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<Suc k] = [i..<Suc k]
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
i < j
j < 0

goal (2 subgoals):
 1. \<And>j. \<lbrakk>i < j; j < 0\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<0] = [i..<0]
 2. \<And>k j. \<lbrakk>\<And>j. \<lbrakk>i < j; j < k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<k] = [i..<k]; i < j; j < Suc k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<Suc k] = [i..<Suc k]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < j
j < 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i < j
j < 0

goal (1 subgoal):
 1. [i..<j] @ [j..<0] = [i..<0]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[i..<j] @ [j..<0] = [i..<0]

goal (1 subgoal):
 1. \<And>k j. \<lbrakk>\<And>j. \<lbrakk>i < j; j < k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<k] = [i..<k]; i < j; j < Suc k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<Suc k] = [i..<Suc k]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k j. \<lbrakk>\<And>j. \<lbrakk>i < j; j < k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<k] = [i..<k]; i < j; j < Suc k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<Suc k] = [i..<Suc k]
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < ?j; ?j < k\<rbrakk> \<Longrightarrow> [i..<?j] @ [?j..<k] = [i..<k]
i < j
j < Suc k

goal (1 subgoal):
 1. \<And>k j. \<lbrakk>\<And>j. \<lbrakk>i < j; j < k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<k] = [i..<k]; i < j; j < Suc k\<rbrakk> \<Longrightarrow> [i..<j] @ [j..<Suc k] = [i..<Suc k]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i < ?j; ?j < k\<rbrakk> \<Longrightarrow> [i..<?j] @ [?j..<k] = [i..<k]
i < j
j < Suc k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < ?j; ?j < k\<rbrakk> \<Longrightarrow> [i..<?j] @ [?j..<k] = [i..<k]
i < j
j < Suc k

goal (1 subgoal):
 1. [i..<j] @ [j..<Suc k] = [i..<Suc k]
[PROOF STEP]
by (cases "j = k", auto)
[PROOF STATE]
proof (state)
this:
[i..<j] @ [j..<Suc k] = [i..<Suc k]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma IArray_sub[simp]: "(!!) as = (!) (IArray.list_of as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!!) as = (!) (IArray.list_of as)
[PROOF STEP]
by auto


[STATEMENT]
lemma subseqs_Cons[simp]: "subseqs (x#xs) = map (Cons x) (subseqs xs) @ subseqs xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseqs (x # xs) = map ((#) x) (subseqs xs) @ subseqs xs
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma singleton_mem_set_subseqs [simp]: "[x] \<in> set (subseqs xs) \<longleftrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([x] \<in> set (subseqs xs)) = (x \<in> set xs)
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma Cons_mem_set_subseqsD: "y#ys \<in> set (subseqs xs) \<Longrightarrow> y \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y # ys \<in> set (subseqs xs) \<Longrightarrow> y \<in> set xs
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma subseqs_subset: "ys \<in> set (subseqs xs) \<Longrightarrow> set ys \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<in> set (subseqs xs) \<Longrightarrow> set ys \<subseteq> set xs
[PROOF STEP]
by (metis Pow_iff image_eqI subseqs_powset)


[STATEMENT]
lemma Cons_mem_set_subseqs_Cons:
  "y#ys \<in> set (subseqs (x#xs)) \<longleftrightarrow> (y = x \<and> ys \<in> set (subseqs xs)) \<or> y#ys \<in> set (subseqs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y # ys \<in> set (subseqs (x # xs))) = (y = x \<and> ys \<in> set (subseqs xs) \<or> y # ys \<in> set (subseqs xs))
[PROOF STEP]
by auto


[STATEMENT]
lemma sorted_subseqs_sorted:
  "sorted xs \<Longrightarrow> ys \<in> set (subseqs xs) \<Longrightarrow> sorted ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> sorted ys
[PROOF STEP]
proof(induct xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>sorted []; ys \<in> set (subseqs [])\<rbrakk> \<Longrightarrow> sorted ys
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>sorted xs; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> sorted ys; sorted (a # xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> sorted ys
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
sorted []
ys \<in> set (subseqs [])

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>sorted []; ys \<in> set (subseqs [])\<rbrakk> \<Longrightarrow> sorted ys
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>sorted xs; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> sorted ys; sorted (a # xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> sorted ys
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted []
ys \<in> set (subseqs [])

goal (1 subgoal):
 1. sorted ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted ys

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>sorted xs; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> sorted ys; sorted (a # xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> sorted ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>sorted xs; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> sorted ys; sorted (a # xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> sorted ys
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<lbrakk>sorted xs_; ?ys \<in> set (subseqs xs_)\<rbrakk> \<Longrightarrow> sorted ?ys
sorted (a_ # xs_)
ys \<in> set (subseqs (a_ # xs_))

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>sorted xs; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> sorted ys; sorted (a # xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> sorted ys
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sorted xs_; ?ys \<in> set (subseqs xs_)\<rbrakk> \<Longrightarrow> sorted ?ys
sorted (a_ # xs_)
ys \<in> set (subseqs (a_ # xs_))

goal (1 subgoal):
 1. sorted ys
[PROOF STEP]
using subseqs_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sorted xs_; ?ys \<in> set (subseqs xs_)\<rbrakk> \<Longrightarrow> sorted ?ys
sorted (a_ # xs_)
ys \<in> set (subseqs (a_ # xs_))
?ys \<in> set (subseqs ?xs) \<Longrightarrow> set ?ys \<subseteq> set ?xs

goal (1 subgoal):
 1. sorted ys
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sorted ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subseqs_of_subseq: "ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs xs)
[PROOF STEP]
proof(induct xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. ys \<in> set (subseqs []) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs [])
 2. \<And>a xs ys. \<lbrakk>\<And>ys. ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ys \<in> set (subseqs [])

goal (2 subgoals):
 1. \<And>ys. ys \<in> set (subseqs []) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs [])
 2. \<And>a xs ys. \<lbrakk>\<And>ys. ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys \<in> set (subseqs [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ys \<in> set (subseqs [])

goal (1 subgoal):
 1. set (subseqs ys) \<subseteq> set (subseqs [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (subseqs ys) \<subseteq> set (subseqs [])

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (a # xs))
[PROOF STEP]
case IHx: (Cons x xs)
[PROOF STATE]
proof (state)
this:
?ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ?ys) \<subseteq> set (subseqs xs)
ys \<in> set (subseqs (x # xs))

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs xs); ys \<in> set (subseqs (a # xs))\<rbrakk> \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (a # xs))
[PROOF STEP]
from IHx.prems
[PROOF STATE]
proof (chain)
picking this:
ys \<in> set (subseqs (x # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ys \<in> set (subseqs (x # xs))

goal (1 subgoal):
 1. set (subseqs ys) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
proof(induct ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs []) \<subseteq> set (subseqs (x # xs))
 2. \<And>a ys. \<lbrakk>ys \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (x # xs)); a # ys \<in> set (subseqs (x # xs))\<rbrakk> \<Longrightarrow> set (subseqs (a # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<in> set (subseqs (x # xs))

goal (2 subgoals):
 1. [] \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs []) \<subseteq> set (subseqs (x # xs))
 2. \<And>a ys. \<lbrakk>ys \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (x # xs)); a # ys \<in> set (subseqs (x # xs))\<rbrakk> \<Longrightarrow> set (subseqs (a # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<in> set (subseqs (x # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] \<in> set (subseqs (x # xs))

goal (1 subgoal):
 1. set (subseqs []) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (subseqs []) \<subseteq> set (subseqs (x # xs))

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>ys \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (x # xs)); a # ys \<in> set (subseqs (x # xs))\<rbrakk> \<Longrightarrow> set (subseqs (a # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>ys \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (x # xs)); a # ys \<in> set (subseqs (x # xs))\<rbrakk> \<Longrightarrow> set (subseqs (a # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
case IHy: (Cons y ys)
[PROOF STATE]
proof (state)
this:
ys \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (x # xs))
y # ys \<in> set (subseqs (x # xs))

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>ys \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (x # xs)); a # ys \<in> set (subseqs (x # xs))\<rbrakk> \<Longrightarrow> set (subseqs (a # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
from IHy.prems[unfolded subseqs_Cons]
[PROOF STATE]
proof (chain)
picking this:
y # ys \<in> set (map ((#) x) (subseqs xs) @ subseqs xs)
[PROOF STEP]
consider "y = x" "ys \<in> set (subseqs xs)" | "y # ys \<in> set (subseqs xs)"
[PROOF STATE]
proof (prove)
using this:
y # ys \<in> set (map ((#) x) (subseqs xs) @ subseqs xs)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>y = x; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> thesis; y # ys \<in> set (subseqs xs) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>y = x; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> ?thesis; y # ys \<in> set (subseqs xs) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>ys \<in> set (subseqs (x # xs)) \<Longrightarrow> set (subseqs ys) \<subseteq> set (subseqs (x # xs)); a # ys \<in> set (subseqs (x # xs))\<rbrakk> \<Longrightarrow> set (subseqs (a # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>y = x; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> ?thesis; y # ys \<in> set (subseqs xs) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>y = x; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> ?thesis; y # ys \<in> set (subseqs xs) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>y = x; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
 2. y # ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
y = x
ys \<in> set (subseqs xs)

goal (2 subgoals):
 1. \<lbrakk>y = x; ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
 2. y # ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
with IHx.hyps
[PROOF STATE]
proof (chain)
picking this:
?ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ?ys) \<subseteq> set (subseqs xs)
y = x
ys \<in> set (subseqs xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs ?ys) \<subseteq> set (subseqs xs)
y = x
ys \<in> set (subseqs xs)

goal (1 subgoal):
 1. set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))

goal (1 subgoal):
 1. y # ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y # ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
y # ys \<in> set (subseqs xs)

goal (1 subgoal):
 1. y # ys \<in> set (subseqs xs) \<Longrightarrow> set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
from IHx.hyps[OF this]
[PROOF STATE]
proof (chain)
picking this:
set (subseqs (y # ys)) \<subseteq> set (subseqs xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (subseqs (y # ys)) \<subseteq> set (subseqs xs)

goal (1 subgoal):
 1. set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (subseqs (y # ys)) \<subseteq> set (subseqs (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (subseqs ys) \<subseteq> set (subseqs (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mem_set_subseqs_append: "xs \<in> set (subseqs ys) \<Longrightarrow> xs \<in> set (subseqs (zs @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> set (subseqs ys) \<Longrightarrow> xs \<in> set (subseqs (zs @ ys))
[PROOF STEP]
by (induct zs, auto)


[STATEMENT]
lemma Cons_mem_set_subseqs_append:
  "x \<in> set ys \<Longrightarrow> xs \<in> set (subseqs zs) \<Longrightarrow> x#xs \<in> set (subseqs (ys@zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs))
[PROOF STEP]
proof(induct ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set []; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ([] @ zs))
 2. \<And>a ys. \<lbrakk>\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs)); x \<in> set (a # ys); xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ((a # ys) @ zs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
x \<in> set []
xs \<in> set (subseqs zs)

goal (2 subgoals):
 1. \<lbrakk>x \<in> set []; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ([] @ zs))
 2. \<And>a ys. \<lbrakk>\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs)); x \<in> set (a # ys); xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ((a # ys) @ zs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set []
xs \<in> set (subseqs zs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> set []
xs \<in> set (subseqs zs)

goal (1 subgoal):
 1. x # xs \<in> set (subseqs ([] @ zs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # xs \<in> set (subseqs ([] @ zs))

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs)); x \<in> set (a # ys); xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ((a # ys) @ zs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs)); x \<in> set (a # ys); xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ((a # ys) @ zs))
[PROOF STEP]
case IH: (Cons y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs))
x \<in> set (y # ys)
xs \<in> set (subseqs zs)

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs)); x \<in> set (a # ys); xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ((a # ys) @ zs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs))
x \<in> set (y # ys)
xs \<in> set (subseqs zs)
[PROOF STEP]
consider "x = y" | "x \<in> set ys"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs))
x \<in> set (y # ys)
xs \<in> set (subseqs zs)

goal (1 subgoal):
 1. \<lbrakk>x = y \<Longrightarrow> thesis; x \<in> set ys \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = y \<Longrightarrow> ?thesis; x \<in> set ys \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a ys. \<lbrakk>\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs)); x \<in> set (a # ys); xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs ((a # ys) @ zs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = y \<Longrightarrow> ?thesis; x \<in> set ys \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = y \<Longrightarrow> ?thesis; x \<in> set ys \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> x # xs \<in> set (subseqs ((y # ys) @ zs))
 2. x \<in> set ys \<Longrightarrow> x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> x # xs \<in> set (subseqs ((y # ys) @ zs))
 2. x \<in> set ys \<Longrightarrow> x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs))
x \<in> set (y # ys)
xs \<in> set (subseqs zs)
x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> set ys; xs \<in> set (subseqs zs)\<rbrakk> \<Longrightarrow> x # xs \<in> set (subseqs (ys @ zs))
x \<in> set (y # ys)
xs \<in> set (subseqs zs)
x = y

goal (1 subgoal):
 1. x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
by (auto intro: mem_set_subseqs_append)
[PROOF STATE]
proof (state)
this:
x # xs \<in> set (subseqs ((y # ys) @ zs))

goal (1 subgoal):
 1. x \<in> set ys \<Longrightarrow> x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> set ys \<Longrightarrow> x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x \<in> set ys

goal (1 subgoal):
 1. x \<in> set ys \<Longrightarrow> x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
from IH.hyps[OF this IH.prems(2)]
[PROOF STATE]
proof (chain)
picking this:
x # xs \<in> set (subseqs (ys @ zs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x # xs \<in> set (subseqs (ys @ zs))

goal (1 subgoal):
 1. x # xs \<in> set (subseqs ((y # ys) @ zs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # xs \<in> set (subseqs ((y # ys) @ zs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x # xs \<in> set (subseqs ((y # ys) @ zs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Cons_mem_set_subseqs_sorted:
  "sorted xs \<Longrightarrow> y#ys \<in> set (subseqs xs) \<Longrightarrow> y#ys \<in> set (subseqs (filter (\<lambda>x. y \<le> x) xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; y # ys \<in> set (subseqs xs)\<rbrakk> \<Longrightarrow> y # ys \<in> set (subseqs (filter ((\<le>) y) xs))
[PROOF STEP]
by (induct xs) (auto simp: Let_def)


[STATEMENT]
lemma subseqs_map[simp]: "subseqs (map f xs) = map (map f) (subseqs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseqs (map f xs) = map (map f) (subseqs xs)
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma subseqs_of_indices: "map (map (nth xs)) (subseqs [0..<length xs]) = subseqs xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map (map ((!) [])) (subseqs [0..<length []]) = subseqs []
 2. \<And>a xs. map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs \<Longrightarrow> map (map ((!) (a # xs))) (subseqs [0..<length (a # xs)]) = subseqs (a # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. map (map ((!) [])) (subseqs [0..<length []]) = subseqs []
 2. \<And>a xs. map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs \<Longrightarrow> map (map ((!) (a # xs))) (subseqs [0..<length (a # xs)]) = subseqs (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (map ((!) [])) (subseqs [0..<length []]) = subseqs []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (map ((!) [])) (subseqs [0..<length []]) = subseqs []

goal (1 subgoal):
 1. \<And>a xs. map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs \<Longrightarrow> map (map ((!) (a # xs))) (subseqs [0..<length (a # xs)]) = subseqs (a # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs \<Longrightarrow> map (map ((!) (a # xs))) (subseqs [0..<length (a # xs)]) = subseqs (a # xs)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs

goal (1 subgoal):
 1. \<And>a xs. map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs \<Longrightarrow> map (map ((!) (a # xs))) (subseqs [0..<length (a # xs)]) = subseqs (a # xs)
[PROOF STEP]
from this[symmetric]
[PROOF STATE]
proof (chain)
picking this:
subseqs xs = map (map ((!) xs)) (subseqs [0..<length xs])
[PROOF STEP]
have "subseqs xs = map (map ((!) (x#xs))) (subseqs [Suc 0..<Suc (length xs)])"
[PROOF STATE]
proof (prove)
using this:
subseqs xs = map (map ((!) xs)) (subseqs [0..<length xs])

goal (1 subgoal):
 1. subseqs xs = map (map ((!) (x # xs))) (subseqs [Suc 0..<Suc (length xs)])
[PROOF STEP]
by (fold map_Suc_upt, simp)
[PROOF STATE]
proof (state)
this:
subseqs xs = map (map ((!) (x # xs))) (subseqs [Suc 0..<Suc (length xs)])

goal (1 subgoal):
 1. \<And>a xs. map (map ((!) xs)) (subseqs [0..<length xs]) = subseqs xs \<Longrightarrow> map (map ((!) (a # xs))) (subseqs [0..<length (a # xs)]) = subseqs (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subseqs xs = map (map ((!) (x # xs))) (subseqs [Suc 0..<Suc (length xs)])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
subseqs xs = map (map ((!) (x # xs))) (subseqs [Suc 0..<Suc (length xs)])

goal (1 subgoal):
 1. map (map ((!) (x # xs))) (subseqs [0..<length (x # xs)]) = subseqs (x # xs)
[PROOF STEP]
by (unfold length_Cons upt_conv_Cons[OF zero_less_Suc], simp)
[PROOF STATE]
proof (state)
this:
map (map ((!) (x # xs))) (subseqs [0..<length (x # xs)]) = subseqs (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subseq_of_lengthI[intro]:
  assumes "ys \<in> set (subseqs xs)" "length ys = n"
  shows "subseq_of_length n xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq_of_length n xs ys
[PROOF STEP]
by (insert assms, unfold subseq_of_length_def, auto)


[STATEMENT]
lemma subseq_of_lengthD[dest]:
  assumes "subseq_of_length n xs ys"
  shows "ys \<in> set (subseqs xs)" "length ys = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<in> set (subseqs xs) &&& length ys = n
[PROOF STEP]
by (insert assms, unfold subseq_of_length_def, auto)


[STATEMENT]
lemma subseq_of_length0[simp]: "subseq_of_length 0 xs ys \<longleftrightarrow> ys = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq_of_length 0 xs ys = (ys = [])
[PROOF STEP]
by auto


[STATEMENT]
lemma subseq_of_length_Nil[simp]: "subseq_of_length n [] ys \<longleftrightarrow> n = 0 \<and> ys = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subseq_of_length n [] ys = (n = 0 \<and> ys = [])
[PROOF STEP]
by (auto simp: subseq_of_length_def)