This instance will be upgraded to Heptapod 0.31.0 (final) on 2022-05-24 at 14:00 UTC+2 (a few minutes of down time)

Commit 86b41bc8 authored by Rene Thiemann's avatar Rene Thiemann
Browse files

restructured matrix-library to use syntactic +,-,... classes, more uniform lemma-names

parent cb65e108ac87
This diff is collapsed.
......@@ -76,9 +76,9 @@ definition berlekamp_mat_i :: "'i list \<Rightarrow> 'i mat" where
definition berlekamp_resulting_mat_i :: "'i list \<Rightarrow> 'i mat" where
"berlekamp_resulting_mat_i u = (let Q = berlekamp_mat_i u;
n = dim\<^sub>r Q;
n = dim_row Q;
QI = mat n n (\<lambda> (i,j). if i = j then arith_ops_record.minus ff_ops (Q $$ (i,j)) (arith_ops_record.one ff_ops) else Q $$ (i,j))
in (gauss_jordan_single_i ff_ops (mat_transpose QI)))"
in (gauss_jordan_single_i ff_ops (transpose_mat QI)))"
definition berlekamp_basis_i :: "'i list \<Rightarrow> 'i list list" where
"berlekamp_basis_i u = (map (poly_of_list_i ff_ops o list_of_vec)
......@@ -223,7 +223,7 @@ proof (intro rel_funI)
(power_polys (power_poly_f_mod f' [:0, 1:] (nat p)) f' 1 (degree f'))) $$
(i, j))"
unfolding mat_of_rows_list_def length_map length_power_polys_i power_polys_works
length_power_polys mat_index_mat[OF i j] split
length_power_polys index_mat[OF i j] split
unfolding poly_def cs_def poly'_def cs'_def using i
by auto
} note main = this
......
......@@ -17,8 +17,8 @@ begin
definition mat_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a mat \<Rightarrow> 'b mat \<Rightarrow> bool" where
"mat_rel R A B \<equiv> dim\<^sub>r A = dim\<^sub>r B \<and> dim\<^sub>c A = dim\<^sub>c B \<and>
(\<forall> i j. i < dim\<^sub>r B \<longrightarrow> j < dim\<^sub>c B \<longrightarrow> R (A $$ (i,j)) (B $$ (i,j)))"
"mat_rel R A B \<equiv> dim_row A = dim_row B \<and> dim_col A = dim_col B \<and>
(\<forall> i j. i < dim_row B \<longrightarrow> j < dim_col B \<longrightarrow> R (A $$ (i,j)) (B $$ (i,j)))"
lemma right_total_mat_rel: "right_total R \<Longrightarrow> right_total (mat_rel R)"
unfolding right_total_def
......@@ -27,7 +27,7 @@ proof
assume "\<forall> y. \<exists> x. R x y"
from choice[OF this] obtain f where f: "\<And> x. R (f x) x" by auto
show "\<exists> A. mat_rel R A B"
by (rule exI[of _ "mat_map f B"], unfold mat_rel_def, auto simp: f)
by (rule exI[of _ "map_mat f B"], unfold mat_rel_def, auto simp: f)
qed
lemma left_unique_mat_rel: "left_unique R \<Longrightarrow> left_unique (mat_rel R)"
......@@ -45,7 +45,7 @@ lemma mat_rel_eq: "((R ===> R ===> op =)) op = op = \<Longrightarrow>
unfolding mat_rel_def rel_fun_def mat_eq_iff by (auto, blast+)
definition vec_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a vec \<Rightarrow> 'b vec \<Rightarrow> bool" where
"vec_rel R A B \<equiv> dim\<^sub>v A = dim\<^sub>v B \<and> (\<forall> i. i < dim\<^sub>v B \<longrightarrow> R (A $ i) (B $ i))"
"vec_rel R A B \<equiv> dim_vec A = dim_vec B \<and> (\<forall> i. i < dim_vec B \<longrightarrow> R (A $ i) (B $ i))"
lemma right_total_vec_rel: "right_total R \<Longrightarrow> right_total (vec_rel R)"
unfolding right_total_def
......@@ -54,7 +54,7 @@ proof
assume "\<forall> y. \<exists> x. R x y"
from choice[OF this] obtain f where f: "\<And> x. R (f x) x" by auto
show "\<exists> A. vec_rel R A B"
by (rule exI[of _ "map\<^sub>v f B"], unfold vec_rel_def, auto simp: f)
by (rule exI[of _ "map_vec f B"], unfold vec_rel_def, auto simp: f)
qed
lemma left_unique_vec_rel: "left_unique R \<Longrightarrow> left_unique (vec_rel R)"
......@@ -74,13 +74,13 @@ lemma vec_rel_eq: "((R ===> R ===> op =)) op = op = \<Longrightarrow>
lemma multrow_transfer[transfer_rule]: "((R ===> R ===> R) ===> op = ===> R
===> mat_rel R ===> mat_rel R) mat_multrow_gen mat_multrow_gen"
unfolding mat_rel_def[abs_def] mat_multrow_gen_def[abs_def]
by (intro rel_funI conjI allI impI mat_eqI, auto simp: rel_fun_def)
by (intro rel_funI conjI allI impI eq_matI, auto simp: rel_fun_def)
(* we need index restrictions, TODO: can this be incorporated into transfer rule? *)
lemma swap_rows_transfer: "mat_rel R A B \<Longrightarrow> i < dim\<^sub>r B \<Longrightarrow> j < dim\<^sub>r B \<Longrightarrow>
lemma swap_rows_transfer: "mat_rel R A B \<Longrightarrow> i < dim_row B \<Longrightarrow> j < dim_row B \<Longrightarrow>
mat_rel R (mat_swaprows i j A) (mat_swaprows i j B)"
unfolding mat_rel_def mat_swaprows_def
by (intro rel_funI conjI allI impI mat_eqI, auto)
by (intro rel_funI conjI allI impI eq_matI, auto)
lemma pivot_positions_gen_transfer: assumes [transfer_rule]: "(R ===> R ===> op =) op = op ="
shows
......@@ -88,21 +88,21 @@ lemma pivot_positions_gen_transfer: assumes [transfer_rule]: "(R ===> R ===> op
proof (intro rel_funI, goal_cases)
case (1 ze ze' A A')
note trans[transfer_rule] = 1
from 1 have dim: "dim\<^sub>r A = dim\<^sub>r A'" "dim\<^sub>c A = dim\<^sub>c A'" unfolding mat_rel_def by auto
obtain i j where id: "i = 0" "j = 0" and ij: "i \<le> dim\<^sub>r A'" "j \<le> dim\<^sub>c A'" by auto
have "pivot_positions_main_gen ze A (dim\<^sub>r A) (dim\<^sub>c A) i j =
pivot_positions_main_gen ze' A' (dim\<^sub>r A') (dim\<^sub>c A') i j"
from 1 have dim: "dim_row A = dim_row A'" "dim_col A = dim_col A'" unfolding mat_rel_def by auto
obtain i j where id: "i = 0" "j = 0" and ij: "i \<le> dim_row A'" "j \<le> dim_col A'" by auto
have "pivot_positions_main_gen ze A (dim_row A) (dim_col A) i j =
pivot_positions_main_gen ze' A' (dim_row A') (dim_col A') i j"
using ij
proof (induct i j rule: pivot_positions_main_gen.induct[of "dim\<^sub>r A'" "dim\<^sub>c A'" A' ze'])
proof (induct i j rule: pivot_positions_main_gen.induct[of "dim_row A'" "dim_col A'" A' ze'])
case (1 i j)
note simps[simp] = pivot_positions_main_gen.simps[of _ _ _ _ i j]
show ?case
proof (cases "i < dim\<^sub>r A' \<and> j < dim\<^sub>c A'")
proof (cases "i < dim_row A' \<and> j < dim_col A'")
case False
with dim show ?thesis by auto
next
case True
hence ij: "i < dim\<^sub>r A'" "j < dim\<^sub>c A'" and j: "Suc j \<le> dim\<^sub>c A'" by auto
hence ij: "i < dim_row A'" "j < dim_col A'" and j: "Suc j \<le> dim_col A'" by auto
note IH = 1(1-2)[OF ij _ _ j]
from ij True trans have [transfer_rule]:"R (A $$ (i,j)) (A' $$ (i,j))"
unfolding mat_rel_def by auto
......@@ -110,12 +110,12 @@ proof (intro rel_funI, goal_cases)
show ?thesis
proof (cases "A' $$ (i,j) = ze'")
case True
from ij have "i \<le> dim\<^sub>r A'" by auto
from ij have "i \<le> dim_row A'" by auto
note IH = IH(1)[OF True this]
thus ?thesis using True ij dim eq by simp
next
case False
from ij have "Suc i \<le> dim\<^sub>r A'" by auto
from ij have "Suc i \<le> dim_row A'" by auto
note IH = IH(2)[OF False this]
thus ?thesis using False ij dim eq by simp
qed
......@@ -140,10 +140,10 @@ lemma find_base_vectors_transfer: assumes [transfer_rule]: "(R ===> R ===> op =)
proof (intro rel_funI, goal_cases)
case (1 um um' ze ze' on on' A A')
note trans[transfer_rule] = 1 pivot_positions_gen_transfer[OF assms]
from 1(4) have dim: "dim\<^sub>r A = dim\<^sub>r A'" "dim\<^sub>c A = dim\<^sub>c A'" unfolding mat_rel_def by auto
from 1(4) have dim: "dim_row A = dim_row A'" "dim_col A = dim_col A'" unfolding mat_rel_def by auto
have id: "pivot_positions_gen ze A = pivot_positions_gen ze' A'" by transfer_prover
obtain xs where xs: "map snd (pivot_positions_gen ze' A') = xs" by auto
obtain ys where ys: "[j\<leftarrow>[0..<dim\<^sub>c A'] . j \<notin> set xs] = ys" by auto
obtain ys where ys: "[j\<leftarrow>[0..<dim_col A'] . j \<notin> set xs] = ys" by auto
show "list_all2 (vec_rel R) (find_base_vectors_gen um ze on A)
(find_base_vectors_gen um' ze' on' A')"
unfolding find_base_vectors_gen_def Let_def id xs list_all2_conv_all_nth length_map ys dim
......@@ -151,11 +151,11 @@ proof (intro rel_funI, goal_cases)
fix i
assume i: "i < length ys"
define y where "y = ys ! i"
from i have y: "y < dim\<^sub>c A'" unfolding y_def ys[symmetric] using nth_mem by fastforce
from i have y: "y < dim_col A'" unfolding y_def ys[symmetric] using nth_mem by fastforce
let ?map = "map_of (map prod.swap (pivot_positions_gen ze' A'))"
{
fix i
assume i: "i < dim\<^sub>c A'"
assume i: "i < dim_col A'"
and neq: "i \<noteq> y"
have "R (case ?map i of None \<Rightarrow> ze | Some j \<Rightarrow> um (A $$ (j, y)))
(case ?map i of None \<Rightarrow> ze' | Some j \<Rightarrow> um' (A' $$ (j, y)))"
......@@ -166,7 +166,7 @@ proof (intro rel_funI, goal_cases)
case (Some j)
from map_of_SomeD[OF this] have "(j,i) \<in> set (pivot_positions_gen ze' A')" by auto
from set_mp[OF set_pivot_positions_main_gen this[unfolded pivot_positions_gen_def]]
have j: "j < dim\<^sub>r A'" by auto
have j: "j < dim_row A'" by auto
with trans(4) y have [transfer_rule]: "R (A $$ (j,y)) (A' $$ (j,y))" unfolding mat_rel_def by auto
show ?thesis unfolding Some by (simp, transfer_prover)
qed
......@@ -182,8 +182,8 @@ qed
lemma eliminate_entries_gen_transfer: assumes *[transfer_rule]: "(R ===> R ===> R) ad ad'"
"(R ===> R ===> R) mul mul'"
and vs: "\<And> j. j < dim\<^sub>r B' \<Longrightarrow> R (vs j) (vs' j)"
and i: "i < dim\<^sub>r B'"
and vs: "\<And> j. j < dim_row B' \<Longrightarrow> R (vs j) (vs' j)"
and i: "i < dim_row B'"
and B: "mat_rel R B B'"
shows "mat_rel R
(eliminate_entries_gen ad mul vs B i j)
......@@ -193,14 +193,14 @@ proof -
show ?thesis unfolding mat_rel_def dim_eliminate_entries_gen
proof (intro conjI impI allI)
fix i' j'
assume ij': "i' < dim\<^sub>r B'" "j' < dim\<^sub>c B'"
with BB have ij: "i'< dim\<^sub>r B" "j' < dim\<^sub>c B" by auto
assume ij': "i' < dim_row B'" "j' < dim_col B'"
with BB have ij: "i'< dim_row B" "j' < dim_col B" by auto
have [transfer_rule]: "R (B $$ (i', j')) (B' $$ (i', j'))" using BB ij' by auto
have [transfer_rule]: "R (B $$ (i, j')) (B' $$ (i, j'))" using BB ij' i by auto
have [transfer_rule]: "R (vs i') (vs' i')" using ij' vs[of i'] by auto
show "R (eliminate_entries_gen ad mul vs B i j $$ (i', j'))
(eliminate_entries_gen ad' mul' vs' B' i j $$ (i', j'))"
unfolding eliminate_entries_gen_def mat_index_mat(1)[OF ij] mat_index_mat(1)[OF ij'] split
unfolding eliminate_entries_gen_def index_mat(1)[OF ij] index_mat(1)[OF ij'] split
by transfer_prover
qed (insert BB, auto)
qed
......@@ -220,15 +220,15 @@ private abbreviation (input) modulo where "modulo \<equiv> arith_ops_record.modu
private abbreviation (input) normalize where "normalize \<equiv> arith_ops_record.normalize ops"
definition eliminate_entries_gen_zero :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> (integer \<Rightarrow> 'a) \<Rightarrow> 'a mat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a mat" where
"eliminate_entries_gen_zero minu time z v A I J = mat (dim\<^sub>r A) (dim\<^sub>c A) (\<lambda> (i, j).
"eliminate_entries_gen_zero minu time z v A I J = mat (dim_row A) (dim_col A) (\<lambda> (i, j).
if v (integer_of_nat i) \<noteq> z \<and> i \<noteq> I then minu (A $$ (i,j)) (time (v (integer_of_nat i)) (A $$ (I,j))) else A $$ (i,j))"
definition eliminate_entries_i where "eliminate_entries_i \<equiv> eliminate_entries_gen_zero minus times zero"
definition multrow_i where "multrow_i \<equiv> mat_multrow_gen times"
lemma dim_eliminate_entries_gen_zero[simp]:
"dim\<^sub>r (eliminate_entries_gen_zero mm tt z v B i as) = dim\<^sub>r B"
"dim\<^sub>c (eliminate_entries_gen_zero mm tt z v B i as) = dim\<^sub>c B"
"dim_row (eliminate_entries_gen_zero mm tt z v B i as) = dim_row B"
"dim_col (eliminate_entries_gen_zero mm tt z v B i as) = dim_col B"
unfolding eliminate_entries_gen_zero_def by auto
partial_function (tailrec) gauss_jordan_main_i :: "nat \<Rightarrow> nat \<Rightarrow> 'i mat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'i mat" where
......@@ -247,7 +247,7 @@ partial_function (tailrec) gauss_jordan_main_i :: "nat \<Rightarrow> nat \<Right
else A)"
definition gauss_jordan_single_i :: "'i mat \<Rightarrow> 'i mat" where
"gauss_jordan_single_i A \<equiv> gauss_jordan_main_i (dim\<^sub>r A) (dim\<^sub>c A) A 0 0"
"gauss_jordan_single_i A \<equiv> gauss_jordan_main_i (dim_row A) (dim_col A) A 0 0"
definition find_base_vectors_i :: "'i mat \<Rightarrow> 'i vec list" where
"find_base_vectors_i A \<equiv> find_base_vectors_gen uminus zero one A"
......@@ -273,21 +273,21 @@ lemma multrow_i[transfer_rule]: "(op = ===> R ===> mat_rel R ===> mat_rel R)
using multrow_transfer[of R] times unfolding multrow_i_def rel_fun_def by blast
lemma eliminate_entries_gen_zero[simp]:
assumes "mat_rel R A A'" "I < dim\<^sub>r A'" shows
assumes "mat_rel R A A'" "I < dim_row A'" shows
"eliminate_entries_gen_zero minus times zero v A I J = eliminate_entries_gen minus times (v o integer_of_nat) A I J"
unfolding eliminate_entries_gen_def eliminate_entries_gen_zero_def
proof(standard,goal_cases)
case (1 i j)
have d1:"DP (A $$ (I, j))" and d2:"DP (A $$ (i, j))" using assms DPR 1
unfolding mat_rel_def mat_dim_col_mat mat_dim_row_mat
unfolding mat_rel_def dim_col_mat dim_row_mat
by (metis Domainp.DomainI)+
have e1:"\<And> x. (0::'a) * x = 0" and e2:"\<And> x. x - (0::'a) = x" by auto
from e1[untransferred,OF d1] e2[untransferred,OF d2] 1 show ?case by auto
qed auto
lemma eliminate_entries_i: assumes
vs: "\<And> j. j < dim\<^sub>r B' \<Longrightarrow> R (vs (integer_of_nat j)) (vs' j)"
and i: "i < dim\<^sub>r B'"
vs: "\<And> j. j < dim_row B' \<Longrightarrow> R (vs (integer_of_nat j)) (vs' j)"
and i: "i < dim_row B'"
and B: "mat_rel R B B'"
shows "mat_rel R (eliminate_entries_i ops vs B i j)
(eliminate_entries vs' B' i j)"
......@@ -295,13 +295,13 @@ lemma eliminate_entries_i: assumes
by (rule eliminate_entries_gen_transfer, insert assms, auto simp: plus times minus)
lemma gauss_jordan_main_i:
"nr = dim\<^sub>r A' \<Longrightarrow> nc = dim\<^sub>c A' \<Longrightarrow> mat_rel R A A' \<Longrightarrow> i \<le> nr \<Longrightarrow> j \<le> nc \<Longrightarrow>
"nr = dim_row A' \<Longrightarrow> nc = dim_col A' \<Longrightarrow> mat_rel R A A' \<Longrightarrow> i \<le> nr \<Longrightarrow> j \<le> nc \<Longrightarrow>
mat_rel R (gauss_jordan_main_i ops nr nc A i j) (fst (gauss_jordan_main A' B' i j))"
proof -
obtain P where P: "P = (A',i,j)" by auto
let ?Rel = "measures [\<lambda> (A' :: 'a mat,i,j). nc - j, \<lambda> (A',i,j). if A' $$ (i,j) = 0 then 1 else 0]"
have wf: "wf ?Rel" by simp
show "nr = dim\<^sub>r A' \<Longrightarrow> nc = dim\<^sub>c A' \<Longrightarrow> mat_rel R A A' \<Longrightarrow> i \<le> nr \<Longrightarrow> j \<le> nc \<Longrightarrow>
show "nr = dim_row A' \<Longrightarrow> nc = dim_col A' \<Longrightarrow> mat_rel R A A' \<Longrightarrow> i \<le> nr \<Longrightarrow> j \<le> nc \<Longrightarrow>
mat_rel R (gauss_jordan_main_i ops nr nc A i j) (fst (gauss_jordan_main A' B' i j))"
using P
proof (induct P arbitrary: A' B' A i j rule: wf_induct[OF wf])
......@@ -322,10 +322,10 @@ proof -
hence id: "(i < nr \<and> j < nc) = True" "\<And> x y z. (if x = x then y else z) = y" by auto
from True prems have ij [transfer_rule]:"R (A $$ (i,j)) (A' $$ (i,j))"
unfolding mat_rel_def by auto
from True prems have i: "i < dim\<^sub>r A'" "j < dim\<^sub>c A'" and i': "i < nr" "j < nc" by auto
from True prems have i: "i < dim_row A'" "j < dim_col A'" and i': "i < nr" "j < nc" by auto
{
fix i
assume "i < dim\<^sub>r A'"
assume "i < dim_row A'"
with i True prems have R[transfer_rule]:"R (A $$ (i,j)) (A' $$ (i,j))"
unfolding mat_rel_def by auto
have "(A $$ (i,j) = zero) = (A' $$ (i,j) = 0)" by transfer_prover
......@@ -341,7 +341,7 @@ proof -
let ?is = "[ i' . i' <- [Suc i ..< nr], A $$ (i',j) \<noteq> zero]"
let ?is' = "[ i' . i' <- [Suc i ..< nr], A' $$ (i',j) \<noteq> 0]"
define xs where "xs = [Suc i..<nr]"
have xs: "set xs \<subseteq> {0 ..< dim\<^sub>r A'}" unfolding xs_def using prems by auto
have xs: "set xs \<subseteq> {0 ..< dim_row A'}" unfolding xs_def using prems by auto
hence id': "?is = ?is'" unfolding xs_def[symmetric]
by (induct xs, insert eq_gen, auto)
show ?thesis
......@@ -357,7 +357,7 @@ proof -
case (Cons i' idx')
from arg_cong[OF this, of set] i
have i': "i' < nr" "A' $$ (i', j) \<noteq> 0" by auto
with ij' prems(1-2) have *: "i' < dim\<^sub>r A'" "i < dim\<^sub>r A'" "j < dim\<^sub>c A'" by auto
with ij' prems(1-2) have *: "i' < dim_row A'" "i < dim_row A'" "j < dim_col A'" by auto
have rel: "((swaprows i i' A', i, j), P) \<in> ?Rel"
by (simp add: P True * i')
have "?thesis = (mat_rel R (gauss_jordan_main_i ops nr nc (swaprows i i' A) i j)
......@@ -372,12 +372,12 @@ proof -
from False eq have neq: "(A $$ (i, j) = zero) = False" "(A' $$ (i, j) = 0) = False" by auto
{
fix B B' i
assume B[transfer_rule]: "mat_rel R B B'" and dim: "dim\<^sub>c B' = nc" and i: "i < dim\<^sub>r B'"
from dim i True have "j < dim\<^sub>c B'" by simp
assume B[transfer_rule]: "mat_rel R B B'" and dim: "dim_col B' = nc" and i: "i < dim_row B'"
from dim i True have "j < dim_col B'" by simp
with B i have "R (B $$ (i,j)) (B' $$ (i,j))"
by (simp add: mat_rel_def)
} note vec_rel = this
from prems have dim: "dim\<^sub>r A = dim\<^sub>r A'" unfolding mat_rel_def by auto
from prems have dim: "dim_row A = dim_row A'" unfolding mat_rel_def by auto
show ?thesis
proof (cases "A' $$ (i, j) = 1")
case True
......@@ -454,43 +454,43 @@ proof(goal_cases)
qed
lemma eliminate_entries_gen_zero [simp]:
assumes "i<(dim\<^sub>r A)" "j<(dim\<^sub>c A)" shows
assumes "i<(dim_row A)" "j<(dim_col A)" shows
"eliminate_entries_gen_zero mminus ttimes z v A I J $$ (i, j) =
(if v (integer_of_nat i) = z \<or> i = I then A $$ (i,j) else mminus (A $$ (i,j)) (ttimes (v (integer_of_nat i)) (A $$ (I,j))))"
using assms unfolding eliminate_entries_gen_zero_def by auto
lemma eliminate_entries_gen [simp]:
assumes "i<(dim\<^sub>r A)" "j<(dim\<^sub>c A)" shows
assumes "i<(dim_row A)" "j<(dim_col A)" shows
"eliminate_entries_gen mminus ttimes v A I J $$ (i, j) =
(if i = I then A $$ (i,j) else mminus (A $$ (i,j)) (ttimes (v i) (A $$ (I,j))))"
using assms unfolding eliminate_entries_gen_def by auto
lemma dim_mat_impl [simp]:
"dim\<^sub>r (mat_impl x) = mat_dim_row_impl x"
"dim\<^sub>c (mat_impl x) = mat_dim_col_impl x"
by (cases "Rep_mat_impl x";auto simp:mat_impl.rep_eq mat_dim_row_def mat_dim_col_def mat_dim_row_impl.rep_eq mat_dim_col_impl.rep_eq)+
"dim_row (mat_impl x) = dim_row_impl x"
"dim_col (mat_impl x) = dim_col_impl x"
by (cases "Rep_mat_impl x";auto simp:mat_impl.rep_eq dim_row_def dim_col_def dim_row_impl.rep_eq dim_col_impl.rep_eq)+
lemma dim_eliminate_entries_i2 [simp]:
"mat_dim_row_impl (eliminate_entries_i2 z mm tt v m i) = mat_dim_row_impl m"
"mat_dim_col_impl (eliminate_entries_i2 z mm tt v m i) = mat_dim_col_impl m"
"dim_row_impl (eliminate_entries_i2 z mm tt v m i) = dim_row_impl m"
"dim_col_impl (eliminate_entries_i2 z mm tt v m i) = dim_col_impl m"
by (transfer, auto)+
lemma tabulate_nth: "i < n \<Longrightarrow> tabulate'' f (integer_of_nat n) !! i = f (integer_of_nat i)"
using of_fun_nth[of i n] by auto
lemma eliminate_entries_i2[code]:"eliminate_entries_gen_zero mm tt z v (mat_impl m) i j
= (if i < mat_dim_row_impl m
= (if i < dim_row_impl m
then mat_impl (eliminate_entries_i2 z mm tt v m (integer_of_nat i))
else (Code.abort (STR ''index out of range in eliminate_entries'')
(\<lambda> _. eliminate_entries_gen_zero mm tt z v (mat_impl m) i j)))"
proof (cases "i < mat_dim_row_impl m")
proof (cases "i < dim_row_impl m")
case True
hence id: "(i < mat_dim_row_impl m) = True" by simp
hence id: "(i < dim_row_impl m) = True" by simp
show ?thesis unfolding id if_True
proof (standard;goal_cases)
case (1 i j)
have dims: "i < dim\<^sub>r (mat_impl m)" "j < dim\<^sub>c (mat_impl m)" using 1 by (auto simp:eliminate_entries_i2.rep_eq)
have dims: "i < dim_row (mat_impl m)" "j < dim_col (mat_impl m)" using 1 by (auto simp:eliminate_entries_i2.rep_eq)
then show ?case unfolding eliminate_entries_gen_zero[OF dims] using True
proof(transfer, goal_cases)
case (1 i m j ia v z mm tt)
......
......@@ -11,27 +11,25 @@ text \<open>The following definition allows non-square-matrices, mat\_one (mat\_
definition eye_matrix::"nat \<Rightarrow> nat \<Rightarrow> real mat"
where "eye_matrix nr nc = mat nr nc (\<lambda>(r, c). if r=c then 1 else 0)"
lemma eye_matrix_dim: "dim\<^sub>r (eye_matrix nr nc) = nr" "dim\<^sub>c (eye_matrix nr nc) = nc" by (simp_all add: eye_matrix_def)
lemma eye_matrix_dim: "dim_row (eye_matrix nr nc) = nr" "dim_col (eye_matrix nr nc) = nc" by (simp_all add: eye_matrix_def)
lemma row_eye_matrix:
assumes "i < nr"
shows "row (eye_matrix nr nc) i = unit\<^sub>v nc i"
by (rule vec_eqI, simp add: assms eye_matrix_def vec_unit_def, simp add: eye_matrix_dim(2))
shows "row (eye_matrix nr nc) i = unit_vec nc i"
by (rule eq_vecI, simp add: assms eye_matrix_def unit_vec_def, simp add: eye_matrix_dim(2))
lemma unit_eq_0[simp]:
assumes i: "i \<ge> n"
shows "unit\<^sub>v n i = \<zero>\<^sub>v n"
apply (rule vec_eqI)
apply (metis (mono_tags, lifting) i leD vec_dim_vec vec_index_vec vec_unit_def vec_zero_def)
by simp
shows "unit_vec n i = 0\<^sub>v n"
by (rule eq_vecI, insert i, auto simp: unit_vec_def)
lemma mult_eye_matrix:
assumes "i < nr"
shows "(eye_matrix nr (dim\<^sub>v v) \<otimes>\<^sub>m\<^sub>v v) $ i = (if i<dim\<^sub>v v then v $ i else 0)" (is "?a $ i = ?b")
shows "(eye_matrix nr (dim_vec v) *\<^sub>v v) $ i = (if i<dim_vec v then v $ i else 0)" (is "?a $ i = ?b")
proof -
have "?a $ i = row (eye_matrix nr (dim\<^sub>v v)) i \<bullet> v" using index_mat_mult_vec assms eye_matrix_dim by auto
also have "... = unit\<^sub>v (dim\<^sub>v v) i \<bullet> v" using row_eye_matrix assms by auto
also have "... = ?b" using scalar_prod_left_unit vec_elemsI unit_eq_0 scalar_prod_left_zero by fastforce
have "?a $ i = row (eye_matrix nr (dim_vec v)) i \<bullet> v" using index_mult_mat_vec assms eye_matrix_dim by auto
also have "... = unit_vec (dim_vec v) i \<bullet> v" using row_eye_matrix assms by auto
also have "... = ?b" using scalar_prod_left_unit carrier_vecI unit_eq_0 scalar_prod_left_zero by fastforce
finally show ?thesis by auto
qed
......@@ -42,24 +40,24 @@ where "all1_vec n = vec n (\<lambda>i. 1)"
definition all1_matrix::"nat \<Rightarrow> nat \<Rightarrow> real mat"
where "all1_matrix nr nc = mat nr nc (\<lambda>(r, c). 1)"
lemma all1_matrix_dim: "dim\<^sub>r (all1_matrix nr nc) = nr" "dim\<^sub>c (all1_matrix nr nc) = nc"
lemma all1_matrix_dim: "dim_row (all1_matrix nr nc) = nr" "dim_col (all1_matrix nr nc) = nc"
by (simp_all add: all1_matrix_def)
lemma row_all1_matrix:
assumes "i < nr"
shows "row (all1_matrix nr nc) i = all1_vec nc"
apply (rule vec_eqI)
apply (rule eq_vecI)
apply (simp add: all1_matrix_def all1_vec_def assms)
by (simp add: all1_matrix_def all1_vec_def)
lemma all1_vec_scalar_prod:
shows "all1_vec (length xs) \<bullet> (vec_of_list xs) = sum_list xs"
proof -
have "all1_vec (length xs) \<bullet> (vec_of_list xs) = (\<Sum>i = 0..<dim\<^sub>v (vec_of_list xs). vec_of_list xs $ i)"
have "all1_vec (length xs) \<bullet> (vec_of_list xs) = (\<Sum>i = 0..<dim_vec (vec_of_list xs). vec_of_list xs $ i)"
unfolding scalar_prod_def by (metis (no_types, lifting) all1_vec_def mult_cancel_right1 sum_ivl_cong
vec.abs_eq vec_dim_vec vec_index_vec vec_of_list.abs_eq)
also have "... = (\<Sum>i = 0..<length xs. xs ! i)" using vec.abs_eq vec_dim_vec vec_of_list.abs_eq
by (metis sum_ivl_cong vec_index_vec)
vec.abs_eq dim_vec index_vec vec_of_list.abs_eq)
also have "... = (\<Sum>i = 0..<length xs. xs ! i)" using vec.abs_eq dim_vec vec_of_list.abs_eq
by (metis sum_ivl_cong index_vec)
also have "... = sum_list xs" by (simp add: sum_list_sum_nth)
finally show ?thesis by auto
qed
......@@ -67,11 +65,11 @@ qed
lemma mult_all1_matrix:
assumes "i < nr"
shows "((all1_matrix nr (dim\<^sub>v v)) \<otimes>\<^sub>m\<^sub>v v) $ i = sum_list (list_of_vec v)" (is "?a $ i = sum_list (list_of_vec v)")
shows "((all1_matrix nr (dim_vec v)) *\<^sub>v v) $ i = sum_list (list_of_vec v)" (is "?a $ i = sum_list (list_of_vec v)")
proof -
have "?a $ i = row (all1_matrix nr (dim\<^sub>v v)) i \<bullet> v" using index_mat_mult_vec assms all1_matrix_dim by auto
have "?a $ i = row (all1_matrix nr (dim_vec v)) i \<bullet> v" using index_mult_mat_vec assms all1_matrix_dim by auto
also have "... = sum_list (list_of_vec v)" unfolding row_all1_matrix[OF assms] using all1_vec_scalar_prod[of "list_of_vec v"]
by (metis vec.abs_eq vec_dim_vec vec_list vec_of_list.abs_eq)
by (metis vec.abs_eq dim_vec vec_list vec_of_list.abs_eq)
finally show ?thesis by auto
qed
......@@ -79,23 +77,23 @@ qed
definition copy_first_matrix::"nat \<Rightarrow> nat \<Rightarrow> real mat"
where "copy_first_matrix nr nc = mat nr nc (\<lambda>(r, c). if c = 0 then 1 else 0)"
lemma copy_first_matrix_dim: "dim\<^sub>r (copy_first_matrix nr nc) = nr" "dim\<^sub>c (copy_first_matrix nr nc) = nc"
lemma copy_first_matrix_dim: "dim_row (copy_first_matrix nr nc) = nr" "dim_col (copy_first_matrix nr nc) = nc"
by (simp_all add: copy_first_matrix_def)
lemma row_copy_first_matrix:
assumes "i < nr"
shows "row (copy_first_matrix nr nc) i = unit\<^sub>v nc 0"
apply (rule vec_eqI)
shows "row (copy_first_matrix nr nc) i = unit_vec nc 0"
apply (rule eq_vecI)
apply (auto simp add: copy_first_matrix_def assms)[1]
by (simp add: copy_first_matrix_def)
lemma mult_copy_first_matrix:
assumes "i < nr" and "dim\<^sub>v v > 0"
shows "(copy_first_matrix nr (dim\<^sub>v v) \<otimes>\<^sub>m\<^sub>v v) $ i = v $ 0" (is "?a $ i = v $ 0")
assumes "i < nr" and "dim_vec v > 0"
shows "(copy_first_matrix nr (dim_vec v) *\<^sub>v v) $ i = v $ 0" (is "?a $ i = v $ 0")
proof -
have "?a $ i = row (copy_first_matrix nr (dim\<^sub>v v)) i \<bullet> v" using index_mat_mult_vec assms copy_first_matrix_dim by auto
also have "... = unit\<^sub>v (dim\<^sub>v v) 0 \<bullet> v" using row_copy_first_matrix assms by auto
also have "... = v $ 0" using assms(2) scalar_prod_left_unit vec_elems by blast
have "?a $ i = row (copy_first_matrix nr (dim_vec v)) i \<bullet> v" using index_mult_mat_vec assms copy_first_matrix_dim by auto
also have "... = unit_vec (dim_vec v) 0 \<bullet> v" using row_copy_first_matrix assms by auto
also have "... = v $ 0" using assms(2) scalar_prod_left_unit carrier_dim_vec by blast
finally show ?thesis by auto
qed
......
This diff is collapsed.
......@@ -75,7 +75,7 @@ proof -
qed
lemma polyfun_det:
assumes "\<And>x. (A x) \<in> carrier\<^sub>m n n"
assumes "\<And>x. (A x) \<in> carrier_mat n n"
assumes "\<And>x i j. i<n \<Longrightarrow> j<n \<Longrightarrow> polyfun N (\<lambda>x. (A x) $$ (i,j))"
shows "polyfun N (\<lambda>x. det (A x))"
proof -
......@@ -98,37 +98,37 @@ assumes "i<m" "j<n"
shows "polyfun {..<a + (m * n + c)} (\<lambda>f. extract_matrix (\<lambda>i. f (i + a)) m n $$ (i,j))"
unfolding index_extract_matrix[OF assms] apply (rule polyfun_single) using two_digit_le[OF assms] by simp
lemma polyfun_mat_mult_vec:
assumes "\<And>x. v x \<in> carrier\<^sub>v n"
lemma polyfun_mult_mat_vec:
assumes "\<And>x. v x \<in> carrier_vec n"
assumes "\<And>j. j<n \<Longrightarrow> polyfun N (\<lambda>x. v x $ j)"
assumes "\<And>x. A x \<in> carrier\<^sub>m m n"
assumes "\<And>x. A x \<in> carrier_mat m n"
assumes "\<And>i j. i<m \<Longrightarrow> j<n \<Longrightarrow> polyfun N (\<lambda>x. A x $$ (i,j))"
assumes "j < m"
shows "polyfun N (\<lambda>x. ((A x) \<otimes>\<^sub>m\<^sub>v (v x)) $ j)"
shows "polyfun N (\<lambda>x. ((A x) *\<^sub>v (v x)) $ j)"
proof -
have "\<And>x. j < dim\<^sub>r (A x)" using `j < m` assms(3) mat_carrierD(1) by force
have "\<And>x. n = dim\<^sub>v (v x)" using assms(1) vec_elemsD by fastforce
have "\<And>x. j < dim_row (A x)" using `j < m` assms(3) carrier_matD(1) by force
have "\<And>x. n = dim_vec (v x)" using assms(1) carrier_vecD by fastforce
{
fix i assume "i \<in> {0..<n}"
then have "i < n" by auto
{
fix x
have "i < dim\<^sub>v (v x)" using assms(1) vec_elemsD `i<n` by fastforce
have "j < dim\<^sub>r (A x)" using `j < m` assms(3) mat_carrierD(1) by force
have "dim\<^sub>c (A x) = dim\<^sub>v (v x)" by (metis assms(1) assms(3) mat_carrierD(2) vec_elemsD)
then have "row (A x) j $ i = A x $$ (j,i)" "i<n" using `j < dim\<^sub>r (A x)` `i<n` by (simp_all add: \<open>i < dim\<^sub>v (v x)\<close>)
have "i < dim_vec (v x)" using assms(1) carrier_vecD `i<n` by fastforce
have "j < dim_row (A x)" using `j < m` assms(3) carrier_matD(1) by force
have "dim_col (A x) = dim_vec (v x)" by (metis assms(1) assms(3) carrier_matD(2) carrier_vecD)
then have "row (A x) j $ i = A x $$ (j,i)" "i<n" using `j < dim_row (A x)` `i<n` by (simp_all add: \<open>i < dim_vec (v x)\<close>)
}
then have "polyfun N (\<lambda>x. row (A x) j $ i * v x $ i)"
using polyfun_mult assms(4)[OF `j < m`] assms(2) by fastforce
}
then show ?thesis unfolding index_mat_mult_vec[OF `\<And>x. j < dim\<^sub>r (A x)`] scalar_prod_def
using polyfun_Sum[of "{0..<n}" N "\<lambda>i x. row (A x) j $ i * v x $ i"] finite_atLeastLessThan[of 0 n] `\<And>x. n = dim\<^sub>v (v x)`
then show ?thesis unfolding index_mult_mat_vec[OF `\<And>x. j < dim_row (A x)`] scalar_prod_def
using polyfun_Sum[of "{0..<n}" N "\<lambda>i x. row (A x) j $ i * v x $ i"] finite_atLeastLessThan[of 0 n] `\<And>x. n = dim_vec (v x)`
by simp
qed
(* The variable a has been inserted here to make the induction work:*)
lemma polyfun_evaluate_net_plus_a:
assumes "map dim\<^sub>v inputs = input_sizes m"
assumes "map dim_vec inputs = input_sizes m"
assumes "valid_net m"
assumes "j < output_size m"
shows "polyfun {..<a + count_weights m} (\<lambda>f. evaluate_net (insert_weights m (\<lambda>i. f (i + a))) inputs $ j)"
......@@ -139,33 +139,33 @@ next
case (Conv x m)
then obtain x1 x2 where "x=(x1,x2)" by fastforce
show ?case unfolding `x=(x1,x2)` insert_weights.simps evaluate_net.simps drop_map unfolding list_of_vec_index
proof (rule polyfun_mat_mult_vec)
proof (rule polyfun_mult_mat_vec)
{
fix f
have 1:"valid_net' (insert_weights m (\<lambda>i. f (i + x1 * x2)))"
using `valid_net (Conv x m)` valid_net.simps by (metis
convnet.distinct(1) convnet.distinct(5) convnet.inject(2) remove_insert_weights)
have 2:"map dim\<^sub>v inputs = input_sizes (insert_weights m (\<lambda>i. f (i + x1 * x2)))"
have 2:"map dim_vec inputs = input_sizes (insert_weights m (\<lambda>i. f (i + x1 * x2)))"
using input_sizes_remove_weights remove_insert_weights
by (simp add: Conv.prems(1))
have "dim\<^sub>v (evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2))) inputs) = output_size m"
have "dim_vec (evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2))) inputs) = output_size m"
using output_size_correct[OF 1 2] using remove_insert_weights by auto
then show "evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2))) inputs \<in> carrier\<^sub>v (output_size m)"
using vec_carrier_def by (metis (full_types) mem_Collect_eq)
then show "evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2))) inputs \<in> carrier_vec (output_size m)"
using carrier_vec_def by (metis (full_types) mem_Collect_eq)
}
have "map dim\<^sub>v inputs = input_sizes m" by (simp add: Conv.prems(1))
have "map dim_vec inputs = input_sizes m" by (simp add: Conv.prems(1))
have "valid_net m" using Conv.prems(2) valid_net.cases by fastforce
show "\<And>j. j < output_size m \<Longrightarrow> polyfun {..<a + count_weights (Conv (x1, x2) m)}
(\<lambda>f. evaluate_net (insert_weights m (\<lambda>i. f (i + x1 * x2 + a))) inputs $ j)"
unfolding vec_of_list_index count_weights.simps
using Conv(1)[OF `map dim\<^sub>v inputs = input_sizes m` `valid_net m`, of _ "x1 * x2 + a"]
using Conv(1)[OF `map dim_vec inputs = input_sizes m` `valid_net m`, of _ "x1 * x2 + a"]
unfolding semigroup_add_class.add.assoc ab_semigroup_add_class.add.commute[of "x1 * x2" a]
by blast
have "output_size m = x2" using Conv.prems(2) \<open>x = (x1, x2)\<close> valid_net.cases by fastforce
show "\<And>f. extract_matrix (\<lambda>i. f (i + a)) x1 x2 \<in> carrier\<^sub>m x1 (output_size m)" unfolding `output_size m = x2` using dim_extract_matrix
using mat_carrierI by (metis (no_types, lifting))
show "\<And>f. extract_matrix (\<lambda>i. f (i + a)) x1 x2 \<in> carrier_mat x1 (output_size m)" unfolding `output_size m = x2` using dim_extract_matrix
using carrier_matI by (metis (no_types, lifting))
show "\<And>i j. i < x1 \<Longrightarrow> j < output_size m \<Longrightarrow> polyfun {..<a + count_weights (Conv (x1, x2) m)} (\<lambda>f. extract_matrix (\<lambda>i. f (i + a)) x1 x2 $$ (i, j))"
unfolding `output_size m = x2` count_weights.simps using polyfun_extract_matrix[of _ x1 _ x2 a "count_weights m"] by blast
......@@ -174,9 +174,9 @@ next
qed
next
case (Pool m1 m2 inputs j a)
have A2:"\<And>f. map dim\<^sub>v (take (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m1"
have A2:"\<And>f. map dim_vec (take (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m1"
by (metis Pool.prems(1) append_eq_conv_conj input_sizes.simps(3) input_sizes_remove_weights remove_insert_weights take_map)
have B2:"\<And>f. map dim\<^sub>v (drop (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m2"
have B2:"\<And>f. map dim_vec (drop (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs) = input_sizes m2"
using Pool.prems(1) append_eq_conv_conj input_sizes.simps(3) input_sizes_remove_weights remove_insert_weights by (metis drop_map)
have A3:"valid_net m1" and B3:"valid_net m2" using `valid_net (Pool m1 m2)` valid_net.simps by blast+
have "output_size (Pool m1 m2) = output_size m2" unfolding output_size.simps
......@@ -187,12 +187,12 @@ next
(take (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs)"
let ?net2 = "\<lambda>f. evaluate_net (insert_weights m2 (\<lambda>i. f (i + count_weights m1 + a)))
(drop (length (input_sizes (insert_weights m1 (\<lambda>i. f (i + a))))) inputs)"
have length1: "\<And>f. output_size m1 = dim\<^sub>v (?net1 f)"
have length1: "\<And>f. output_size m1 = dim_vec (?net1 f)"
by (metis A2 A3 input_sizes_remove_weights output_size_correct remove_insert_weights)
then have jlength1:"\<And>f. j < dim\<^sub>v (?net1 f)" using A4 by metis
have length2: "\<And>f. output_size m2 = dim\<^sub>v (?net2 f)"
then have jlength1:"\<And>f. j < dim_vec (?net1 f)" using A4 by metis
have length2: "\<And>f. output_size m2 = dim_vec (?net2 f)"
by (metis B2 B3 input_sizes_remove_weights output_size_correct remove_insert_weights)
then have jlength2:"\<And>f. j < dim\<^sub>v (?net2 f)" using B4 by metis
then have jlength2:"\<And>f. j < dim_vec (?net2 f)" using B4 by metis
have cong1:"\<And>xf. (\<lambda>f. evaluate_net (insert_weights m1 (\<lambda>i. f (i + a)))
(take (length (input_sizes (insert_weights m1 (\<lambda>i. xf (i + a))))) inputs) $ j)
= (\<lambda>f. ?net1 f $ j)"
......@@ -212,7 +212,7 @@ next
qed
lemma polyfun_evaluate_net:
assumes "map dim\<^sub>v inputs = input_sizes m"
assumes "map dim_vec inputs = input_sizes m"
assumes "valid_net m"
assumes "j < output_size m"
shows "polyfun {..<count_weights m} (\<lambda>f. evaluate_net (insert_weights m f) inputs $ j)"
......@@ -244,8 +244,8 @@ qed
lemma polyfun_matricize:
assumes "\<And>x. dims (T x) = ds"
assumes "\<And>is. is \<lhd> ds \<Longrightarrow> polyfun N (\<lambda>x. Tensor.lookup (T x) is)"
assumes "\<And>x. dim\<^sub>r (matricize I (T x)) = nr"
assumes "\<And>x. dim\<^sub>c (matricize I (T x)) = nc"
assumes "\<And>x. dim_row (matricize I (T x)) = nr"
assumes "\<And>x. dim_col (matricize I (T x)) = nc"
assumes "i < nr"
assumes "j < nc"
shows "polyfun N (\<lambda>x. matricize I (T x) $$ (i,j))"
......@@ -255,10 +255,10 @@ proof -
(digit_encode (nths ds (-I )) j))"
have 1:"\<And>x. matricize I (T x) $$ (i,j) = Tensor.lookup (T x) (?weave x)" unfolding matricize_def
by (metis (no_types, lifting) assms(1) assms(3) assms(4) assms(5) assms(6) case_prod_conv
mat_dim_col_mat(1) mat_dim_row_mat(1) mat_index_mat(1) matricize_def)
dim_col_mat(1) dim_row_mat(1) index_mat(1) matricize_def)
have "\<And>x. ?weave x \<lhd> ds"