[STATEMENT]
lemma unifiers_Pairs:
  assumes
    "finite AAA" and
    "\<forall>AA \<in> AAA. finite AA"
  shows "unifiers (set (Pairs AAA)) = {\<sigma>. is_unifiers \<sigma> AAA}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifiers (set (Pairs AAA)) = {\<sigma>. is_unifiers \<sigma> AAA}
[PROOF STEP]
proof (rule; rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> unifiers (set (Pairs AAA)) \<Longrightarrow> x \<in> {\<sigma>. is_unifiers \<sigma> AAA}
 2. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
fix \<sigma> :: "('a, 'b) subst"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> unifiers (set (Pairs AAA)) \<Longrightarrow> x \<in> {\<sigma>. is_unifiers \<sigma> AAA}
 2. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
assume asm: "\<sigma> \<in> unifiers (set (Pairs AAA))"
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> unifiers (set (Pairs AAA))

goal (2 subgoals):
 1. \<And>x. x \<in> unifiers (set (Pairs AAA)) \<Longrightarrow> x \<in> {\<sigma>. is_unifiers \<sigma> AAA}
 2. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
have "\<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
fix AA :: "('a, 'b) term set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
assume asm': "AA \<in> AAA"
[PROOF STATE]
proof (state)
this:
AA \<in> AAA

goal (1 subgoal):
 1. \<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AA \<in> AAA
[PROOF STEP]
have "\<forall>p \<in> set (pairs (compare_linorder.sorted_list_of_set AA)).
      subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>"
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA

goal (1 subgoal):
 1. \<forall>p\<in>set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>
[PROOF STEP]
using assms asm
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> unifiers (set (Pairs AAA))

goal (1 subgoal):
 1. \<forall>p\<in>set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>
[PROOF STEP]
unfolding Pairs_def
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> unifiers (set (concat (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))))

goal (1 subgoal):
 1. \<forall>p\<in>set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>

goal (1 subgoal):
 1. \<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>
[PROOF STEP]
have "\<forall>A \<in> AA. \<forall>B \<in> AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>

goal (1 subgoal):
 1. \<forall>A\<in>AA. \<forall>B\<in>AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
using assms asm'
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (pairs (compare_linorder.sorted_list_of_set AA)). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>
finite AAA
\<forall>AA\<in>AAA. finite AA
AA \<in> AAA

goal (1 subgoal):
 1. \<forall>A\<in>AA. \<forall>B\<in>AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
unfolding unifies_all_pairs_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (compare_linorder.sorted_list_of_set AA). \<forall>b\<in>set (compare_linorder.sorted_list_of_set AA). subst_atm_abbrev a \<sigma> = subst_atm_abbrev b \<sigma>
finite AAA
\<forall>AA\<in>AAA. finite AA
AA \<in> AAA

goal (1 subgoal):
 1. \<forall>A\<in>AA. \<forall>B\<in>AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
using compare_linorder.sorted_list_of_set
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (compare_linorder.sorted_list_of_set AA). \<forall>b\<in>set (compare_linorder.sorted_list_of_set AA). subst_atm_abbrev a \<sigma> = subst_atm_abbrev b \<sigma>
finite AAA
\<forall>AA\<in>AAA. finite AA
AA \<in> AAA
finite ?A \<Longrightarrow> set (compare_linorder.sorted_list_of_set ?A) = ?A
compare_linorder.sorted (compare_linorder.sorted_list_of_set ?A)
distinct (compare_linorder.sorted_list_of_set ?A)

goal (1 subgoal):
 1. \<forall>A\<in>AA. \<forall>B\<in>AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>AA. \<forall>B\<in>AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>

goal (1 subgoal):
 1. \<And>AA. AA \<in> AAA \<Longrightarrow> card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>AA. \<forall>B\<in>AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
show "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>AA. \<forall>B\<in>AA. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
by (smt imageE card.empty card_Suc_eq card_mono finite.intros(1) finite_insert le_SucI
           singletonI subsetI)
[PROOF STATE]
proof (state)
this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?AA1 \<in> AAA \<Longrightarrow> card (?AA1 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (2 subgoals):
 1. \<And>x. x \<in> unifiers (set (Pairs AAA)) \<Longrightarrow> x \<in> {\<sigma>. is_unifiers \<sigma> AAA}
 2. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?AA1 \<in> AAA \<Longrightarrow> card (?AA1 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
show "\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}"
[PROOF STATE]
proof (prove)
using this:
?AA1 \<in> AAA \<Longrightarrow> card (?AA1 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (1 subgoal):
 1. \<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?AA1 \<in> AAA \<Longrightarrow> card (?AA1 \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
finite AAA
\<forall>AA\<in>AAA. finite AA

goal (1 subgoal):
 1. \<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
[PROOF STEP]
by (auto simp: is_unifiers_def is_unifier_def subst_atms_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
fix \<sigma> :: "('a, 'b) subst"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
assume asm: "\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}"
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
fix AB_pairs A B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
assume
      "AB_pairs \<in> set (compare_linorder.sorted_list_of_set
         ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))" and
      "(A, B) \<in> set AB_pairs"
[PROOF STATE]
proof (state)
this:
AB_pairs \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))
(A, B) \<in> set AB_pairs

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AB_pairs \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))
(A, B) \<in> set AB_pairs
[PROOF STEP]
have "\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA"
[PROOF STATE]
proof (prove)
using this:
AB_pairs \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))
(A, B) \<in> set AB_pairs

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
AB_pairs \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))
(A, B) \<in> set AB_pairs
finite AAA
\<forall>AA\<in>AAA. finite AA

goal (1 subgoal):
 1. \<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
by (simp add: in_pairs_sorted_list_of_set_in_set)
[PROOF STATE]
proof (state)
this:
\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA
[PROOF STEP]
obtain AA where
     a: "AA \<in> AAA" "A \<in> AA" "B \<in> AA"
[PROOF STATE]
proof (prove)
using this:
\<exists>AA. AA \<in> AAA \<and> A \<in> AA \<and> B \<in> AA

goal (1 subgoal):
 1. (\<And>AA. \<lbrakk>AA \<in> AAA; A \<in> AA; B \<in> AA\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AA \<in> AAA
A \<in> AA
B \<in> AA

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
from a assms asm
[PROOF STATE]
proof (chain)
picking this:
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
[PROOF STEP]
have card_AA_\<sigma>: "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0"
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
unfolding is_unifiers_def is_unifier_def subst_atms_def
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. \<forall>AA\<in>AAA. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> 1}

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
have "subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
proof (cases "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
 2. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0

goal (2 subgoals):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
 2. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0

goal (2 subgoals):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
 2. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
have "subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
[PROOF STEP]
using a assms asm card_AA_\<sigma>
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (1 subgoal):
 1. subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>

goal (2 subgoals):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
 2. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>

goal (2 subgoals):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
 2. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
have "subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
[PROOF STEP]
using a assms asm card_AA_\<sigma>
[PROOF STATE]
proof (prove)
using this:
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (1 subgoal):
 1. subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>

goal (2 subgoals):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
 2. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0
subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0
subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>

goal (1 subgoal):
 1. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
using a assms asm card_AA_\<sigma>
[PROOF STATE]
proof (prove)
using this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = Suc 0
subst_atm_abbrev A \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
subst_atm_abbrev B \<sigma> \<in> AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (1 subgoal):
 1. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
by (metis (no_types, lifting) card_Suc_eq singletonD)
[PROOF STATE]
proof (state)
this:
subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0
[PROOF STEP]
have "card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0"
[PROOF STATE]
proof (prove)
using this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0
[PROOF STEP]
using a assms asm card_AA_\<sigma>
[PROOF STATE]
proof (prove)
using this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0

goal (1 subgoal):
 1. card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<noteq> Suc 0 \<Longrightarrow> subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0

goal (1 subgoal):
 1. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
using a assms asm card_AA_\<sigma>
[PROOF STATE]
proof (prove)
using this:
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) = 0
AA \<in> AAA
A \<in> AA
B \<in> AA
finite AAA
\<forall>AA\<in>AAA. finite AA
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA}
card (AA \<cdot>\<^sub>s\<^sub>e\<^sub>t \<sigma>) \<le> Suc 0

goal (1 subgoal):
 1. subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subst_atm_abbrev A \<sigma> = subst_atm_abbrev B \<sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?AB_pairs3 \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA)); (?A3, ?B3) \<in> set ?AB_pairs3\<rbrakk> \<Longrightarrow> subst_atm_abbrev ?A3 \<sigma> = subst_atm_abbrev ?B3 \<sigma>

goal (1 subgoal):
 1. \<And>x. x \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<Longrightarrow> x \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?AB_pairs3 \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA)); (?A3, ?B3) \<in> set ?AB_pairs3\<rbrakk> \<Longrightarrow> subst_atm_abbrev ?A3 \<sigma> = subst_atm_abbrev ?B3 \<sigma>
[PROOF STEP]
show "\<sigma> \<in> unifiers (set (Pairs AAA))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?AB_pairs3 \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA)); (?A3, ?B3) \<in> set ?AB_pairs3\<rbrakk> \<Longrightarrow> subst_atm_abbrev ?A3 \<sigma> = subst_atm_abbrev ?B3 \<sigma>

goal (1 subgoal):
 1. \<sigma> \<in> unifiers (set (Pairs AAA))
[PROOF STEP]
unfolding Pairs_def unifiers_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?AB_pairs3 \<in> set (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA)); (?A3, ?B3) \<in> set ?AB_pairs3\<rbrakk> \<Longrightarrow> subst_atm_abbrev ?A3 \<sigma> = subst_atm_abbrev ?B3 \<sigma>

goal (1 subgoal):
 1. \<sigma> \<in> {\<sigma>. \<forall>p\<in>set (concat (compare_linorder.sorted_list_of_set ((pairs \<circ> compare_linorder.sorted_list_of_set) ` AAA))). subst_atm_abbrev (fst p) \<sigma> = subst_atm_abbrev (snd p) \<sigma>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> unifiers (set (Pairs AAA))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mgu_sets_is_imgu:
  fixes AAA :: "('a :: compare, nat) term set set" and \<sigma> :: "('a, nat) subst"
  assumes fin: "finite AAA" "\<forall>AA \<in> AAA. finite AA" and "mgu_sets AAA = Some \<sigma>"
  shows "is_imgu \<sigma> AAA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IsaFoR_Term.is_imgu \<sigma> AAA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. IsaFoR_Term.is_imgu \<sigma> AAA
[PROOF STEP]
have "Unifiers.is_imgu \<sigma> (set (Pairs AAA))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Unifiers.is_imgu \<sigma> (set (Pairs AAA))
[PROOF STEP]
using assms unify_sound
[PROOF STATE]
proof (prove)
using this:
finite AAA
\<forall>AA\<in>AAA. finite AA
mgu_sets AAA = Some \<sigma>
unify ?E [] = Some ?cs \<Longrightarrow> Unifiers.is_imgu (subst_of ?cs) (set ?E)

goal (1 subgoal):
 1. Unifiers.is_imgu \<sigma> (set (Pairs AAA))
[PROOF STEP]
unfolding mgu_sets_def
[PROOF STATE]
proof (prove)
using this:
finite AAA
\<forall>AA\<in>AAA. finite AA
map_option subst_of (unify (Pairs AAA) []) = Some \<sigma>
unify ?E [] = Some ?cs \<Longrightarrow> Unifiers.is_imgu (subst_of ?cs) (set ?E)

goal (1 subgoal):
 1. Unifiers.is_imgu \<sigma> (set (Pairs AAA))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Unifiers.is_imgu \<sigma> (set (Pairs AAA))

goal (1 subgoal):
 1. IsaFoR_Term.is_imgu \<sigma> AAA
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Unifiers.is_imgu \<sigma> (set (Pairs AAA))

goal (1 subgoal):
 1. IsaFoR_Term.is_imgu \<sigma> AAA
[PROOF STEP]
unfolding Unifiers.is_imgu_def is_imgu_def unifiers_Pairs[OF fin]
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> {\<sigma>. is_unifiers \<sigma> AAA} \<and> (\<forall>\<tau>\<in>{\<sigma>. is_unifiers \<sigma> AAA}. \<tau> = comp_subst_abbrev \<sigma> \<tau>)

goal (1 subgoal):
 1. is_unifiers \<sigma> AAA \<and> (\<forall>\<tau>. is_unifiers \<tau> AAA \<longrightarrow> \<tau> = comp_subst_abbrev \<sigma> \<tau>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
IsaFoR_Term.is_imgu \<sigma> AAA

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma kbo_code[code]: "kbo s t =
  (let wt = weight t; ws = weight s in
  if vars_term_ms (KBO.SCF t) \<subseteq># vars_term_ms (KBO.SCF s) \<and> wt \<le> ws
  then
    (if wt < ws then (True, True)
    else
      (case s of
        Var y \<Rightarrow> (False, case t of Var x \<Rightarrow> True | Fun g ts \<Rightarrow> ts = [] \<and> least weights g)
      | Fun f ss \<Rightarrow>
          (case t of
            Var x \<Rightarrow> (True, True)
          | Fun g ts \<Rightarrow>
              if pr_strict weights (f, length ss) (g, length ts) then (True, True)
              else if (f, length ss) = (g, length ts) then lex_ext_unbounded kbo ss ts
              else (False, False))))
  else (False, False))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kbo s t = (let wt = weight t; ws = weight s in if vars_term_ms (KBO.SCF t) \<subseteq># vars_term_ms (KBO.SCF s) \<and> wt \<le> ws then if wt < ws then (True, True) else case s of Var y \<Rightarrow> (False, case t of Var x \<Rightarrow> True | Fun g ts \<Rightarrow> ts = [] \<and> least weights g) | Fun f ss \<Rightarrow> case t of Var x \<Rightarrow> (True, True) | Fun g ts \<Rightarrow> if pr_strict weights (f, length ss) (g, length ts) then (True, True) else if (f, length ss) = (g, length ts) then lex_ext_unbounded kbo ss ts else (False, False) else (False, False))
[PROOF STEP]
by (subst KBO.kbo.simps) (auto simp: Let_def split: term.splits)


[STATEMENT]
lemma less_kbo_gtotal: "ground s \<Longrightarrow> ground t \<Longrightarrow> s = t \<or> less_kbo s t \<or> less_kbo t s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ground s; ground t\<rbrakk> \<Longrightarrow> s = t \<or> less_kbo s t \<or> less_kbo t s
[PROOF STEP]
unfolding less_kbo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ground s; ground t\<rbrakk> \<Longrightarrow> s = t \<or> fst (kbo t s) \<or> fst (kbo s t)
[PROOF STEP]
using KBO.S_ground_total
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(pr_strict weights)\<^sup>=\<^sup>= = (pr_strict weights)\<^sup>=\<^sup>=; \<And>f g. \<lbrakk>f \<in> ?F; g \<in> ?F\<rbrakk> \<Longrightarrow> f = g \<or> pr_strict weights f g \<or> pr_strict weights g f; funas_term ?s \<subseteq> ?F; ground ?s; funas_term ?t \<subseteq> ?F; ground ?t\<rbrakk> \<Longrightarrow> ?s = ?t \<or> fst (kbo ?s ?t) \<or> fst (kbo ?t ?s)

goal (1 subgoal):
 1. \<lbrakk>ground s; ground t\<rbrakk> \<Longrightarrow> s = t \<or> fst (kbo t s) \<or> fst (kbo s t)
[PROOF STEP]
by (metis pr_strict_total subset_UNIV)


[STATEMENT]
lemma less_kbo_subst:
  fixes \<sigma> :: "('f :: weighted, 'v) subst"
  shows "less_kbo s t \<Longrightarrow> less_kbo (s \<cdot> \<sigma>) (t \<cdot> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_kbo s t \<Longrightarrow> less_kbo (subst_atm_abbrev s \<sigma>) (subst_atm_abbrev t \<sigma>)
[PROOF STEP]
unfolding less_kbo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (kbo t s) \<Longrightarrow> fst (kbo (subst_atm_abbrev t \<sigma>) (subst_atm_abbrev s \<sigma>))
[PROOF STEP]
by (rule KBO.S_subst)


[STATEMENT]
lemma wfP_less_kbo: "wfP less_kbo"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wfP less_kbo
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wfP less_kbo
[PROOF STEP]
have "SN {(x, y). fst (kbo x y)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SN {(x, y). fst (kbo x y)}
[PROOF STEP]
using pr_strict_asymp
[PROOF STATE]
proof (prove)
using this:
asymp (pr_strict weights)

goal (1 subgoal):
 1. SN {(x, y). fst (kbo x y)}
[PROOF STEP]
by (fastforce simp: asymp.simps irreflp_def intro!: KBO.S_SN scf_ok)
[PROOF STATE]
proof (state)
this:
SN {(x, y). fst (kbo x y)}

goal (1 subgoal):
 1. wfP less_kbo
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
SN {(x, y). fst (kbo x y)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
SN {(x, y). fst (kbo x y)}

goal (1 subgoal):
 1. wfP less_kbo
[PROOF STEP]
unfolding SN_iff_wf wfP_def
[PROOF STATE]
proof (prove)
using this:
wf ({(x, y). fst (kbo x y)}\<inverse>)

goal (1 subgoal):
 1. wf {(x, y). less_kbo x y}
[PROOF STEP]
by (rule wf_subset) (auto simp: less_kbo_def)
[PROOF STATE]
proof (state)
this:
wfP less_kbo

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_trm_extension: "{(s,t). less_kbo s t} \<subseteq> leq_term"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s, t). less_kbo s t} \<subseteq> leq_term
[PROOF STEP]
unfolding leq_term_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(s, t). less_kbo s t} \<subseteq> (SOME leq. {(x, y). less_kbo x y} \<subseteq> leq \<and> Well_order leq \<and> Field leq = UNIV)
[PROOF STEP]
by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto


[STATEMENT]
lemma less_trm_well_order: "well_order leq_term"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_order leq_term
[PROOF STEP]
unfolding leq_term_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_order (SOME leq. {(x, y). less_kbo x y} \<subseteq> leq \<and> Well_order leq \<and> Field leq = UNIV)
[PROOF STEP]
by (rule someI2_ex[OF total_well_order_extension[OF wfP_less_kbo[unfolded wfP_def]]]) auto


[STATEMENT]
lemma leq_term_minus_Id: "leq_term - Id = {(x,y). x < y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. leq_term - Id = {(x, y). x < y}
[PROOF STEP]
using less_trm_well_order
[PROOF STATE]
proof (prove)
using this:
well_order leq_term

goal (1 subgoal):
 1. leq_term - Id = {(x, y). x < y}
[PROOF STEP]
unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def less_term_def less_eq_term_def
[PROOF STATE]
proof (prove)
using this:
((preorder_on UNIV leq_term \<and> (\<forall>x y. (x, y) \<in> leq_term \<longrightarrow> (y, x) \<in> leq_term \<longrightarrow> x = y)) \<and> total leq_term) \<and> wf (leq_term - Id)

goal (1 subgoal):
 1. leq_term - Id = {(x, y). strict (in_rel leq_term) x y}
[PROOF STEP]
by auto


[STATEMENT]
lemma less_term_alt: "(<) = in_rel (leq_term - Id)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (<) = in_rel (leq_term - Id)
[PROOF STEP]
by (simp add: in_rel_Collect_case_prod_eq leq_term_minus_Id)


[STATEMENT]
lemma ground_less_less_kbo: "ground s \<Longrightarrow> ground t \<Longrightarrow> s < t \<Longrightarrow> less_kbo s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ground s; ground t; s < t\<rbrakk> \<Longrightarrow> less_kbo s t
[PROOF STEP]
using less_kbo_gtotal[of s t] less_trm_extension
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ground s; ground t\<rbrakk> \<Longrightarrow> s = t \<or> less_kbo s t \<or> less_kbo t s
{(s, t). less_kbo s t} \<subseteq> leq_term

goal (1 subgoal):
 1. \<lbrakk>ground s; ground t; s < t\<rbrakk> \<Longrightarrow> less_kbo s t
[PROOF STEP]
by (auto simp: less_term_def less_eq_term_def)


[STATEMENT]
lemma less_kbo_less: "less_kbo s t \<Longrightarrow> s < t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_kbo s t \<Longrightarrow> s < t
[PROOF STEP]
using less_trm_extension
[PROOF STATE]
proof (prove)
using this:
{(s, t). less_kbo s t} \<subseteq> leq_term

goal (1 subgoal):
 1. less_kbo s t \<Longrightarrow> s < t
[PROOF STEP]
by (auto simp: less_term_alt less_kbo_def KBO.S_irrefl)


[STATEMENT]
lemma is_ground_atm_ground: "is_ground_atm t \<longleftrightarrow> ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ground_atm t = ground t
[PROOF STEP]
unfolding is_ground_atm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>\<sigma>. t = subst_atm_abbrev t \<sigma>) = ground t
[PROOF STEP]
by (induct t) (fastforce simp: in_set_conv_nth list_eq_iff_nth_eq)+


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


[STATEMENT]
lemma index_mat_multrow_mat[simp]:
  "i < n \<Longrightarrow> j < n \<Longrightarrow> multrow_mat n k a $$ (i,j) = (if k = i \<and> k = j then a else if i = j
     then 1 else 0)"
  "dim_row (multrow_mat n k a) = n" "dim_col (multrow_mat n k a) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < n; j < n\<rbrakk> \<Longrightarrow> multrow_mat n k a $$ (i, j) = (if k = i \<and> k = j then a else if i = j then 1::'a else (0::'a))) &&& dim_row (multrow_mat n k a) = n &&& dim_col (multrow_mat n k a) = n
[PROOF STEP]
unfolding multrow_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < n; j < n\<rbrakk> \<Longrightarrow> mat n n (\<lambda>(i, j). if k = i \<and> k = j then a else if i = j then 1::'a else (0::'a)) $$ (i, j) = (if k = i \<and> k = j then a else if i = j then 1::'a else (0::'a))) &&& dim_row (mat n n (\<lambda>(i, j). if k = i \<and> k = j then a else if i = j then 1::'a else (0::'a))) = n &&& dim_col (mat n n (\<lambda>(i, j). if k = i \<and> k = j then a else if i = j then 1::'a else (0::'a))) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma index_mat_swaprows[simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> swaprows k l A $$ (i,j) = (if k = i then A $$ (l,j) else
    if l = i then A $$ (k,j) else A $$ (i,j))"
  "dim_row (swaprows k l A) = dim_row A" "dim_col (swaprows k l A) = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> swaprows k l A $$ (i, j) = (if k = i then A $$ (l, j) else if l = i then A $$ (k, j) else A $$ (i, j))) &&& dim_row (swaprows k l A) = dim_row A &&& dim_col (swaprows k l A) = dim_col A
[PROOF STEP]
unfolding mat_swaprows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then A $$ (l, j) else if l = i then A $$ (k, j) else A $$ (i, j)) $$ (i, j) = (if k = i then A $$ (l, j) else if l = i then A $$ (k, j) else A $$ (i, j))) &&& dim_row (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then A $$ (l, j) else if l = i then A $$ (k, j) else A $$ (i, j))) = dim_row A &&& dim_col (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then A $$ (l, j) else if l = i then A $$ (k, j) else A $$ (i, j))) = dim_col A
[PROOF STEP]
by auto


[STATEMENT]
lemma index_mat_swaprows_mat[simp]:
  "i < n \<Longrightarrow> j < n \<Longrightarrow> swaprows_mat n k l $$ (i,j) =
    (if k = i \<and> l = j \<or> k = j \<and> l = i \<or> i = j \<and> i \<noteq> k \<and> i \<noteq> l then 1 else 0)"
  "dim_row (swaprows_mat n k l) = n" "dim_col (swaprows_mat n k l) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < n; j < n\<rbrakk> \<Longrightarrow> swaprows_mat n k l $$ (i, j) = (if k = i \<and> l = j \<or> k = j \<and> l = i \<or> i = j \<and> i \<noteq> k \<and> i \<noteq> l then 1::'a else (0::'a))) &&& dim_row (swaprows_mat n k l) = n &&& dim_col (swaprows_mat n k l) = n
[PROOF STEP]
unfolding swaprows_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < n; j < n\<rbrakk> \<Longrightarrow> mat n n (\<lambda>(i, j). if k = i \<and> l = j \<or> k = j \<and> l = i \<or> i = j \<and> i \<noteq> k \<and> i \<noteq> l then 1::'a else (0::'a)) $$ (i, j) = (if k = i \<and> l = j \<or> k = j \<and> l = i \<or> i = j \<and> i \<noteq> k \<and> i \<noteq> l then 1::'a else (0::'a))) &&& dim_row (mat n n (\<lambda>(i, j). if k = i \<and> l = j \<or> k = j \<and> l = i \<or> i = j \<and> i \<noteq> k \<and> i \<noteq> l then 1::'b else (0::'b))) = n &&& dim_col (mat n n (\<lambda>(i, j). if k = i \<and> l = j \<or> k = j \<and> l = i \<or> i = j \<and> i \<noteq> k \<and> i \<noteq> l then 1::'c else (0::'c))) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma index_mat_addrow[simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> mat_addrow_gen ad mul a k l A $$ (i,j) = (if k = i then
    ad (mul a (A $$ (l,j))) (A $$ (i,j)) else A $$ (i,j))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> mat_addrow_gen ad mul a i l A $$ (i,j) = ad (mul a (A $$ (l,j))) (A $$ (i,j))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> k \<noteq> i \<Longrightarrow> mat_addrow_gen ad mul a k l A $$ (i,j) = A $$(i,j)"
  "dim_row (mat_addrow_gen ad mul a k l A) = dim_row A" "dim_col (mat_addrow_gen ad mul a k l A) = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat_addrow_gen ad mul a k l A $$ (i, j) = (if k = i then ad (mul a (A $$ (l, j))) (A $$ (i, j)) else A $$ (i, j))) &&& (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat_addrow_gen ad mul a i l A $$ (i, j) = ad (mul a (A $$ (l, j))) (A $$ (i, j)))) &&& (\<lbrakk>i < dim_row A; j < dim_col A; k \<noteq> i\<rbrakk> \<Longrightarrow> mat_addrow_gen ad mul a k l A $$ (i, j) = A $$ (i, j)) &&& dim_row (mat_addrow_gen ad mul a k l A) = dim_row A &&& dim_col (mat_addrow_gen ad mul a k l A) = dim_col A
[PROOF STEP]
unfolding mat_addrow_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then ad (mul a (A $$ (l, j))) (A $$ (i, j)) else A $$ (i, j)) $$ (i, j) = (if k = i then ad (mul a (A $$ (l, j))) (A $$ (i, j)) else A $$ (i, j))) &&& (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(ia, j). if i = ia then ad (mul a (A $$ (l, j))) (A $$ (ia, j)) else A $$ (ia, j)) $$ (i, j) = ad (mul a (A $$ (l, j))) (A $$ (i, j)))) &&& (\<lbrakk>i < dim_row A; j < dim_col A; k \<noteq> i\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then ad (mul a (A $$ (l, j))) (A $$ (i, j)) else A $$ (i, j)) $$ (i, j) = A $$ (i, j)) &&& dim_row (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then ad (mul a (A $$ (l, j))) (A $$ (i, j)) else A $$ (i, j))) = dim_row A &&& dim_col (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then ad (mul a (A $$ (l, j))) (A $$ (i, j)) else A $$ (i, j))) = dim_col A
[PROOF STEP]
by auto


[STATEMENT]
lemma index_mat_addrow_mat[simp]:
  "i < n \<Longrightarrow> j < n \<Longrightarrow> addrow_mat n a k l $$ (i,j) =
    (if k = i \<and> l = j then (+) a else id) (if i = j then 1 else 0)"
  "dim_row (addrow_mat n a k l) = n" "dim_col (addrow_mat n a k l) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < n; j < n\<rbrakk> \<Longrightarrow> addrow_mat n a k l $$ (i, j) = (if k = i \<and> l = j then (+) a else id) (if i = j then 1::'a else (0::'a))) &&& dim_row (addrow_mat n a k l) = n &&& dim_col (addrow_mat n a k l) = n
[PROOF STEP]
unfolding addrow_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < n; j < n\<rbrakk> \<Longrightarrow> mat n n (\<lambda>(i, j). (if k = i \<and> l = j then (+) a else id) (if i = j then 1::'a else (0::'a))) $$ (i, j) = (if k = i \<and> l = j then (+) a else id) (if i = j then 1::'a else (0::'a))) &&& dim_row (mat n n (\<lambda>(i, j). (if k = i \<and> l = j then (+) a else id) (if i = j then 1::'a else (0::'a)))) = n &&& dim_col (mat n n (\<lambda>(i, j). (if k = i \<and> l = j then (+) a else id) (if i = j then 1::'a else (0::'a)))) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma multrow_carrier[simp]: "(mat_multrow_gen mul k a A \<in> carrier_mat n nc) = (A \<in> carrier_mat n nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_multrow_gen mul k a A \<in> carrier_mat n nc) = (A \<in> carrier_mat n nc)
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_multrow_gen mul k a A \<in> {m. dim_row m = n \<and> dim_col m = nc}) = (A \<in> {m. dim_row m = n \<and> dim_col m = nc})
[PROOF STEP]
by fastforce


[STATEMENT]
lemma multrow_mat_carrier[simp]: "multrow_mat n k a \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a \<in> carrier_mat n n
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a \<in> {m. dim_row m = n \<and> dim_col m = n}
[PROOF STEP]
by auto


[STATEMENT]
lemma addrow_mat_carrier[simp]: "addrow_mat n a k l \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l \<in> carrier_mat n n
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l \<in> {m. dim_row m = n \<and> dim_col m = n}
[PROOF STEP]
by auto


[STATEMENT]
lemma swaprows_mat_carrier[simp]: "swaprows_mat n k l \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l \<in> carrier_mat n n
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l \<in> {m. dim_row m = n \<and> dim_col m = n}
[PROOF STEP]
by auto


[STATEMENT]
lemma swaprows_carrier[simp]: "(swaprows k l A \<in> carrier_mat n nc) = (A \<in> carrier_mat n nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (swaprows k l A \<in> carrier_mat n nc) = (A \<in> carrier_mat n nc)
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (swaprows k l A \<in> {m. dim_row m = n \<and> dim_col m = nc}) = (A \<in> {m. dim_row m = n \<and> dim_col m = nc})
[PROOF STEP]
by fastforce


[STATEMENT]
lemma addrow_carrier[simp]: "(mat_addrow_gen ad mul a k l A \<in> carrier_mat n nc) = (A \<in> carrier_mat n nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_addrow_gen ad mul a k l A \<in> carrier_mat n nc) = (A \<in> carrier_mat n nc)
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_addrow_gen ad mul a k l A \<in> {m. dim_row m = n \<and> dim_col m = nc}) = (A \<in> {m. dim_row m = n \<and> dim_col m = nc})
[PROOF STEP]
by fastforce


[STATEMENT]
lemma row_multrow:  "k \<noteq> i \<Longrightarrow> i < n \<Longrightarrow> row (multrow_mat n k a) i = unit_vec n i"
  "k < n \<Longrightarrow> row (multrow_mat n k a) k = a \<cdot>\<^sub>v unit_vec n k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>k \<noteq> i; i < n\<rbrakk> \<Longrightarrow> row (multrow_mat n k a) i = unit_vec n i) &&& (k < n \<Longrightarrow> row (multrow_mat n k a) k = a \<cdot>\<^sub>v unit_vec n k)
[PROOF STEP]
by (rule eq_vecI, auto)


[STATEMENT]
lemma multrow_mat: assumes A: "A \<in> carrier_mat n nc"
  shows "multrow k a A = multrow_mat n k a * A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow k a A = multrow_mat n k a * A
[PROOF STEP]
by (rule eq_matI, insert A, auto simp: row_multrow smult_scalar_prod_distrib[of _ n])


[STATEMENT]
lemma row_addrow:
  "k \<noteq> i \<Longrightarrow> i < n \<Longrightarrow> row (addrow_mat n a k l) i = unit_vec n i"
  "k < n \<Longrightarrow> l < n \<Longrightarrow> row (addrow_mat n a k l) k = a \<cdot>\<^sub>v unit_vec n l + unit_vec n k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>k \<noteq> i; i < n\<rbrakk> \<Longrightarrow> row (addrow_mat n a k l) i = unit_vec n i) &&& (\<lbrakk>k < n; l < n\<rbrakk> \<Longrightarrow> row (addrow_mat n a k l) k = a \<cdot>\<^sub>v unit_vec n l + unit_vec n k)
[PROOF STEP]
by (rule eq_vecI, auto)


[STATEMENT]
lemma addrow_mat: assumes A: "A \<in> carrier_mat n nc"
  and l: "l < n"
  shows "addrow a k l A = addrow_mat n a k l * A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow a k l A = addrow_mat n a k l * A
[PROOF STEP]
by (rule eq_matI, insert l A, auto simp: row_addrow
  add_scalar_prod_distrib[of _ n] smult_scalar_prod_distrib[of _ n])


[STATEMENT]
lemma row_swaprows:
  "l < n \<Longrightarrow> row (swaprows_mat n l l) l = unit_vec n l"
  "i \<noteq> k \<Longrightarrow> i \<noteq> l \<Longrightarrow> i < n \<Longrightarrow> row (swaprows_mat n k l) i = unit_vec n i"
  "k < n \<Longrightarrow> l < n \<Longrightarrow> row (swaprows_mat n k l) l = unit_vec n k"
  "k < n \<Longrightarrow> l < n \<Longrightarrow> row (swaprows_mat n k l) k = unit_vec n l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((l < n \<Longrightarrow> row (swaprows_mat n l l) l = unit_vec n l) &&& (\<lbrakk>i \<noteq> k; i \<noteq> l; i < n\<rbrakk> \<Longrightarrow> row (swaprows_mat n k l) i = unit_vec n i)) &&& (\<lbrakk>k < n; l < n\<rbrakk> \<Longrightarrow> row (swaprows_mat n k l) l = unit_vec n k) &&& (\<lbrakk>k < n; l < n\<rbrakk> \<Longrightarrow> row (swaprows_mat n k l) k = unit_vec n l)
[PROOF STEP]
by (rule eq_vecI, auto)


[STATEMENT]
lemma swaprows_mat: assumes A: "A \<in> carrier_mat n nc" and k: "k < n" "l < n"
  shows "swaprows k l A = swaprows_mat n k l * A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows k l A = swaprows_mat n k l * A
[PROOF STEP]
by (rule eq_matI, insert A k, auto simp: row_swaprows)


[STATEMENT]
lemma swaprows_mat_inv: assumes k: "k < n" and l: "l < n"
  shows "swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
have "swaprows_mat n k l * swaprows_mat n k l =
    swaprows_mat n k l * (swaprows_mat n k l * 1\<^sub>m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = swaprows_mat n k l * (swaprows_mat n k l * 1\<^sub>m n)
[PROOF STEP]
by (simp add: right_mult_one_mat[of _ n])
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l * swaprows_mat n k l = swaprows_mat n k l * (swaprows_mat n k l * 1\<^sub>m n)

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l * swaprows_mat n k l = swaprows_mat n k l * (swaprows_mat n k l * 1\<^sub>m n)

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
have "swaprows_mat n k l * 1\<^sub>m n = swaprows k l (1\<^sub>m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l * 1\<^sub>m n = swaprows k l (1\<^sub>m n)
[PROOF STEP]
by (rule swaprows_mat[symmetric, OF _ k l, of _ n], simp)
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l * 1\<^sub>m n = swaprows k l (1\<^sub>m n)

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l * 1\<^sub>m n = swaprows k l (1\<^sub>m n)

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
have "swaprows_mat n k l * \<dots> = swaprows k l \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l * swaprows k l (1\<^sub>m n) = swaprows k l (swaprows k l (1\<^sub>m n))
[PROOF STEP]
by (rule swaprows_mat[symmetric, of _ _ n], insert k l, auto)
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l * swaprows k l (1\<^sub>m n) = swaprows k l (swaprows k l (1\<^sub>m n))

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l * swaprows k l (1\<^sub>m n) = swaprows k l (swaprows k l (1\<^sub>m n))

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
have "\<dots> = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows k l (swaprows k l (1\<^sub>m n)) = 1\<^sub>m n
[PROOF STEP]
by (rule eq_matI, insert k l, auto)
[PROOF STATE]
proof (state)
this:
swaprows k l (swaprows k l (1\<^sub>m n)) = 1\<^sub>m n

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n

goal (1 subgoal):
 1. swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l * swaprows_mat n k l = 1\<^sub>m n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma swaprows_mat_Unit: assumes k: "k < n" and l: "l < n"
  shows "swaprows_mat n k l \<in> Units (ring_mat TYPE('a :: semiring_1) n b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. swaprows_mat n k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
interpret m: semiring "ring_mat TYPE('a) n b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semiring (ring_mat TYPE('a) n b)
[PROOF STEP]
by (rule semiring_mat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. swaprows_mat n k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
unfolding Units_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows_mat n k l \<in> {y \<in> carrier (ring_mat TYPE('a) n b). \<exists>x\<in>carrier (ring_mat TYPE('a) n b). x \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> y = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub> \<and> y \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> x = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub>}
[PROOF STEP]
by (rule, rule conjI[OF _ bexI[of _ "swaprows_mat n k l"]],
    auto simp: ring_mat_def swaprows_mat_inv[OF k l] swaprows_mat_inv[OF l k])
[PROOF STATE]
proof (state)
this:
swaprows_mat n k l \<in> Units (ring_mat TYPE('a) n b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addrow_mat_inv: assumes k: "k < n" and l: "l < n" and neq: "k \<noteq> l"
  shows "addrow_mat n a k l * addrow_mat n (- (a :: 'a :: comm_ring_1)) k l = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
have "addrow_mat n a k l * addrow_mat n (- a) k l =
    addrow_mat n a k l * (addrow_mat n (- a) k l * 1\<^sub>m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = addrow_mat n a k l * (addrow_mat n (- a) k l * 1\<^sub>m n)
[PROOF STEP]
by (simp add: right_mult_one_mat[of _ n])
[PROOF STATE]
proof (state)
this:
addrow_mat n a k l * addrow_mat n (- a) k l = addrow_mat n a k l * (addrow_mat n (- a) k l * 1\<^sub>m n)

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
addrow_mat n a k l * addrow_mat n (- a) k l = addrow_mat n a k l * (addrow_mat n (- a) k l * 1\<^sub>m n)

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
have "addrow_mat n (- a) k l * 1\<^sub>m n = addrow (- a) k l (1\<^sub>m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n (- a) k l * 1\<^sub>m n = addrow (- a) k l (1\<^sub>m n)
[PROOF STEP]
by (rule addrow_mat[symmetric, of _ _ n], insert k l, auto)
[PROOF STATE]
proof (state)
this:
addrow_mat n (- a) k l * 1\<^sub>m n = addrow (- a) k l (1\<^sub>m n)

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
addrow_mat n (- a) k l * 1\<^sub>m n = addrow (- a) k l (1\<^sub>m n)

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
have "addrow_mat n a k l * \<dots> = addrow a k l \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l * addrow (- a) k l (1\<^sub>m n) = addrow a k l (addrow (- a) k l (1\<^sub>m n))
[PROOF STEP]
by (rule addrow_mat[symmetric, of _ _ n], insert k l, auto)
[PROOF STATE]
proof (state)
this:
addrow_mat n a k l * addrow (- a) k l (1\<^sub>m n) = addrow a k l (addrow (- a) k l (1\<^sub>m n))

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
addrow_mat n a k l * addrow (- a) k l (1\<^sub>m n) = addrow a k l (addrow (- a) k l (1\<^sub>m n))

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
have "\<dots> = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow a k l (addrow (- a) k l (1\<^sub>m n)) = 1\<^sub>m n
[PROOF STEP]
by (rule eq_matI, insert k l neq, auto, algebra)
[PROOF STATE]
proof (state)
this:
addrow a k l (addrow (- a) k l (1\<^sub>m n)) = 1\<^sub>m n

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n

goal (1 subgoal):
 1. addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
addrow_mat n a k l * addrow_mat n (- a) k l = 1\<^sub>m n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addrow_mat_Unit: assumes k: "k < n" and l: "l < n" and neq: "k \<noteq> l"
  shows "addrow_mat n a k l \<in> Units (ring_mat TYPE('a :: comm_ring_1) n b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. addrow_mat n a k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
interpret m: semiring "ring_mat TYPE('a) n b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semiring (ring_mat TYPE('a) n b)
[PROOF STEP]
by (rule semiring_mat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. addrow_mat n a k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
unfolding Units_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat n a k l \<in> {y \<in> carrier (ring_mat TYPE('a) n b). \<exists>x\<in>carrier (ring_mat TYPE('a) n b). x \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> y = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub> \<and> y \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> x = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub>}
[PROOF STEP]
by (rule, rule conjI[OF _ bexI[of _ "addrow_mat n (- a) k l"]], insert neq,
    auto simp: ring_mat_def addrow_mat_inv[OF k l neq],
    rule trans[OF _ addrow_mat_inv[OF k l neq, of "- a"]], auto)
[PROOF STATE]
proof (state)
this:
addrow_mat n a k l \<in> Units (ring_mat TYPE('a) n b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multrow_mat_inv: assumes k: "k < n" and a: "(a :: 'a :: division_ring) \<noteq> 0"
  shows "multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
have "multrow_mat n k a * multrow_mat n k (inverse a) =
    multrow_mat n k a * (multrow_mat n k (inverse a) * 1\<^sub>m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = multrow_mat n k a * (multrow_mat n k (inverse a) * 1\<^sub>m n)
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = multrow_mat n k a * (multrow_mat n k (inverse a) * 1\<^sub>m n)
[PROOF STEP]
by (simp add: right_mult_one_mat[of _ n])
[PROOF STATE]
proof (state)
this:
multrow_mat n k a * multrow_mat n k (inverse a) = multrow_mat n k a * (multrow_mat n k (inverse a) * 1\<^sub>m n)

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multrow_mat n k a * multrow_mat n k (inverse a) = multrow_mat n k a * (multrow_mat n k (inverse a) * 1\<^sub>m n)

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
have "multrow_mat n k (inverse a) * 1\<^sub>m n = multrow k (inverse a) (1\<^sub>m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k (inverse a) * 1\<^sub>m n = multrow k (inverse a) (1\<^sub>m n)
[PROOF STEP]
by (rule multrow_mat[symmetric, of _ _ n], insert k, auto)
[PROOF STATE]
proof (state)
this:
multrow_mat n k (inverse a) * 1\<^sub>m n = multrow k (inverse a) (1\<^sub>m n)

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multrow_mat n k (inverse a) * 1\<^sub>m n = multrow k (inverse a) (1\<^sub>m n)

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
have "multrow_mat n k a * \<dots> = multrow k a \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a * multrow k (inverse a) (1\<^sub>m n) = multrow k a (multrow k (inverse a) (1\<^sub>m n))
[PROOF STEP]
by (rule multrow_mat[symmetric, of _ _ n], insert k, auto)
[PROOF STATE]
proof (state)
this:
multrow_mat n k a * multrow k (inverse a) (1\<^sub>m n) = multrow k a (multrow k (inverse a) (1\<^sub>m n))

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multrow_mat n k a * multrow k (inverse a) (1\<^sub>m n) = multrow k a (multrow k (inverse a) (1\<^sub>m n))

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
have "\<dots> = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow k a (multrow k (inverse a) (1\<^sub>m n)) = 1\<^sub>m n
[PROOF STEP]
by (rule eq_matI, insert a k a, auto)
[PROOF STATE]
proof (state)
this:
multrow k a (multrow k (inverse a) (1\<^sub>m n)) = 1\<^sub>m n

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n

goal (1 subgoal):
 1. multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
multrow_mat n k a * multrow_mat n k (inverse a) = 1\<^sub>m n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multrow_mat_Unit: assumes k: "k < n" and a: "(a :: 'a :: division_ring) \<noteq> 0"
  shows "multrow_mat n k a \<in> Units (ring_mat TYPE('a) n b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multrow_mat n k a \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> (0::'a)
[PROOF STEP]
have ia: "inverse a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'a)

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

goal (1 subgoal):
 1. multrow_mat n k a \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
interpret m: semiring "ring_mat TYPE('a) n b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semiring (ring_mat TYPE('a) n b)
[PROOF STEP]
by (rule semiring_mat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multrow_mat n k a \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
unfolding Units_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow_mat n k a \<in> {y \<in> carrier (ring_mat TYPE('a) n b). \<exists>x\<in>carrier (ring_mat TYPE('a) n b). x \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> y = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub> \<and> y \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> x = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub>}
[PROOF STEP]
by (rule, rule conjI[OF _ bexI[of _ "multrow_mat n k (inverse a)"]], insert a,
    auto simp: ring_mat_def multrow_mat_inv[OF k],
    rule trans[OF _ multrow_mat_inv[OF k ia]], insert a, auto)
[PROOF STATE]
proof (state)
this:
multrow_mat n k a \<in> Units (ring_mat TYPE('a) n b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_eliminate_entries_gen[simp]: "dim_row (eliminate_entries_gen v B i as) = dim_row B"
  "dim_col (eliminate_entries_gen v B i as) = dim_col B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (local.eliminate_entries_gen v B i as) = dim_row B &&& dim_col (local.eliminate_entries_gen v B i as) = dim_col B
[PROOF STEP]
unfolding eliminate_entries_gen_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> i then minus (B $$ (ia, j)) (times (v ia) (B $$ (i, j))) else B $$ (ia, j))) = dim_row B &&& dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> i then minus (B $$ (ia, j)) (times (v ia) (B $$ (i, j))) else B $$ (ia, j))) = dim_col B
[PROOF STEP]
by auto


[STATEMENT]
lemma dimc_eliminate_entries_rec[simp]: "dim_col (eliminate_entries_rec B i as) = dim_col B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (eliminate_entries_rec B i as) = dim_col B
[PROOF STEP]
by (induct as arbitrary: B, auto simp: Let_def)


[STATEMENT]
lemma dimr_eliminate_entries_rec[simp]: "dim_row (eliminate_entries_rec B i as) = dim_row B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (eliminate_entries_rec B i as) = dim_row B
[PROOF STEP]
by (induct as arbitrary: B, auto simp: Let_def)


[STATEMENT]
lemma carrier_eliminate_entries: "A \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_gen v A i bs \<in> carrier_mat nr nc"
  "B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i as \<in> carrier_mat nr nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<in> carrier_mat nr nc \<Longrightarrow> local.eliminate_entries_gen v A i bs \<in> carrier_mat nr nc) &&& (B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i as \<in> carrier_mat nr nc)
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<in> {m. dim_row m = nr \<and> dim_col m = nc} \<Longrightarrow> local.eliminate_entries_gen v A i bs \<in> {m. dim_row m = nr \<and> dim_col m = nc}) &&& (B \<in> {m. dim_row m = nr \<and> dim_col m = nc} \<Longrightarrow> eliminate_entries_rec B i as \<in> {m. dim_row m = nr \<and> dim_col m = nc})
[PROOF STEP]
by auto


[STATEMENT]
lemma eliminate_entries_convert:
  assumes jA: "J < dim_col A" and *: "I < dim_row A" "dim_row B = dim_row A"
  shows "eliminate_entries (\<lambda> i. A $$ (i,J)) B I J =
    eliminate_entries_rec B I (map (\<lambda> i. (- A $$ (i, J), i)) (filter (\<lambda> i. i \<noteq> I) [0 ..< dim_row A]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
let ?ais = "\<lambda> is. map (\<lambda> i. (- A $$ (i, J), i)) (filter (\<lambda> i. i \<noteq> I) is)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
define one_go where "one_go = (\<lambda> B is. mat (dim_row B) (dim_col B) (\<lambda> (i, j).
    if i \<noteq> I \<and> i \<in> set is then B $$ (i,j) - (A $$ (i,J))  * B $$ (I,j) else B $$ (i,j)))"
[PROOF STATE]
proof (state)
this:
one_go = (\<lambda>B is. mat (dim_row B) (dim_col B) (\<lambda>(i, j). if i \<noteq> I \<and> i \<in> set is then B $$ (i, j) - A $$ (i, J) * B $$ (I, j) else B $$ (i, j)))

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
one_go = (\<lambda>B is. mat (dim_row B) (dim_col B) (\<lambda>(i, j). if i \<noteq> I \<and> i \<in> set is then B $$ (i, j) - A $$ (i, J) * B $$ (I, j) else B $$ (i, j)))

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
fix "is" :: "nat list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
assume "distinct is"
[PROOF STATE]
proof (state)
this:
distinct is

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
from * this
[PROOF STATE]
proof (chain)
picking this:
I < dim_row A
dim_row B = dim_row A
distinct is
[PROOF STEP]
have "eliminate_entries_rec B I (?ais is) = one_go B is"
[PROOF STATE]
proof (prove)
using this:
I < dim_row A
dim_row B = dim_row A
distinct is

goal (1 subgoal):
 1. eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is
[PROOF STEP]
proof (induct "is" arbitrary: B)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct []\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [])) = one_go B []
 2. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
I < dim_row A
dim_row B = dim_row A
distinct []

goal (2 subgoals):
 1. \<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct []\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [])) = one_go B []
 2. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [])) = one_go B []
[PROOF STEP]
unfolding one_go_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [])) = mat (dim_row B) (dim_col B) (\<lambda>(i, j). if i \<noteq> I \<and> i \<in> set [] then B $$ (i, j) - A $$ (i, J) * B $$ (I, j) else B $$ (i, j))
[PROOF STEP]
by (rule eq_matI, auto)
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [])) = one_go B []

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
case (Cons i "is")
[PROOF STATE]
proof (state)
this:
\<lbrakk>I < dim_row A; dim_row ?B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec ?B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go ?B is
I < dim_row A
dim_row B = dim_row A
distinct (i # is)

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
note I = Cons(2)
[PROOF STATE]
proof (state)
this:
I < dim_row A

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
note dim = Cons(3)
[PROOF STATE]
proof (state)
this:
dim_row B = dim_row A

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
note II = Cons(2)[folded dim]
[PROOF STATE]
proof (state)
this:
I < dim_row B

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
let ?B = "addrow (- A $$ (i, J)) i I B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
from Cons(4) I dim
[PROOF STATE]
proof (chain)
picking this:
distinct (i # is)
I < dim_row A
dim_row B = dim_row A
[PROOF STEP]
have "I < dim_row A" "dim_row ?B = dim_row A" and dist: "distinct is"
[PROOF STATE]
proof (prove)
using this:
distinct (i # is)
I < dim_row A
dim_row B = dim_row A

goal (1 subgoal):
 1. (I < dim_row A &&& dim_row (addrow (- A $$ (i, J)) i I B) = dim_row A) &&& distinct is
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I < dim_row A
dim_row (addrow (- A $$ (i, J)) i I B) = dim_row A
distinct is

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
note IH = Cons(1)[OF this]
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec (addrow (- A $$ (i, J)) i I B) I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go (addrow (- A $$ (i, J)) i I B) is

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
from Cons(4)
[PROOF STATE]
proof (chain)
picking this:
distinct (i # is)
[PROOF STEP]
have i: "i \<notin> set is"
[PROOF STATE]
proof (prove)
using this:
distinct (i # is)

goal (1 subgoal):
 1. i \<notin> set is
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<notin> set is

goal (1 subgoal):
 1. \<And>a is B. \<lbrakk>\<And>B. \<lbrakk>I < dim_row A; dim_row B = dim_row A; distinct is\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is; I < dim_row A; dim_row B = dim_row A; distinct (a # is)\<rbrakk> \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (a # is))) = one_go B (a # is)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
proof (cases "i = I")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
 2. i \<noteq> I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> I

goal (2 subgoals):
 1. i = I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
 2. i \<noteq> I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
hence id: "?ais (i # is) = (- A $$ (i, J), i) # ?ais is"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> I

goal (1 subgoal):
 1. map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is)) = (- A $$ (i, J), i) # map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is)) = (- A $$ (i, J), i) # map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)

goal (2 subgoals):
 1. i = I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
 2. i \<noteq> I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
unfolding id eliminate_entries_rec.simps IH
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_go (addrow (- A $$ (i, J)) i I B) is = one_go B (i # is)
[PROOF STEP]
unfolding one_go_def index_mat_addrow
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j)) = mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j))
[PROOF STEP]
proof (rule eq_matI, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ia j. \<lbrakk>ia < dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j))); j < dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))\<rbrakk> \<Longrightarrow> mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j)) $$ (ia, j) = mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)) $$ (ia, j)
 2. dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
 3. dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
[PROOF STEP]
case (1 ii jj)
[PROOF STATE]
proof (state)
this:
ii < dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
jj < dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))

goal (3 subgoals):
 1. \<And>ia j. \<lbrakk>ia < dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j))); j < dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))\<rbrakk> \<Longrightarrow> mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j)) $$ (ia, j) = mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)) $$ (ia, j)
 2. dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
 3. dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
[PROOF STEP]
hence ii: "ii < dim_row B" and jj: "jj < dim_col B" and iiA: "ii < dim_row A"
[PROOF STATE]
proof (prove)
using this:
ii < dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
jj < dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))

goal (1 subgoal):
 1. ii < dim_row B &&& jj < dim_col B &&& ii < dim_row A
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
ii < dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
jj < dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
dim_row B = dim_row A

goal (1 subgoal):
 1. ii < dim_row B &&& jj < dim_col B &&& ii < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ii < dim_row B
jj < dim_col B
ii < dim_row A

goal (3 subgoals):
 1. \<And>ia j. \<lbrakk>ia < dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j))); j < dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))\<rbrakk> \<Longrightarrow> mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j)) $$ (ia, j) = mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)) $$ (ia, j)
 2. dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
 3. dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j)) $$ (ii, jj) = mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)) $$ (ii, jj)
[PROOF STEP]
unfolding index_mat[OF ii jj] split
            index_mat_addrow(1)[OF ii jj] index_mat_addrow(1)[OF II jj]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ii \<noteq> I \<and> ii \<in> set is then (if i = ii then - A $$ (i, J) * B $$ (I, jj) + B $$ (ii, jj) else B $$ (ii, jj)) - A $$ (ii, J) * (if i = I then - A $$ (i, J) * B $$ (I, jj) + B $$ (I, jj) else B $$ (I, jj)) else if i = ii then - A $$ (i, J) * B $$ (I, jj) + B $$ (ii, jj) else B $$ (ii, jj)) = (if ii \<noteq> I \<and> ii \<in> set (i # is) then B $$ (ii, jj) - A $$ (ii, J) * B $$ (I, jj) else B $$ (ii, jj))
[PROOF STEP]
using i False
[PROOF STATE]
proof (prove)
using this:
i \<notin> set is
i \<noteq> I

goal (1 subgoal):
 1. (if ii \<noteq> I \<and> ii \<in> set is then (if i = ii then - A $$ (i, J) * B $$ (I, jj) + B $$ (ii, jj) else B $$ (ii, jj)) - A $$ (ii, J) * (if i = I then - A $$ (i, J) * B $$ (I, jj) + B $$ (I, jj) else B $$ (I, jj)) else if i = ii then - A $$ (i, J) * B $$ (I, jj) + B $$ (ii, jj) else B $$ (ii, jj)) = (if ii \<noteq> I \<and> ii \<in> set (i # is) then B $$ (ii, jj) - A $$ (ii, J) * B $$ (I, jj) else B $$ (ii, jj))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j)) $$ (ii, jj) = mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)) $$ (ii, jj)

goal (2 subgoals):
 1. dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_row (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
 2. dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set is then addrow (- A $$ (i, J)) i I B $$ (ia, j) - A $$ (ia, J) * addrow (- A $$ (i, J)) i I B $$ (I, j) else addrow (- A $$ (i, J)) i I B $$ (ia, j))) = dim_col (mat (dim_row B) (dim_col B) (\<lambda>(ia, j). if ia \<noteq> I \<and> ia \<in> set (i # is) then B $$ (ia, j) - A $$ (ia, J) * B $$ (I, j) else B $$ (ia, j)))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)

goal (1 subgoal):
 1. i = I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = I

goal (1 subgoal):
 1. i = I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
hence id: "?ais (i # is) = ?ais is"
[PROOF STATE]
proof (prove)
using this:
i = I

goal (1 subgoal):
 1. map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is)) = map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is)) = map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)

goal (1 subgoal):
 1. i = I \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)
[PROOF STEP]
unfolding id Cons(1)[OF I dim dist]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_go B is = one_go B (i # is)
[PROOF STEP]
unfolding one_go_def True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (dim_row B) (dim_col B) (\<lambda>(i, j). if i \<noteq> I \<and> i \<in> set is then B $$ (i, j) - A $$ (i, J) * B $$ (I, j) else B $$ (i, j)) = mat (dim_row B) (dim_col B) (\<lambda>(i, j). if i \<noteq> I \<and> i \<in> set (I # is) then B $$ (i, j) - A $$ (i, J) * B $$ (I, j) else B $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) (i # is))) = one_go B (i # is)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) is)) = one_go B is

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
distinct ?is2 \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) ?is2)) = one_go B ?is2

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
distinct ?is2 \<Longrightarrow> eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) ?is2)) = one_go B ?is2

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))
[PROOF STEP]
by (subst main, force, unfold one_go_def eliminate_entries_gen_def, rule eq_matI,
    insert *, auto)
[PROOF STATE]
proof (state)
this:
eliminate_entries (\<lambda>i. A $$ (i, J)) B I J = eliminate_entries_rec B I (map (\<lambda>i. (- A $$ (i, J), i)) (filter (\<lambda>i. i \<noteq> I) [0..<dim_row A]))

goal:
No subgoals!
[PROOF STEP]
qed