[STATEMENT]
lemma step_3_a_inv: "A \<in> carrier_mat n n
  \<Longrightarrow> i < j \<Longrightarrow> j < n
  \<Longrightarrow> inv_upto jb A j
  \<Longrightarrow> inv_from uppert A j
  \<Longrightarrow> inv_from_bot (\<lambda> A i. one_zero A i j) A i
  \<Longrightarrow> ev_block n A
  \<Longrightarrow> inv_from uppert (step_3_a i j A) j
    \<and> inv_upto jb (step_3_a i j A) j
    \<and> inv_at one_zero (step_3_a i j A) j \<and> same_diag A (step_3_a i j A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A i; local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j A) j \<and> inv_upto local.jb (step_3_a i j A) j \<and> inv_at one_zero (step_3_a i j A) j \<and> local.same_diag A (step_3_a i j A)
[PROOF STEP]
proof (induct i j A rule: step_3_a.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j A. \<lbrakk>A \<in> carrier_mat n n; 0 < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A 0; local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)
 2. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case (1 j A)
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat n n
0 < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A 0
local.ev_block n A

goal (2 subgoals):
 1. \<And>j A. \<lbrakk>A \<in> carrier_mat n n; 0 < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A 0; local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)
 2. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
0 < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A 0
local.ev_block n A

goal (1 subgoal):
 1. inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)
[PROOF STEP]
by (simp add: inv_from_bot_def inv_at_def)
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case (2 i j A)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = A $$ (i, j); ?xa = (if A $$ (i, i + 1) = (1::'a) \<and> ?x \<noteq> (0::'a) then add_col_sub_row (- ?x) (Suc i) j A else A); ?xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb ?xa j; inv_from local.uppert ?xa j; inv_from_bot (\<lambda>A i. one_zero A i j) ?xa i; local.ev_block n ?xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j ?xa) j \<and> inv_upto local.jb (step_3_a i j ?xa) j \<and> inv_at one_zero (step_3_a i j ?xa) j \<and> local.same_diag ?xa (step_3_a i j ?xa)
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from 2(2-)
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A
[PROOF STEP]
have A: "A \<in> carrier_mat n n" and ij: "Suc i < j" "i < j" and j: "j < n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A

goal (1 subgoal):
 1. A \<in> carrier_mat n n &&& (Suc i < j &&& i < j) &&& j < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat n n
Suc i < j
i < j
j < n

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
let ?cond = "A $$ (i, i + 1) = 1 \<and> A $$ (i, j) \<noteq> 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
let ?B = "add_col_sub_row (- A $$ (i, j)) (Suc i) j A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
obtain B where B: "B = (if ?cond then ?B else A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. B = (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have Bn: "B \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. B \<in> carrier_mat n n
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) \<in> carrier_mat n n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat n n

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note IH = 2(1)[OF refl B Bn ij(2) j]
[PROOF STATE]
proof (state)
this:
\<lbrakk>inv_upto local.jb B j; inv_from local.uppert B j; inv_from_bot (\<lambda>A i. one_zero A i j) B i; local.ev_block n B\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have id: "step_3_a (Suc i) j A = step_3_a i j B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_3_a (Suc i) j A = step_3_a i j B
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_3_a (Suc i) j A = step_3_a i j (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A)
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
step_3_a (Suc i) j A = step_3_a i j B

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from ij j
[PROOF STATE]
proof (chain)
picking this:
Suc i < j
i < j
j < n
[PROOF STEP]
have *: "Suc i < n" "j < n" "Suc i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
Suc i < j
i < j
j < n

goal (1 subgoal):
 1. Suc i < n &&& j < n &&& Suc i \<noteq> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i < n
j < n
Suc i \<noteq> j

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from 2(2-)
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A
[PROOF STEP]
have inv: "inv_upto jb A j" "inv_from uppert A j" "ev_block n A"
    "inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A

goal (1 subgoal):
 1. (inv_upto local.jb A j &&& inv_from local.uppert A j) &&& local.ev_block n A &&& inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_upto local.jb A j
inv_from local.uppert A j
local.ev_block n A
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note evbA = ev_blockD[OF inv(3)]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?j < n\<rbrakk> \<Longrightarrow> A $$ (?i, ?i) = A $$ (?j, ?j)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
proof (cases ?cond)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a))

goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
hence B: "B = A"
[PROOF STATE]
proof (prove)
using this:
\<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a))

goal (1 subgoal):
 1. B = A
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
\<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a))

goal (1 subgoal):
 1. (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = A

goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have inv2: "inv_from_bot (\<lambda>A i. one_zero A i j) A i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from_bot (\<lambda>A i. one_zero A i j) A i
[PROOF STEP]
by (rule inv_from_bot_step[OF _ inv(4)],
      insert False ij evbA[of i j] *, auto simp: one_zero_def)
[PROOF STATE]
proof (state)
this:
inv_from_bot (\<lambda>A i. one_zero A i j) A i

goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
unfolding id B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from local.uppert (step_3_a i j A) j \<and> inv_upto local.jb (step_3_a i j A) j \<and> inv_at one_zero (step_3_a i j A) j \<and> local.same_diag A (step_3_a i j A)
[PROOF STEP]
by (rule IH[unfolded B], insert inv inv2, auto)
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
hence B: "B = ?B"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. B = add_col_sub_row (- A $$ (i, j)) (Suc i) j A
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) = add_col_sub_row (- A $$ (i, j)) (Suc i) j A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = add_col_sub_row (- A $$ (i, j)) (Suc i) j A

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
let ?C = "step_3_a i j B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from inv_uptoD[OF inv(1) j *(1) ij(1), unfolded jb_def] ij
[PROOF STATE]
proof (chain)
picking this:
(Suc j = Suc i \<longrightarrow> A $$ (j, Suc i) \<in> {0::'a, 1::'a}) \<and> (j \<noteq> Suc i \<longrightarrow> Suc j \<noteq> Suc i \<or> A $$ (j, j) \<noteq> A $$ (Suc i, Suc i) \<longrightarrow> A $$ (j, Suc i) = (0::'a))
Suc i < j
i < j
[PROOF STEP]
have Aji: "A $$ (j, Suc i) = 0"
[PROOF STATE]
proof (prove)
using this:
(Suc j = Suc i \<longrightarrow> A $$ (j, Suc i) \<in> {0::'a, 1::'a}) \<and> (j \<noteq> Suc i \<longrightarrow> Suc j \<noteq> Suc i \<or> A $$ (j, j) \<noteq> A $$ (Suc i, Suc i) \<longrightarrow> A $$ (j, Suc i) = (0::'a))
Suc i < j
i < j

goal (1 subgoal):
 1. A $$ (j, Suc i) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (j, Suc i) = (0::'a)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have diag: "same_diag A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.same_diag A B
[PROOF STEP]
unfolding same_diag_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. A $$ (i, i) = B $$ (i, i)
[PROOF STEP]
by (intro allI impI, insert ij j A Aji B, auto)
[PROOF STATE]
proof (state)
this:
local.same_diag A B

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have upto: "same_upto j A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. same_upto j A B
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. same_upto j A (add_col_sub_row (- A $$ (i, j)) (Suc i) j A)
[PROOF STEP]
by (rule add_col_sub_row_same_upto[OF \<open>Suc i < j\<close> \<open>j < n\<close> A inv_upto_mono[OF jb_imp_uppert inv(1)]])
[PROOF STATE]
proof (state)
this:
same_upto j A B

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from add_col_sub_row_inv_from_uppert[OF inv(2) A \<open>Suc i < n\<close> \<open>Suc i < j\<close> \<open>j < n\<close>]
[PROOF STATE]
proof (chain)
picking this:
inv_from local.uppert (add_col_sub_row ?v (Suc i) j A) j
[PROOF STEP]
have from_j: "inv_from uppert B j"
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (add_col_sub_row ?v (Suc i) j A) j

goal (1 subgoal):
 1. inv_from local.uppert B j
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (add_col_sub_row ?v (Suc i) j A) j

goal (1 subgoal):
 1. inv_from local.uppert (add_col_sub_row (- A $$ (i, j)) (Suc i) j A) j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv_from local.uppert B j

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have ev: "A $$ (Suc i, Suc i) = A $$ (j,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (Suc i, Suc i) = A $$ (j, j)
[PROOF STEP]
using evbA[of "Suc i" j] ij j
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc i < n; j < n\<rbrakk> \<Longrightarrow> A $$ (Suc i, Suc i) = A $$ (j, j)
Suc i < j
i < j
j < n

goal (1 subgoal):
 1. A $$ (Suc i, Suc i) = A $$ (j, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (Suc i, Suc i) = A $$ (j, j)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have evb_B: "ev_block n B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.ev_block n B
[PROOF STEP]
by (rule same_diag_ev_block[OF diag inv(3)])
[PROOF STATE]
proof (state)
this:
local.ev_block n B

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note evbB = ev_blockD[OF evb_B]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?j < n\<rbrakk> \<Longrightarrow> B $$ (?i, ?i) = B $$ (?j, ?j)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?j < n\<rbrakk> \<Longrightarrow> B $$ (?i, ?i) = B $$ (?j, ?j)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
assume "k < n"
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
with A *
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
Suc i < n
j < n
Suc i \<noteq> j
k < n
[PROOF STEP]
have k: "k < dim_row A" "k < dim_col A" "j < dim_row A" "j < dim_col A" "j < dim_row A"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
Suc i < n
j < n
Suc i \<noteq> j
k < n

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

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note id = B add_col_sub_index_row[OF k]
[PROOF STATE]
proof (state)
this:
B = add_col_sub_row (- A $$ (i, j)) (Suc i) j A
add_col_sub_row ?a ?k j A $$ (k, j) = (if k = ?k \<and> j = j then A $$ (k, j) + ?a * A $$ (k, k) - ?a * ?a * A $$ (j, k) - ?a * A $$ (j, j) else if k = ?k \<and> j \<noteq> j then A $$ (k, j) - ?a * A $$ (j, j) else if k \<noteq> ?k \<and> j = j then A $$ (k, j) + ?a * A $$ (k, ?k) else A $$ (k, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have "B $$ (k,j) = (if k = i then 0 else A $$ (k,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B $$ (k, j) = (if k = i then 0::'a else A $$ (k, j))
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k = Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, k) - - A $$ (i, j) * - A $$ (i, j) * A $$ (j, k) - - A $$ (i, j) * A $$ (j, j) else if k = Suc i \<and> j \<noteq> j then A $$ (k, j) - - A $$ (i, j) * A $$ (j, j) else if k \<noteq> Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, Suc i) else A $$ (k, j)) = (if k = i then 0::'a else A $$ (k, j))
[PROOF STEP]
using inv_uptoD[OF inv(1), of k "Suc i", unfolded jb_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k < n; Suc i < n; Suc i < j\<rbrakk> \<Longrightarrow> (Suc k = Suc i \<longrightarrow> A $$ (k, Suc i) \<in> {0::'a, 1::'a}) \<and> (k \<noteq> Suc i \<longrightarrow> Suc k \<noteq> Suc i \<or> A $$ (k, k) \<noteq> A $$ (Suc i, Suc i) \<longrightarrow> A $$ (k, Suc i) = (0::'a))

goal (1 subgoal):
 1. (if k = Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, k) - - A $$ (i, j) * - A $$ (i, j) * A $$ (j, k) - - A $$ (i, j) * A $$ (j, j) else if k = Suc i \<and> j \<noteq> j then A $$ (k, j) - - A $$ (i, j) * A $$ (j, j) else if k \<noteq> Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, Suc i) else A $$ (k, j)) = (if k = i then 0::'a else A $$ (k, j))
[PROOF STEP]
by (insert * Aji True ij \<open>k < n\<close>, auto simp: ev)
[PROOF STATE]
proof (state)
this:
B $$ (k, j) = (if k = i then 0::'a else A $$ (k, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?k2 < n \<Longrightarrow> B $$ (?k2, j) = (if ?k2 = i then 0::'a else A $$ (?k2, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note id2 = this
[PROOF STATE]
proof (state)
this:
?k2 < n \<Longrightarrow> B $$ (?k2, j) = (if ?k2 = i then 0::'a else A $$ (?k2, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have "inv_from_bot (\<lambda>A i. one_zero A i j) B i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from_bot (\<lambda>A i. one_zero A i j) B i
[PROOF STEP]
unfolding inv_from_bot_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<ge>i. i < n \<longrightarrow> one_zero B i j
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> i; i < n\<rbrakk> \<Longrightarrow> one_zero B i j
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> i; i < n\<rbrakk> \<Longrightarrow> one_zero B i j
[PROOF STEP]
assume "i \<le> k" "k < n"
[PROOF STATE]
proof (state)
this:
i \<le> k
k < n

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> i; i < n\<rbrakk> \<Longrightarrow> one_zero B i j
[PROOF STEP]
thus "one_zero B k j"
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k < n

goal (1 subgoal):
 1. one_zero B k j
[PROOF STEP]
using inv(4)[unfolded inv_from_bot_def]
        upto[unfolded same_upto_def] evbB[OF \<open>k < n\<close> \<open>j < n\<close>]
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k < n
\<forall>i\<ge>Suc i. i < n \<longrightarrow> one_zero A i j
\<forall>i' j'. i' < n \<longrightarrow> j' < j \<longrightarrow> A $$ (i', j') = B $$ (i', j')
B $$ (k, k) = B $$ (j, j)

goal (1 subgoal):
 1. one_zero B k j
[PROOF STEP]
unfolding one_zero_def id2[OF \<open>k < n\<close>]
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k < n
\<forall>i\<ge>Suc i. i < n \<longrightarrow> (Suc i < j \<longrightarrow> A $$ (i, Suc i) = (1::'a) \<longrightarrow> A $$ (i, j) = (0::'a)) \<and> (j < i \<longrightarrow> A $$ (i, j) = (0::'a)) \<and> (i < j \<longrightarrow> A $$ (i, i) \<noteq> A $$ (j, j) \<longrightarrow> A $$ (i, j) = (0::'a))
\<forall>i' j'. i' < n \<longrightarrow> j' < j \<longrightarrow> A $$ (i', j') = B $$ (i', j')
B $$ (k, k) = B $$ (j, j)

goal (1 subgoal):
 1. (Suc k < j \<longrightarrow> B $$ (k, Suc k) = (1::'a) \<longrightarrow> (if k = i then 0::'a else A $$ (k, j)) = (0::'a)) \<and> (j < k \<longrightarrow> (if k = i then 0::'a else A $$ (k, j)) = (0::'a)) \<and> (k < j \<longrightarrow> B $$ (k, k) \<noteq> B $$ (j, j) \<longrightarrow> (if k = i then 0::'a else A $$ (k, j)) = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_zero B k j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_from_bot (\<lambda>A i. one_zero A i j) B i

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from IH[OF same_upto_inv_upto_jb[OF upto inv(1)] from_j this evb_B]
      same_diag_trans[OF diag]
[PROOF STATE]
proof (chain)
picking this:
inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)
local.same_diag B ?C \<Longrightarrow> local.same_diag A ?C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)
local.same_diag B ?C \<Longrightarrow> local.same_diag A ?C

goal (1 subgoal):
 1. inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)
local.same_diag B ?C \<Longrightarrow> local.same_diag A ?C

goal (1 subgoal):
 1. inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag A (step_3_a i j B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zippers_rose_tree_same_hash':
  assumes "z \<in> set (zippers_rose_tree e h (p, t))"
  shows "hash_tree h (tree_of_zipper\<^sub>m z) =
    hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
z \<in> set (zippers_rose_tree e h (p, t))

goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
proof(induction "(p, t)" arbitrary: p t rule: zippers_rose_tree.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p t. \<lbrakk>\<And>pa ta. \<lbrakk>(pa, ta) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (pa, ta))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e pa, embed_source_tree e ta)); z \<in> set (zippers_rose_tree e h (p, t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
case (1 p t)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?p, ?t) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (?p, ?t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e ?p, embed_source_tree e ?t))
z \<in> set (zippers_rose_tree e h (p, t))

goal (1 subgoal):
 1. \<And>p t. \<lbrakk>\<And>pa ta. \<lbrakk>(pa, ta) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (pa, ta))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e pa, embed_source_tree e ta)); z \<in> set (zippers_rose_tree e h (p, t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
from "1.prems"[unfolded zippers_rose_tree.simps]
[PROOF STATE]
proof (chain)
picking this:
z \<in> set ((blind_path e h p, embed_source_tree e t) # concat (map (zippers_rose_tree e h) (zipper_children (p, t))))
[PROOF STEP]
consider (find) "z = (blind_path e h p, embed_source_tree e t)"
    | (rec) x ts l t' r where "t = Tree (x, ts)" "(l, t', r) \<in> set (splits ts)" "z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))"
[PROOF STATE]
proof (prove)
using this:
z \<in> set ((blind_path e h p, embed_source_tree e t) # concat (map (zippers_rose_tree e h) (zipper_children (p, t))))

goal (1 subgoal):
 1. \<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases t)(auto simp add: zipper_children.simps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> ?thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>p t. \<lbrakk>\<And>pa ta. \<lbrakk>(pa, ta) \<in> set (zipper_children (p, t)); z \<in> set (zippers_rose_tree e h (pa, ta))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e pa, embed_source_tree e ta)); z \<in> set (zippers_rose_tree e h (p, t))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> ?thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> ?thesis; \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
 2. \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
case rec
[PROOF STATE]
proof (state)
this:
t = Tree (x, ts)
(l, t', r) \<in> set (splits ts)
z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))

goal (2 subgoals):
 1. z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
 2. \<And>x ts l t' r. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = Tree (x, ts)
(l, t', r) \<in> set (splits ts)
z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = Tree (x, ts)
(l, t', r) \<in> set (splits ts)
z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))

goal (1 subgoal):
 1. hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
apply(subst "1.hyps"[of "(x, l, r) # p" "t'"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> ((x, l, r) # p, t') \<in> set (zipper_children (p, t))
 2. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))
 3. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m (embed_path e ((x, l, r) # p), embed_source_tree e t')) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
apply(simp_all add: rev_image_eqI zipper_children.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = Tree (x, ts); (l, t', r) \<in> set (splits ts); z \<in> set (zippers_rose_tree e h ((x, l, r) # p, t'))\<rbrakk> \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m (embed_path e ((x, l, r) # p), embed_source_tree e t')) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, Tree\<^sub>m (Unblinded (e x, map (embed_source_tree e) ts))))
[PROOF STEP]
by (metis (no_types) childz_same_tree comp_apply embed_source_tree.simps rec(2))
[PROOF STATE]
proof (state)
this:
hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))

goal (1 subgoal):
 1. z = (blind_path e h p, embed_source_tree e t) \<Longrightarrow> hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))
[PROOF STEP]
qed(simp add: blind_embed_path_same_hash)
[PROOF STATE]
proof (state)
this:
hash_tree h (tree_of_zipper\<^sub>m z) = hash_tree h (tree_of_zipper\<^sub>m (embed_path e p, embed_source_tree e t))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma GF_advice_sync_less:
  assumes "\<And>i. i < n \<Longrightarrow> \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n af \<phi> (w [i \<rightarrow> j + i])[X]\<^sub>\<nu>"
  assumes "\<exists>j. suffix (n + j) w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> j + n])[X]\<^sub>\<nu>"
  shows "\<exists>k \<ge> n. (\<forall>j < n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
let ?index = "\<lambda>i. min i n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
let ?formula = "\<lambda>i. if (i < n) then \<phi> else \<psi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
assume "i < Suc n"
[PROOF STATE]
proof (state)
this:
i < Suc n

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < Suc n
[PROOF STEP]
have min_def: "min i n = i"
[PROOF STATE]
proof (prove)
using this:
i < Suc n

goal (1 subgoal):
 1. min i n = i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
min i n = i

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "\<exists>j. suffix ((?index i) + j) w \<Turnstile>\<^sub>n af (?formula i) (w [?index i \<rightarrow> (?index i) + j])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. suffix (min i n + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> min i n + j])[X]\<^sub>\<nu>
[PROOF STEP]
unfolding min_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [i \<rightarrow> i + j])[X]\<^sub>\<nu>
[PROOF STEP]
by (cases "i < n")
         (metis (full_types) assms(1) add.commute, metis (full_types) assms(2) \<open>i < Suc n\<close> add.commute  less_SucE)
[PROOF STATE]
proof (state)
this:
\<exists>j. suffix (min i n + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> min i n + j])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>
[PROOF STEP]
obtain k where leq: "(\<And>i. i < Suc n \<Longrightarrow> min i n \<le> k)"
    and suffix: "\<And>i. i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
using this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>\<And>i. i < Suc n \<Longrightarrow> min i n \<le> k; \<And>i. i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GF_advice_sync[of "Suc n" ?index w ?formula X]
[PROOF STATE]
proof (prove)
using this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>
(\<And>i. i < Suc n \<Longrightarrow> \<exists>j. suffix (min i n + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> min i n + j])[X]\<^sub>\<nu>) \<Longrightarrow> \<exists>k. \<forall>i<Suc n. min i n \<le> k \<and> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>\<And>i. i < Suc n \<Longrightarrow> min i n \<le> k; \<And>i. i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?i < Suc n \<Longrightarrow> min ?i n \<le> k
?i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if ?i < n then \<phi> else \<psi>) (w [min ?i n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "\<forall>j < n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
using suffix
[PROOF STATE]
proof (prove)
using this:
?i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if ?i < n then \<phi> else \<psi>) (w [min ?i n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
by (metis (full_types) less_SucI min.strict_order_iff)
[PROOF STATE]
proof (state)
this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
using suffix[of n, simplified]
[PROOF STATE]
proof (prove)
using this:
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "k \<ge> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
using leq
[PROOF STATE]
proof (prove)
using this:
?i < Suc n \<Longrightarrow> min ?i n \<le> k

goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
n \<le> k

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
n \<le> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
n \<le> k

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in category) cat_is_inverse_is_inverse_the_inverse:
  assumes "is_inverse \<CC> g f"
  shows "is_inverse \<CC> (f\<inverse>\<^sub>C\<^bsub>\<CC>\<^esub>) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inverse \<CC> (f\<inverse>\<^sub>C\<^bsub>\<CC>\<^esub>) f
[PROOF STEP]
unfolding the_inverse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_inverse \<CC> (THE g. is_inverse \<CC> g f) f
[PROOF STEP]
proof(rule theI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_inverse \<CC> ?a f
 2. \<And>x. is_inverse \<CC> x f \<Longrightarrow> x = ?a
[PROOF STEP]
fix g'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_inverse \<CC> ?a f
 2. \<And>x. is_inverse \<CC> x f \<Longrightarrow> x = ?a
[PROOF STEP]
assume "is_inverse \<CC> g' f"
[PROOF STATE]
proof (state)
this:
is_inverse \<CC> g' f

goal (2 subgoals):
 1. is_inverse \<CC> ?a f
 2. \<And>x. is_inverse \<CC> x f \<Longrightarrow> x = ?a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_inverse \<CC> g' f
[PROOF STEP]
show "g' = g"
[PROOF STATE]
proof (prove)
using this:
is_inverse \<CC> g' f

goal (1 subgoal):
 1. g' = g
[PROOF STEP]
by (meson cat_is_inverse_eq assms)
[PROOF STATE]
proof (state)
this:
g' = g

goal (1 subgoal):
 1. is_inverse \<CC> g f
[PROOF STEP]
qed (rule assms)


[STATEMENT]
lemma return_returns_heap [iff]: "(h \<turnstile> return x \<rightarrow>\<^sub>h h') = (h = h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> return x \<rightarrow>\<^sub>h h' = (h = h')
[PROOF STEP]
unfolding returns_heap_def return_def execute_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case the_prog (Prog (\<lambda>h. Inr (x, h))) h of Inl x \<Rightarrow> False | Inr (xa, xb) \<Rightarrow> h' = xb) = (h = h')
[PROOF STEP]
by auto


[STATEMENT]
lemma pure_eq_iff:
  "(\<forall>h' x. h \<turnstile> f \<rightarrow>\<^sub>r x \<longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h' \<longrightarrow> h = h') \<longleftrightarrow> pure f h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h' x. h \<turnstile> f \<rightarrow>\<^sub>r x \<longrightarrow> h \<turnstile> f \<rightarrow>\<^sub>h h' \<longrightarrow> h = h') = pure f h
[PROOF STEP]
by(auto simp add: pure_def)


[STATEMENT]
lemma fold_M_pure_I : "(\<And>d x. pure (f d x) h) \<Longrightarrow> (\<And>d. pure (fold_M f d xs) h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d x. pure (f d x) h) \<Longrightarrow> (\<And>d. pure (fold_M f d xs) h)
[PROOF STEP]
apply(induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>d. (\<And>d x. pure (f d x) h) \<Longrightarrow> pure (fold_M f d []) h
 2. \<And>a xs d. \<lbrakk>\<And>d. (\<And>d x. pure (f d x) h) \<Longrightarrow> pure (fold_M f d xs) h; \<And>d x. pure (f d x) h\<rbrakk> \<Longrightarrow> pure (fold_M f d (a # xs)) h
[PROOF STEP]
by(auto intro: bind_pure_I)


[STATEMENT]
lemma bind_cong [fundef_cong]:
  fixes f1 f2 :: "('heap, 'e, 'result) prog"
    and g1 g2 :: "'result \<Rightarrow> ('heap, 'e, 'result2) prog"
  assumes "h \<turnstile> f1 = h \<turnstile> f2"
    and "\<And>y h'. h \<turnstile> f1 \<rightarrow>\<^sub>r y \<Longrightarrow> h \<turnstile> f1 \<rightarrow>\<^sub>h h' \<Longrightarrow> h' \<turnstile> g1 y = h' \<turnstile> g2 y"
  shows "h \<turnstile> (f1 \<bind> g1) = h \<turnstile> (f2 \<bind> g2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> f1 \<bind> g1 = h \<turnstile> f2 \<bind> g2
[PROOF STEP]
apply(insert assms, cases "h \<turnstile> f1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>h \<turnstile> f1 = h \<turnstile> f2; \<And>y h'. \<lbrakk>h \<turnstile> f1 \<rightarrow>\<^sub>r y; h \<turnstile> f1 \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h' \<turnstile> g1 y = h' \<turnstile> g2 y; h \<turnstile> f1 = Inl a\<rbrakk> \<Longrightarrow> h \<turnstile> f1 \<bind> g1 = h \<turnstile> f2 \<bind> g2
 2. \<And>b. \<lbrakk>h \<turnstile> f1 = h \<turnstile> f2; \<And>y h'. \<lbrakk>h \<turnstile> f1 \<rightarrow>\<^sub>r y; h \<turnstile> f1 \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h' \<turnstile> g1 y = h' \<turnstile> g2 y; h \<turnstile> f1 = Inr b\<rbrakk> \<Longrightarrow> h \<turnstile> f1 \<bind> g1 = h \<turnstile> f2 \<bind> g2
[PROOF STEP]
by(auto simp add: bind_def returns_result_def returns_heap_def execute_def
      split: sum.splits)


[STATEMENT]
lemma min_one_proper_design: "proper_design \<V> \<B> \<or> proper_design \<V>' \<B>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_design \<V> \<B> \<or> proper_design \<V>' \<B>'
[PROOF STEP]
using blocks_nempty des1_is_proper des2_is_proper
[PROOF STATE]
proof (prove)
using this:
\<B> \<noteq> {#} \<or> \<B>' \<noteq> {#}
\<B> \<noteq> {#} \<Longrightarrow> proper_design \<V> \<B>
\<B>' \<noteq> {#} \<Longrightarrow> proper_design \<V>' \<B>'

goal (1 subgoal):
 1. proper_design \<V> \<B> \<or> proper_design \<V>' \<B>'
[PROOF STEP]
by (unfold_locales, blast)


[STATEMENT]
lemma fresh_var_eqE[elim_format]: "fresh_var e = x \<Longrightarrow> x \<notin>  fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_var e = x \<Longrightarrow> x \<notin> fv e
[PROOF STEP]
by (metis fresh_var_not_free)


[STATEMENT]
lemma insert_in_traverse_pairs [rewrite]:
  "tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)
[PROOF STEP]
@qed


[STATEMENT]
lemma heap_upds_ok_invariant:
  "invariant step heap_upds_ok_conf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant (\<Rightarrow>) heap_upds_ok_conf
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; heap_upds_ok_conf x\<rbrakk> \<Longrightarrow> heap_upds_ok_conf y
[PROOF STEP]
fix c c'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; heap_upds_ok_conf x\<rbrakk> \<Longrightarrow> heap_upds_ok_conf y
[PROOF STEP]
assume "c \<Rightarrow> c'" and "heap_upds_ok_conf c"
[PROOF STATE]
proof (state)
this:
c \<Rightarrow> c'
heap_upds_ok_conf c

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<Rightarrow> y; heap_upds_ok_conf x\<rbrakk> \<Longrightarrow> heap_upds_ok_conf y
[PROOF STEP]
thus "heap_upds_ok_conf c'"
[PROOF STATE]
proof (prove)
using this:
c \<Rightarrow> c'
heap_upds_ok_conf c

goal (1 subgoal):
 1. heap_upds_ok_conf c'
[PROOF STEP]
by (induction rule: step.induct) auto
[PROOF STATE]
proof (state)
this:
heap_upds_ok_conf c'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in finite_group) finite_generate:
  assumes "A \<subseteq> carrier G"
  shows "finite (generate G A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (generate G A)
[PROOF STEP]
using generate_incl[of A] rev_finite_subset[of "carrier G" "generate G A"] assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> carrier G \<Longrightarrow> generate G A \<subseteq> carrier G
\<lbrakk>finite (carrier G); generate G A \<subseteq> carrier G\<rbrakk> \<Longrightarrow> finite (generate G A)
A \<subseteq> carrier G

goal (1 subgoal):
 1. finite (generate G A)
[PROOF STEP]
by simp


[STATEMENT]
lemma eq_dff_cancel_right[simp]: "x * y =dff x * z \<longleftrightarrow> x = 0 \<or> y =dff z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y =dff x * z) = (x = 0 \<or> y =dff z)
[PROOF STEP]
unfolding eq_dff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (divides_ff (x * y) (x * z) \<and> divides_ff (x * z) (x * y)) = (x = 0 \<or> divides_ff y z \<and> divides_ff z y)
[PROOF STEP]
by auto


[STATEMENT]
lemma wp_method_via_spy_framework_ts_completeness :
  assumes "observable M2"
  and   "minimal M2"
  and   "size M2 \<le> size_r (to_prime M1) + (nat_of_integer additionalStates)"
  and   "FSM.inputs M2 = FSM.inputs M1"
  and   "FSM.outputs M2 = FSM.outputs M1"
  and   "isAlreadyPrime \<Longrightarrow> observable M1 \<and> minimal M1 \<and> reachable_states M1 = states M1"
  and   "size (to_prime M1) < 2^64"
shows "(L M1 = L M2) \<longleftrightarrow> list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)
[PROOF STEP]
using apply_to_prime_and_return_io_lists_completeness[where f=wp_method_via_spy_framework and isAlreadyPrime=isAlreadyPrime, OF _ assms(1,2,3,4,5,6,7)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>M1 m M2. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1\<rbrakk> \<Longrightarrow> (L M1 = L M2) = (L M1 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m) = L M2 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m)) \<and> finite_tree (wp_method_via_spy_framework M1 m); isAlreadyPrime \<Longrightarrow> isAlreadyPrime\<rbrakk> \<Longrightarrow> (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)

goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)
[PROOF STEP]
using wp_method_via_spy_framework_completeness_and_finiteness
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>M1 m M2. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1\<rbrakk> \<Longrightarrow> (L M1 = L M2) = (L M1 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m) = L M2 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m)) \<and> finite_tree (wp_method_via_spy_framework M1 m); isAlreadyPrime \<Longrightarrow> isAlreadyPrime\<rbrakk> \<Longrightarrow> (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> (L ?M1.0 = L ?M2.0) = (L ?M1.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m) = L ?M2.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m))
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> finite_tree (wp_method_via_spy_framework ?M1.0 ?m)

goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (wp_method_via_spy_framework_ts M1 additionalStates isAlreadyPrime)
[PROOF STEP]
unfolding wp_method_via_spy_framework_ts_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>M1 m M2. \<lbrakk>observable M1; observable M2; minimal M1; minimal M2; size_r M1 \<le> m; FSM.size M2 \<le> m; FSM.inputs M2 = FSM.inputs M1; FSM.outputs M2 = FSM.outputs M1\<rbrakk> \<Longrightarrow> (L M1 = L M2) = (L M1 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m) = L M2 \<inter> Prefix_Tree.set (wp_method_via_spy_framework M1 m)) \<and> finite_tree (wp_method_via_spy_framework M1 m); isAlreadyPrime \<Longrightarrow> isAlreadyPrime\<rbrakk> \<Longrightarrow> (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> (L ?M1.0 = L ?M2.0) = (L ?M1.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m) = L ?M2.0 \<inter> Prefix_Tree.set (wp_method_via_spy_framework ?M1.0 ?m))
\<lbrakk>observable ?M1.0; observable ?M2.0; minimal ?M1.0; minimal ?M2.0; size_r ?M1.0 \<le> ?m; FSM.size ?M2.0 \<le> ?m; FSM.inputs ?M2.0 = FSM.inputs ?M1.0; FSM.outputs ?M2.0 = FSM.outputs ?M1.0\<rbrakk> \<Longrightarrow> finite_tree (wp_method_via_spy_framework ?M1.0 ?m)

goal (1 subgoal):
 1. (L M1 = L M2) = list_all (passes_test_case M2 (FSM.initial M2)) (apply_to_prime_and_return_io_lists M1 additionalStates isAlreadyPrime wp_method_via_spy_framework)
[PROOF STEP]
by metis


[STATEMENT]
theorem equiv_rels:
  assumes "equiv {..<n} r"
  shows "count_list (equiv_rels n) r = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
obtain y where y_def: "rgf y" "length y = n" "kernel_of y = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>rgf y; length y = n; kernel_of y = r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rgf_exists assms
[PROOF STATE]
proof (prove)
using this:
equiv {..<?n} ?r \<Longrightarrow> \<exists>x. rgf x \<and> length x = ?n \<and> kernel_of x = ?r
equiv {..<n} r

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>rgf y; length y = n; kernel_of y = r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rgf y
length y = n
kernel_of y = r

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have a: "\<And>x. x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of x) = (y=x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of x) = (y = x)
[PROOF STEP]
using enum_rgfs_returns_rgfs y_def(1,2) enum_rgfs_len inj_onD[OF kernel_of_inj_on_rgfs]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (enum_rgfs ?n) \<Longrightarrow> rgf ?x
rgf y
length y = n
?x \<in> set (enum_rgfs ?n) \<Longrightarrow> length ?x = ?n
\<lbrakk>kernel_of ?x = kernel_of ?y; ?x \<in> {x. rgf x}; ?y \<in> {x. rgf x}\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<And>x. x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of x) = (y = x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of ?x) = (y = ?x)

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "count_list (equiv_rels n) r =
    length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (equiv_rels n) r = length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))
[PROOF STEP]
by (simp add:equiv_rels_def count_list_expand length_filter comp_def)
[PROOF STATE]
proof (state)
this:
count_list (equiv_rels n) r = length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_list (equiv_rels n) r = length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))
[PROOF STEP]
using y_def(3)
[PROOF STATE]
proof (prove)
using this:
kernel_of y = r

goal (1 subgoal):
 1. length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. r = kernel_of x) (enum_rgfs n)) = length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = length (filter (\<lambda>x. y = x) (enum_rgfs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (enum_rgfs n) \<Longrightarrow> (kernel_of y = kernel_of ?x) = (y = ?x)

goal (1 subgoal):
 1. length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))
[PROOF STEP]
by (simp cong:filter_cong)
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter (\<lambda>x. kernel_of y = kernel_of x) (enum_rgfs n)) = length (filter ((=) y) (enum_rgfs n))

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = count_list (enum_rgfs n) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) y) (enum_rgfs n)) = count_list (enum_rgfs n) y
[PROOF STEP]
by (simp add:count_list_expand length_filter)
[PROOF STATE]
proof (state)
this:
length (filter ((=) y) (enum_rgfs n)) = count_list (enum_rgfs n) y

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (filter ((=) y) (enum_rgfs n)) = count_list (enum_rgfs n) y

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
have "... = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (enum_rgfs n) y = 1
[PROOF STEP]
using equiv_rels_enum y_def(1,2)
[PROOF STATE]
proof (prove)
using this:
rgf ?x \<Longrightarrow> count_list (enum_rgfs (length ?x)) ?x = 1
rgf y
length y = n

goal (1 subgoal):
 1. count_list (enum_rgfs n) y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
count_list (enum_rgfs n) y = 1

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count_list (equiv_rels n) r = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count_list (equiv_rels n) r = 1

goal (1 subgoal):
 1. count_list (equiv_rels n) r = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list (equiv_rels n) r = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singleton_times_left_hmset[simp]: "\<omega>^M * N = HMSet (image_mset ((+) M) (hmsetmset N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>^ M * N = HMSet (image_mset ((+) M) (hmsetmset N))
[PROOF STEP]
by (simp add: times_hmultiset_def Times_mset_single_left)


[STATEMENT]
lemma term_ok'_betapply:
  assumes "term_ok' (sig \<Theta>) f" "term_ok' (sig \<Theta>) u"
  shows "term_ok' (sig \<Theta>) (f \<bullet> u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
proof(cases "f")
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x11 x12. f = Ct x11 x12 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 2. \<And>x21 x22. f = Fv x21 x22 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 3. \<And>x3. f = Bv x3 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 4. \<And>x41 x42. f = Abs x41 x42 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 5. \<And>x51 x52. f = x51 $ x52 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
case (Abs T t)
[PROOF STATE]
proof (state)
this:
f = Abs T t

goal (5 subgoals):
 1. \<And>x11 x12. f = Ct x11 x12 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 2. \<And>x21 x22. f = Fv x21 x22 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 3. \<And>x3. f = Bv x3 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 4. \<And>x41 x42. f = Abs x41 x42 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 5. \<And>x51 x52. f = x51 $ x52 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f = Abs T t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f = Abs T t

goal (1 subgoal):
 1. term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
using assms term_ok'_subst_bv1
[PROOF STATE]
proof (prove)
using this:
f = Abs T t
term_ok' (sig \<Theta>) f
term_ok' (sig \<Theta>) u
\<lbrakk>term_ok' (sig ?\<Theta>) ?f; term_ok' (sig ?\<Theta>) ?u\<rbrakk> \<Longrightarrow> term_ok' (sig ?\<Theta>) (subst_bv1 ?f ?lev ?u)

goal (1 subgoal):
 1. term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
by (simp add: subst_bv_def)
[PROOF STATE]
proof (state)
this:
term_ok' (sig \<Theta>) (f \<bullet> u)

goal (4 subgoals):
 1. \<And>x11 x12. f = Ct x11 x12 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 2. \<And>x21 x22. f = Fv x21 x22 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 3. \<And>x3. f = Bv x3 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 4. \<And>x51 x52. f = x51 $ x52 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma typ_of_eta_expand: "typ_of f = Some (\<tau> \<rightarrow> \<tau>') \<Longrightarrow> typ_of (Abs \<tau> (f $ Bv 0)) = Some (\<tau> \<rightarrow> \<tau>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typ_of f = Some (\<tau> \<rightarrow> \<tau>') \<Longrightarrow> typ_of (Abs \<tau> (f $ Bv 0)) = Some (\<tau> \<rightarrow> \<tau>')
[PROOF STEP]
using typ_of1_weaken
[PROOF STATE]
proof (prove)
using this:
typ_of1 ?Ts ?t = Some ?T \<Longrightarrow> typ_of1 (?Ts @ ?Ts') ?t = Some ?T

goal (1 subgoal):
 1. typ_of f = Some (\<tau> \<rightarrow> \<tau>') \<Longrightarrow> typ_of (Abs \<tau> (f $ Bv 0)) = Some (\<tau> \<rightarrow> \<tau>')
[PROOF STEP]
by (fastforce simp add: bind_eq_Some_conv typ_of_def)


[STATEMENT]
lemma subst_typ_rename_tvar_preserves_eq:
  "(y, S) \<notin> tvsT T \<Longrightarrow> (y, S) \<notin> tvsT \<tau> \<Longrightarrow>
    subst_typ [((x, S), Tv y S)] T = subst_typ [((x, S), Tv y S)] \<tau> \<Longrightarrow> T=\<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, S) \<notin> tvsT T; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] T = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> T = \<tau>
[PROOF STEP]
proof (induction T arbitrary: \<tau>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 \<tau>. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set x2; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Ty x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Ty x1 x2 = \<tau>
 2. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
case (Ty n Ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n Ts)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] \<tau>

goal (2 subgoals):
 1. \<And>x1 x2 \<tau>. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set x2; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Ty x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Ty x1 x2 = \<tau>
 2. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n Ts)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] \<tau>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n Ts)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] \<tau>

goal (1 subgoal):
 1. Ty n Ts = \<tau>
[PROOF STEP]
proof (induction \<tau>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT x2a; subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] x2a\<rbrakk> \<Longrightarrow> Ty n Ts = x2a; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT (Ty x1 x2); subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] (Ty x1 x2)\<rbrakk> \<Longrightarrow> Ty n Ts = Ty x1 x2
 2. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n Ts = Tv x1 x2
[PROOF STEP]
case (Ty n Ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT ?x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] ?x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = ?x2a
\<lbrakk>?x2a \<in> set Ts__; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts__)
(y, S) \<notin> tvsT (Ty n Ts)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty n Ts)

goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = x2a; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT (Ty x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = Ty x1 x2
 2. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = Tv x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Ts; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT ?x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] ?x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = ?x2a
\<lbrakk>?x2a \<in> set Ts__; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts__)
(y, S) \<notin> tvsT (Ty n Ts)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty n Ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Ts; \<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT ?x2a; subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] ?x2a\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = ?x2a
\<lbrakk>?x2a \<in> set Ts__; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts__)
(y, S) \<notin> tvsT (Ty n Ts)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Ty n Ts)

goal (1 subgoal):
 1. Ty n__ Ts__ = Ty n Ts
[PROOF STEP]
by simp (smt list.inj_map_strong)
[PROOF STATE]
proof (state)
this:
Ty n__ Ts__ = Ty n Ts

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts__; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts__); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts__) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts__ = Tv x1 x2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n Ts); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n Ts) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n Ts = Tv x1 x2
[PROOF STEP]
case (Tv n S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts)
(y, S) \<notin> tvsT (Tv n S)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv n S)

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>x2a \<tau>. \<lbrakk>x2a \<in> set Ts; (y, S) \<notin> tvsT x2a; (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] x2a = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> x2a = \<tau>; (y, S) \<notin> tvsT (Ty n__ Ts); (y, S) \<notin> tvsT (Tv x1 x2); subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv x1 x2)\<rbrakk> \<Longrightarrow> Ty n__ Ts = Tv x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts)
(y, S) \<notin> tvsT (Tv n S)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv n S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Ts; (y, S) \<notin> tvsT ?x2a; (y, S) \<notin> tvsT ?\<tau>; subst_typ [((x, S), Tv y S)] ?x2a = subst_typ [((x, S), Tv y S)] ?\<tau>\<rbrakk> \<Longrightarrow> ?x2a = ?\<tau>
(y, S) \<notin> tvsT (Ty n__ Ts)
(y, S) \<notin> tvsT (Tv n S)
subst_typ [((x, S), Tv y S)] (Ty n__ Ts) = subst_typ [((x, S), Tv y S)] (Tv n S)

goal (1 subgoal):
 1. Ty n__ Ts = Tv n S
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
Ty n__ Ts = Tv n S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Ty n Ts = \<tau>

goal (1 subgoal):
 1. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
case (Tv n S)
[PROOF STATE]
proof (state)
this:
(y, S) \<notin> tvsT (Tv n S)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Tv n S) = subst_typ [((x, S), Tv y S)] \<tau>

goal (1 subgoal):
 1. \<And>x1 x2 \<tau>. \<lbrakk>(y, S) \<notin> tvsT (Tv x1 x2); (y, S) \<notin> tvsT \<tau>; subst_typ [((x, S), Tv y S)] (Tv x1 x2) = subst_typ [((x, S), Tv y S)] \<tau>\<rbrakk> \<Longrightarrow> Tv x1 x2 = \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(y, S) \<notin> tvsT (Tv n S)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Tv n S) = subst_typ [((x, S), Tv y S)] \<tau>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(y, S) \<notin> tvsT (Tv n S)
(y, S) \<notin> tvsT \<tau>
subst_typ [((x, S), Tv y S)] (Tv n S) = subst_typ [((x, S), Tv y S)] \<tau>

goal (1 subgoal):
 1. Tv n S = \<tau>
[PROOF STEP]
by (induction \<tau>) (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
Tv n S = \<tau>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZmX_carrier:
  shows "ZmX \<in> carrier_mat 2 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZmX \<in> carrier_mat 2 2
[PROOF STEP]
unfolding ZmX_def X_def Z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (1 / sqrt 2) \<cdot>\<^sub>m (Matrix.mat 2 2 (\<lambda>(i, j). if i \<noteq> j then 0 else if i = 0 then 1 else - 1) - Matrix.mat 2 2 (\<lambda>(i, j). if i = j then 0 else 1)) \<in> carrier_mat 2 2
[PROOF STEP]
by (simp add: minus_carrier_mat')