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 0bd0489a authored by Manuel Eberl's avatar Manuel Eberl
Browse files

Adapted to isabelle-dev 558ba6b37f5c

parent 49bcc3dcdc2e
......@@ -50,7 +50,7 @@ fun prod_list_m :: "int poly list \<Rightarrow> int poly" where
| "prod_list_m [] = 1"
context
fixes sl_impl :: "(int poly, int \<times> int poly list, 'state)sublists_foldr_impl"
fixes sl_impl :: "(int poly, int \<times> int poly list, 'state)subseqs_foldr_impl"
and m2 :: "int"
begin
definition inv_M2 :: "int \<Rightarrow> int" where
......@@ -65,7 +65,7 @@ partial_function (tailrec) reconstruction :: "'state \<Rightarrow> int poly \<Ri
"reconstruction state u luu lu d r vs res cands = (case cands of Nil
\<Rightarrow> let d' = Suc d
in if d' + d' > r then (u # res) else
(case next_sublists_foldr sl_impl state of (cands,state') \<Rightarrow>
(case next_subseqs_foldr sl_impl state of (cands,state') \<Rightarrow>
reconstruction state' u luu lu d' r vs res cands)
| (lv',ws) # cands' \<Rightarrow> let
lv = inv_M2 lv' (* lv is last coefficient of vb below *)
......@@ -81,7 +81,7 @@ partial_function (tailrec) reconstruction :: "'state \<Rightarrow> int poly \<Ri
else let
lu' = lead_coeff u';
vs' = fold remove1 ws vs;
(cands'', state') = sublists_foldr sl_impl (lu',[]) vs' d
(cands'', state') = subseqs_foldr sl_impl (lu',[]) vs' d
in reconstruction state' u' (smult lu' u') lu' d r' vs' res' cands''
else reconstruction state u luu lu d r vs res cands'
else reconstruction state u luu lu d r vs res cands')"
......@@ -96,12 +96,12 @@ declare poly_mod.inv_M2_def[code]
declare poly_mod.inv_Mp2_def[code_unfold]
definition zassenhaus_reconstruction_generic ::
"(int poly, int \<times> int poly list, 'state) sublists_foldr_impl
"(int poly, int \<times> int poly list, 'state) subseqs_foldr_impl
\<Rightarrow> int poly list \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> int poly \<Rightarrow> int poly list" where
"zassenhaus_reconstruction_generic sl_impl vs p n f = (let
lf = lead_coeff f;
pn = p^n;
(_, state) = sublists_foldr sl_impl (lf,[]) vs 0
(_, state) = subseqs_foldr sl_impl (lf,[]) vs 0
in
poly_mod.reconstruction pn sl_impl (pn div 2) state f (smult lf f) lf 0 (length vs) vs [] [])"
......@@ -131,7 +131,7 @@ proof -
qed
qed
lemma mset_sublists_size: "mset ` {ys. ys \<in> set (sublists xs) \<and> length ys = n} =
lemma mset_subseqs_size: "mset ` {ys. ys \<in> set (subseqs xs) \<and> length ys = n} =
{ws. ws \<subseteq># mset xs \<and> size ws = n}"
proof (induct xs arbitrary: n)
case (Cons x xs n)
......@@ -148,13 +148,13 @@ proof (induct xs arbitrary: n)
\<union> ((\<lambda> ps. ps + {#x#}) ` {ps. ps \<subseteq># mset xs \<and> size ps = m})" unfolding Suc by auto
finally have id: "?r =
{ps. ps \<subseteq># mset xs \<and> size ps = n} \<union> (\<lambda>ps. ps + {#x#}) ` {ps. ps \<subseteq># mset xs \<and> size ps = m}" .
have "?l = mset ` {ys \<in> set (sublists xs). length ys = Suc m}
\<union> mset ` {ys \<in> op # x ` set (sublists xs). length ys = Suc m}"
have "?l = mset ` {ys \<in> set (subseqs xs). length ys = Suc m}
\<union> mset ` {ys \<in> op # x ` set (subseqs xs). length ys = Suc m}"
unfolding Suc by (auto simp: Let_def)
also have "mset ` {ys \<in> op # x ` set (sublists xs). length ys = Suc m}
= (\<lambda>ps. ps + {#x#}) ` mset ` {ys \<in> set (sublists xs). length ys = m}" by force
finally have id': "?l = mset ` {ys \<in> set (sublists xs). length ys = Suc m} \<union>
(\<lambda>ps. ps + {#x#}) ` mset ` {ys \<in> set (sublists xs). length ys = m}" .
also have "mset ` {ys \<in> op # x ` set (subseqs xs). length ys = Suc m}
= (\<lambda>ps. ps + {#x#}) ` mset ` {ys \<in> set (subseqs xs). length ys = m}" by force
finally have id': "?l = mset ` {ys \<in> set (subseqs xs). length ys = Suc m} \<union>
(\<lambda>ps. ps + {#x#}) ` mset ` {ys \<in> set (subseqs xs). length ys = m}" .
show ?thesis unfolding id id' Cons[symmetric] unfolding Suc by simp
qed
qed auto
......@@ -202,12 +202,12 @@ lemma mul_const_commute_below: "mul_const x (mul_const y z) = mul_const y (mul_c
context
fixes p n
and sl_impl :: "(int poly, int \<times> int poly list, 'state)sublists_foldr_impl"
and sl_impl :: "(int poly, int \<times> int poly list, 'state)subseqs_foldr_impl"
and sli :: "int \<times> int poly list \<Rightarrow> int poly list \<Rightarrow> nat \<Rightarrow> 'state \<Rightarrow> bool"
assumes prime: "prime p"
and m: "m = p^n"
and n: "n \<noteq> 0"
and sl_impl: "correct_sublists_foldr_impl (\<lambda>x. map_prod (mul_const x) (Cons x)) sl_impl sli"
and sl_impl: "correct_subseqs_foldr_impl (\<lambda>x. map_prod (mul_const x) (Cons x)) sl_impl sli"
begin
private definition "test_dvd_exec lu u ws = (\<not> inv_Mp (Mp (smult lu (prod_mset ws))) dvd smult lu u)"
......@@ -239,7 +239,7 @@ qed
lemma coprime_exp_mod: "coprime lu p \<Longrightarrow> prime p \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lu mod p ^ n \<noteq> 0"
by (metis coprime_exp inverse_mod m m1 mod_0 mod_mult_eq mult_zero_right zero_neq_one)
interpretation correct_sublists_foldr_impl "\<lambda>x. map_prod (mul_const x) (Cons x)" sl_impl sli by fact
interpretation correct_subseqs_foldr_impl "\<lambda>x. map_prod (mul_const x) (Cons x)" sl_impl sli by fact
lemma reconstruction: assumes
res: "reconstruction sl_impl m2 state u (smult lu u) lu d r vs res cands = fs"
......@@ -275,7 +275,7 @@ proof -
have wf: "wf R" unfolding R_def by simp
have mset_snd_S: "\<And> vs lu d. (mset \<circ> snd) ` S (lu,[]) vs d =
{ ws. ws \<subseteq># mset vs \<and> size ws = d}"
by (fold mset_sublists_size image_comp, unfold S_def image_Collect, auto)
by (fold mset_subseqs_size image_comp, unfold S_def image_Collect, auto)
have inv_M2[simp]: "inv_M2 m2 = inv_M" unfolding inv_M2_def m2 inv_M_def
by (intro ext, auto)
have inv_Mp2[simp]: "inv_Mp2 m2 = inv_Mp" unfolding inv_Mp2_def inv_Mp_def by simp
......@@ -426,10 +426,10 @@ proof -
next
case False
with dr have dr: "?d' + ?d' \<le> r" and dr': "?d' < r" by auto
obtain state' cands' where sln: "next_sublists_foldr sl_impl state = (cands',state')" by force
from next_sublists_foldr[OF sln state] have state': "sli (lu,[]) vs (Suc d) state'"
obtain state' cands' where sln: "next_subseqs_foldr sl_impl state = (cands',state')" by force
from next_subseqs_foldr[OF sln state] have state': "sli (lu,[]) vs (Suc d) state'"
and cands': "set cands' = S (lu,[]) vs (Suc d)" by auto
let ?new = "sublists_length mul_const lu ?d' vs"
let ?new = "subseqs_length mul_const lu ?d' vs"
have R: "((r - Suc d, cands'), meas) \<in> R" unfolding meas R_def using False by auto
from res False sln
have fact: "reconstruction sl_impl m2 state' u ?luu lu ?d' r vs res cands' = fs" by auto
......@@ -454,10 +454,10 @@ proof -
let ?lv = "inv_M lv'"
define vb where "vb \<equiv> inv_Mp (Mp (smult lu (prod_list ws)))"
note res = res[unfolded Cons c list.simps split]
from cands[unfolded Cons c S_def] have ws: "ws \<in> set (sublists vs)" "length ws = d"
from cands[unfolded Cons c S_def] have ws: "ws \<in> set (subseqs vs)" "length ws = d"
and lv'': "lv' = foldr mul_const ws lu" by auto
from sublists_sub_mset[OF ws(1)] have ws_vs: "mset ws \<subseteq># mset vs" "set ws \<subseteq> set vs"
using set_mset_mono sublists_length_simple_False by auto fastforce
from subseqs_sub_mset[OF ws(1)] have ws_vs: "mset ws \<subseteq># mset vs" "set ws \<subseteq> set vs"
using set_mset_mono subseqs_length_simple_False by auto fastforce
have mon_ws: "monic (prod_mset (mset ws))"
by (rule monic_prod_mset, insert ws_vs vs_mi, auto)
have l_ws: "lead_coeff (prod_mset (mset ws)) = 1" using mon_ws .
......@@ -569,13 +569,13 @@ proof -
define lu' where "lu' \<equiv> lead_coeff u'"
let ?luu' = "smult lu' u'"
define vs' where "vs' \<equiv> fold remove1 ws vs"
obtain state' cands' where slc: "sublists_foldr sl_impl (lu',[]) vs' d = (cands', state')" by force
from sublists_foldr[OF slc] have state': "sli (lu',[]) vs' d state'"
obtain state' cands' where slc: "subseqs_foldr sl_impl (lu',[]) vs' d = (cands', state')" by force
from subseqs_foldr[OF slc] have state': "sli (lu',[]) vs' d state'"
and cands': "set cands' = S (lu',[]) vs' d" by auto
let ?res' = "pp_vb # res"
let ?r' = "r - length ws"
note defs = vb_def pp_vb_def u'_def lu'_def vs'_def slc
from fold_remove1_mset[OF sublists_sub_mset[OF ws(1)]]
from fold_remove1_mset[OF subseqs_sub_mset[OF ws(1)]]
have vs_split: "mset vs = mset vs' + mset ws" unfolding vs'_def by auto
hence vs'_diff: "mset vs' = mset vs - mset ws" and ws_sub: "mset ws \<subseteq># mset vs" by auto
from arg_cong[OF vs_split, of size]
......@@ -782,12 +782,12 @@ qed
end
end
(* select implementation of sublists *)
(* select implementation of subseqs *)
definition zassenhaus_reconstruction ::
"int poly list \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> int poly \<Rightarrow> int poly list" where
"zassenhaus_reconstruction vs p n f = (let
mul = poly_mod.mul_const (p^n);
sl_impl = my_sublists.impl (\<lambda>x. map_prod (mul x) (Cons x))
sl_impl = my_subseqs.impl (\<lambda>x. map_prod (mul x) (Cons x))
in zassenhaus_reconstruction_generic sl_impl vs p n f)"
context
......@@ -827,7 +827,7 @@ qed
lemma zassenhaus_reconstruction_generic:
assumes sl_impl: "correct_sublists_foldr_impl (\<lambda>v. map_prod (poly_mod.mul_const (p^n) v) (Cons v)) sl_impl sli"
assumes sl_impl: "correct_subseqs_foldr_impl (\<lambda>v. map_prod (poly_mod.mul_const (p^n) v) (Cons v)) sl_impl sli"
and res: "zassenhaus_reconstruction_generic sl_impl hs p n f = fs"
shows "f = prod_list fs \<and> (\<forall> fi \<in> set fs. irreducible\<^sub>d fi)"
proof -
......@@ -836,9 +836,9 @@ proof -
let ?q = "p^n"
have p1: "p > 1" using prime unfolding prime_int_iff by simp
interpret poly_mod_2 "p^n" using p1 n unfolding poly_mod_2_def by simp
obtain cands state where slc: "sublists_foldr sl_impl (lead_coeff f, []) hs 0 = (cands, state)" by force
interpret correct_sublists_foldr_impl "\<lambda>x. map_prod (mul_const x) (Cons x)" sl_impl sli by fact
from sublists_foldr[OF slc] have state: "sli (lead_coeff f, []) hs 0 state" by auto
obtain cands state where slc: "subseqs_foldr sl_impl (lead_coeff f, []) hs 0 = (cands, state)" by force
interpret correct_subseqs_foldr_impl "\<lambda>x. map_prod (mul_const x) (Cons x)" sl_impl sli by fact
from subseqs_foldr[OF slc] have state: "sli (lead_coeff f, []) hs 0 state" by auto
from res[unfolded zassenhaus_reconstruction_generic_def bh split Let_def slc fst_conv]
have res: "reconstruction sl_impl (?q div 2) state f ?ff ?lc 0 (length hs) hs [] [] = fs" by auto
from berlekamp_hensel_unique[OF prime cop sf bh n]
......@@ -878,7 +878,7 @@ proof -
interpret poly_mod_prime by (unfold_locales, rule prime)
from m1 n have pn: "p^n > 1" by simp
show ?thesis
by (rule zassenhaus_reconstruction_generic[OF my_sublists.impl_correct
by (rule zassenhaus_reconstruction_generic[OF my_subseqs.impl_correct
res[unfolded zassenhaus_reconstruction_def Let_def]])
qed
end
......
......@@ -880,53 +880,53 @@ context PreCoxeterSystemWithDeletion
begin
lemma deletion_reduce:
"ss \<in> lists S \<Longrightarrow> \<exists>ts. ts \<in> ssublists ss \<inter> reduced_words_for S (sum_list ss)"
"ss \<in> lists S \<Longrightarrow> \<exists>ts. ts \<in> ssubseqs ss \<inter> reduced_words_for S (sum_list ss)"
proof (cases "S_reduced ss")
case True
thus "ss \<in> lists S \<Longrightarrow>
\<exists>ts. ts \<in> ssublists ss \<inter> reduced_words_for S (sum_list ss)"
by (force simp add: ssublists_refl)
\<exists>ts. ts \<in> ssubseqs ss \<inter> reduced_words_for S (sum_list ss)"
by (force simp add: ssubseqs_refl)
next
case False
have "ss \<in> lists S \<Longrightarrow> \<not> S_reduced ss \<Longrightarrow>
\<exists>ts. ts \<in> ssublists ss \<inter> reduced_words_for S (sum_list ss)"
\<exists>ts. ts \<in> ssubseqs ss \<inter> reduced_words_for S (sum_list ss)"
proof (induct ss rule: length_induct)
fix xs::"'w list"
assume xs:
"\<forall>ys. length ys < length xs \<longrightarrow> ys \<in> lists S \<longrightarrow> \<not> S_reduced ys
\<longrightarrow> (\<exists>ts. ts \<in> ssublists ys \<inter> reduced_words_for S (sum_list ys))"
\<longrightarrow> (\<exists>ts. ts \<in> ssubseqs ys \<inter> reduced_words_for S (sum_list ys))"
"xs \<in> lists S" "\<not> S_reduced xs"
from xs(2,3) obtain as a bs b cs
where asbscs: "xs = as@[a]@bs@[b]@cs" "sum_list xs = sum_list (as@bs@cs)"
using deletion[of xs]
by fast
show "\<exists>ts. ts \<in> ssublists xs \<inter> reduced_words_for S (sum_list xs)"
show "\<exists>ts. ts \<in> ssubseqs xs \<inter> reduced_words_for S (sum_list xs)"
proof (cases "S_reduced (as@bs@cs)")
case True with asbscs xs(2) show ?thesis
using delete2_ssublists by fastforce
using delete2_ssubseqs by fastforce
next
case False
moreover from asbscs(1) xs(2)
have "length (as@bs@cs) < length xs" "as@bs@cs \<in> lists S"
by auto
ultimately obtain ts
where ts: "ts \<in> ssublists (as@bs@cs) \<inter>
where ts: "ts \<in> ssubseqs (as@bs@cs) \<inter>
reduced_words_for S (sum_list (as@bs@cs))"
using xs(1,2) asbscs(1)
by fast
with asbscs show ?thesis
using delete2_ssublists[of as bs cs a b] ssublists_subset by auto
using delete2_ssubseqs[of as bs cs a b] ssubseqs_subset by auto
qed
qed
with False
show "ss \<in> lists S \<Longrightarrow>
\<exists>ts. ts \<in> ssublists ss \<inter> reduced_words_for S (sum_list ss)"
\<exists>ts. ts \<in> ssubseqs ss \<inter> reduced_words_for S (sum_list ss)"
by fast
qed
lemma deletion_reduce':
"ss \<in> lists S \<Longrightarrow> \<exists>ts\<in>reduced_words_for S (sum_list ss). set ts \<subseteq> set ss"
using deletion_reduce[of ss] sublists_powset[of ss] by auto
using deletion_reduce[of ss] subseqs_powset[of ss] by auto
end (* context PreCoxeterSystemWithDeletion *)
......@@ -1286,10 +1286,10 @@ lemma special_subgroup_word_length:
proof-
from assms obtain ts where ts: "ts \<in> lists T" "w = sum_list ts"
using special_subgroup_eq_sum_list by auto
with assms(1) obtain us where "us \<in> ssublists ts" "S_reduced_for w us"
with assms(1) obtain us where "us \<in> ssubseqs ts" "S_reduced_for w us"
using deletion_reduce[of ts] by fast
with assms(1) ts(1) show ?thesis
using ssublists_lists[of ts] reduced_word_for_sum_list
using ssubseqs_lists[of ts] reduced_word_for_sum_list
is_arg_min_size_subprop[of length "word_for S w" us "word_for T w"]
unfolding reduced_word_for_def word_length_def
by fast
......
......@@ -920,55 +920,55 @@ proof (induct xs arbitrary: x)
case Cons with assms show ?case using binrelchain_Cons_reduce by auto
qed (simp add: assms)
subsubsection {* Set of sublists *}
subsubsection {* Set of subseqs *}
lemma sublists_Cons: "sublists (x#xs) = map (Cons x) (sublists xs) @ (sublists xs)"
using cong_let[of "sublists xs" "\<lambda>xss. map (Cons x) xss @ xss"] by simp
lemma subseqs_Cons: "subseqs (x#xs) = map (Cons x) (subseqs xs) @ (subseqs xs)"
using cong_let[of "subseqs xs" "\<lambda>xss. map (Cons x) xss @ xss"] by simp
abbreviation "ssublists xs \<equiv> set (sublists xs)"
abbreviation "ssubseqs xs \<equiv> set (subseqs xs)"
lemma nil_ssublists: "[] \<in> ssublists xs"
lemma nil_ssubseqs: "[] \<in> ssubseqs xs"
proof (induct xs)
case (Cons x xs) thus ?case using sublists_Cons[of x] by simp
case (Cons x xs) thus ?case using subseqs_Cons[of x] by simp
qed simp
lemma ssublists_Cons: "ssublists (x#xs) = (Cons x) ` (ssublists xs) \<union> ssublists xs"
using sublists_Cons[of x] by simp
lemma ssubseqs_Cons: "ssubseqs (x#xs) = (Cons x) ` (ssubseqs xs) \<union> ssubseqs xs"
using subseqs_Cons[of x] by simp
lemma ssublists_refl: "xs \<in> ssublists xs"
lemma ssubseqs_refl: "xs \<in> ssubseqs xs"
proof (induct xs)
case (Cons x xs) thus ?case using ssublists_Cons by fast
qed (rule nil_ssublists)
case (Cons x xs) thus ?case using ssubseqs_Cons by fast
qed (rule nil_ssubseqs)
lemma ssublists_subset: "as \<in> ssublists bs \<Longrightarrow> ssublists as \<subseteq> ssublists bs"
lemma ssubseqs_subset: "as \<in> ssubseqs bs \<Longrightarrow> ssubseqs as \<subseteq> ssubseqs bs"
proof (induct bs arbitrary: as)
case (Cons b bs) show ?case
proof (cases "as \<in> set (sublists bs)")
case True with Cons show ?thesis using ssublists_Cons by fastforce
proof (cases "as \<in> set (subseqs bs)")
case True with Cons show ?thesis using ssubseqs_Cons by fastforce
next
case False with Cons show ?thesis
using nil_ssublists[of "b#bs"] ssublists_Cons[of "hd as"] ssublists_Cons[of b]
using nil_ssubseqs[of "b#bs"] ssubseqs_Cons[of "hd as"] ssubseqs_Cons[of b]
by (cases as) auto
qed
qed simp
lemma ssublists_lists:
"as \<in> lists A \<Longrightarrow> bs \<in> ssublists as \<Longrightarrow> bs \<in> lists A"
lemma ssubseqs_lists:
"as \<in> lists A \<Longrightarrow> bs \<in> ssubseqs as \<Longrightarrow> bs \<in> lists A"
proof (induct as arbitrary: bs)
case (Cons a as) thus ?case using ssublists_Cons[of a] by fastforce
case (Cons a as) thus ?case using ssubseqs_Cons[of a] by fastforce
qed simp
lemma delete1_ssublists:
"as@bs \<in> ssublists (as@[a]@bs)"
lemma delete1_ssubseqs:
"as@bs \<in> ssubseqs (as@[a]@bs)"
proof (induct as)
case Nil show ?case using ssublists_refl ssublists_Cons[of a bs] by auto
case Nil show ?case using ssubseqs_refl ssubseqs_Cons[of a bs] by auto
next
case (Cons x xs) thus ?case using ssublists_Cons[of x] by simp
case (Cons x xs) thus ?case using ssubseqs_Cons[of x] by simp
qed
lemma delete2_ssublists:
"as@bs@cs \<in> ssublists (as@[a]@bs@[b]@cs)"
using delete1_ssublists[of "as@[a]@bs"] delete1_ssublists ssublists_subset
lemma delete2_ssubseqs:
"as@bs@cs \<in> ssubseqs (as@[a]@bs@[b]@cs)"
using delete1_ssubseqs[of "as@[a]@bs"] delete1_ssubseqs ssubseqs_subset
by fastforce
......
......@@ -203,11 +203,11 @@ instantiation set :: (cenum) cenum begin
definition
"CENUM('a set) =
(case ID CENUM('a) of None \<Rightarrow> None | Some (enum_a, enum_all_a, enum_ex_a) \<Rightarrow> Some
(map set (sublists enum_a),
\<lambda>P. list_all P (map set (sublists enum_a)),
\<lambda>P. list_ex P (map set (sublists enum_a))))"
(map set (subseqs enum_a),
\<lambda>P. list_all P (map set (subseqs enum_a)),
\<lambda>P. list_ex P (map set (subseqs enum_a))))"
instance
by(intro_classes)(auto simp add: cEnum_set_def sublists_powset list_ex_iff list_all_iff split: option.split_asm dest!: ID_cEnum)
by(intro_classes)(auto simp add: cEnum_set_def subseqs_powset list_ex_iff list_all_iff split: option.split_asm dest!: ID_cEnum)
end
instantiation unit :: cenum begin
......
......@@ -484,13 +484,13 @@ lemma order_A:
shows "order (A ws) = 2 * N_half" using dims_A length_replicate by auto
lemma dims_A':
shows "dim\<^sub>r (A' ws) = prod_list (sublist (Tensor.dims (A ws)) {n. even n})"
and "dim\<^sub>c (A' ws) = prod_list (sublist (Tensor.dims (A ws)) {n. odd n})"
shows "dim\<^sub>r (A' ws) = prod_list (nths (Tensor.dims (A ws)) {n. even n})"
and "dim\<^sub>c (A' ws) = prod_list (nths (Tensor.dims (A ws)) {n. odd n})"
unfolding A'_def matricize_def by (simp_all add: A_def Collect_neg_eq)
lemma dims_A'_pow:
shows "dim\<^sub>r (A' ws) = (last rs) ^ N_half" "dim\<^sub>c (A' ws) = (last rs) ^ N_half"
unfolding dims_A' dims_A sublist_replicate set_le_in card_even card_odd prod_list_replicate
unfolding dims_A' dims_A nths_replicate set_le_in card_even card_odd prod_list_replicate
by simp_all
......@@ -519,8 +519,8 @@ lemma order_Aw: "order Aw = 2 * N_half"
unfolding Aw_def' using order_A by auto
lemma dims_Aw':
"dim\<^sub>r Aw' = prod_list (sublist (Tensor.dims Aw) {n. even n})"
"dim\<^sub>c Aw' = prod_list (sublist (Tensor.dims Aw) {n. odd n})"
"dim\<^sub>r Aw' = prod_list (nths (Tensor.dims Aw) {n. even n})"
"dim\<^sub>c Aw' = prod_list (nths (Tensor.dims Aw) {n. odd n})"
unfolding Aw'_def' Aw_def' using dims_A' by auto
lemma dims_Aw'_pow: "dim\<^sub>r Aw' = (last rs) ^ N_half" "dim\<^sub>c Aw' = (last rs) ^ N_half"
......@@ -529,7 +529,7 @@ lemma dims_Aw'_pow: "dim\<^sub>r Aw' = (last rs) ^ N_half" "dim\<^sub>c Aw' = (l
lemma witness_tensor:
assumes "is \<lhd> Tensor.dims Aw"
shows "Tensor.lookup Aw is
= (if sublist is {n. even n} = sublist is {n. odd n} \<and> (\<forall>i\<in>set is. i < last (butlast rs)) then 1 else 0)"
= (if nths is {n. even n} = nths is {n. odd n} \<and> (\<forall>i\<in>set is. i < last (butlast rs)) then 1 else 0)"
using assms deep no_zeros y_valid unfolding Aw_def proof (induction "butlast (butlast (butlast rs))" arbitrary:rs "is" y)
case Nil
have "length rs = 3"
......@@ -548,23 +548,23 @@ using assms deep no_zeros y_valid unfolding Aw_def proof (induction "butlast (bu
= (if is ! 0 = is ! 1 \<and> is ! 0 < rs ! 1 then 1 else 0)"
using Nil.prems(4) \<open>rs = [rs ! 0, rs ! 1, rs ! 2]\<close> by (metis list.sel(3) lookup_tensors_ht_l1)
have "is ! 0 = is ! 1 \<and> is ! 0 < rs ! 1
\<longleftrightarrow> sublist is {n. even n} = sublist is {n. odd n} \<and> (\<forall>i\<in>set is. i < last (butlast rs))"
\<longleftrightarrow> nths is {n. even n} = nths is {n. odd n} \<and> (\<forall>i\<in>set is. i < last (butlast rs))"
proof -
have "length is = 2" by (metis One_nat_def Suc_eq_plus1 \<open>is \<lhd> [rs ! 2, rs ! 2]\<close> list.size(3) list.size(4) numeral_2_eq_2 valid_index_length)
have "sublist is {n. even n} = [is!0]"
apply (rule sublist_only_one)
have "nths is {n. even n} = [is!0]"
apply (rule nths_only_one)
using subset_antisym less_2_cases `length is = 2` by fastforce
have "sublist is {n. odd n} = [is!1]"
apply (rule sublist_only_one)
have "nths is {n. odd n} = [is!1]"
apply (rule nths_only_one)
using subset_antisym less_2_cases `length is = 2` by fastforce
have "last (butlast rs) = rs!1" by (metis One_nat_def Suc_eq_plus1 \<open>rs = [rs ! 0, rs ! 1, rs ! 2]\<close>
append_butlast_last_id last_conv_nth length_butlast length_tl lessI list.sel(3) list.simps(3)
list.size(3) list.size(4) nat.simps(3) nth_append)
show ?thesis unfolding `last (butlast rs) = rs!1`
apply (rule iffI; rule conjI)
apply (simp add: \<open>sublist is (Collect even) = [is ! 0]\<close> \<open>sublist is {n. odd n} = [is ! 1]\<close>)
apply (simp add: \<open>nths is (Collect even) = [is ! 0]\<close> \<open>nths is {n. odd n} = [is ! 1]\<close>)
apply (metis `length is = 2` One_nat_def in_set_conv_nth less_2_cases)
apply (simp add: \<open>sublist is (Collect even) = [is ! 0]\<close> \<open>sublist is {n. odd n} = [is ! 1]\<close>)
apply (simp add: \<open>nths is (Collect even) = [is ! 0]\<close> \<open>nths is {n. odd n} = [is ! 1]\<close>)
apply (simp add: \<open>length is = 2\<close>)
done
qed
......@@ -584,7 +584,7 @@ next
have 4:"0 < (tl rs) ! 0" using "2" "3" by auto
have IH: "\<And>is'. is' \<lhd> Tensor.dims (tensors_from_net (witness_l (tl rs)) $ 0)
\<Longrightarrow> Tensor.lookup (tensors_from_net (witness_l (tl rs)) $ 0) is' =
(if sublist is' (Collect even) = sublist is' {n. odd n} \<and> (\<forall>i\<in>set is'. i < last (butlast (tl rs))) then 1 else 0)"
(if nths is' (Collect even) = nths is' {n. odd n} \<and> (\<forall>i\<in>set is'. i < last (butlast (tl rs))) then 1 else 0)"
using "1" "2" "3" 4 Cons.hyps(1) by blast
text \<open>The list "is" can be split in two parts:\<close>
......@@ -610,7 +610,7 @@ next
qed
text \<open>A shorthand for the condition to find a "1" in the tensor:\<close>
let ?cond = "\<lambda>is rs. sublist is {n. even n} = sublist is {n. odd n} \<and> (\<forall>i\<in>set is. i < last (butlast rs))"
let ?cond = "\<lambda>is rs. nths is {n. even n} = nths is {n. odd n} \<and> (\<forall>i\<in>set is. i < last (butlast rs))"
text \<open>We can use the IH on our newly created is1 and is2:\<close>
have IH_is12:
......@@ -634,13 +634,13 @@ next
length_butlast length_tl list.size(4) one_add_one zero_less_Suc)+
then have "{j. j + length is1 \<in> {n. even n}} = {n. even n}"
"{j. j + length is1 \<in> {n. odd n}} = {n. odd n}" by simp_all
have "length (sublist is2 (Collect even)) = length (sublist is2 (Collect odd))"
using length_sublist_even \<open>even (length is2)\<close> by blast
have cond1_iff: "(sublist is1 (Collect even) = sublist is1 {n. odd n} \<and> sublist is2 (Collect even) = sublist is2 {n. odd n})
= (sublist is (Collect even) = sublist is {n. odd n})"
unfolding `is = is1 @ is2` sublist_append
have "length (nths is2 (Collect even)) = length (nths is2 (Collect odd))"
using length_nths_even \<open>even (length is2)\<close> by blast
have cond1_iff: "(nths is1 (Collect even) = nths is1 {n. odd n} \<and> nths is2 (Collect even) = nths is2 {n. odd n})
= (nths is (Collect even) = nths is {n. odd n})"
unfolding `is = is1 @ is2` nths_append
`{j. j + length is1 \<in> {n. odd n}} = {n. odd n}` `{j. j + length is1 \<in> {n. even n}} = {n. even n}`
by (simp add: \<open>length (sublist is2 (Collect even)) = length (sublist is2 (Collect odd))\<close>)
by (simp add: \<open>length (nths is2 (Collect even)) = length (nths is2 (Collect odd))\<close>)
have "last (butlast (tl rs)) = last (butlast rs)" using Nitpick.size_list_simp(2) \<open>even (length is1)\<close>
\<open>length is1 = 2 ^ (length (tl rs) - 2)\<close> butlast_tl last_tl length_butlast length_tl not_less_eq zero_less_diff
by (metis (full_types) Cons.hyps(2) length_Cons less_nat_zero_code)
......@@ -703,11 +703,11 @@ qed
lemma witness_matricization:
assumes "i < dim\<^sub>r Aw'" and "j < dim\<^sub>c Aw'"
shows "Aw' $$ (i, j)
= (if i=j \<and> (\<forall>i0\<in>set (digit_encode (sublist (Tensor.dims Aw) {n. even n}) i). i0 < last (butlast rs)) then 1 else 0)"
= (if i=j \<and> (\<forall>i0\<in>set (digit_encode (nths (Tensor.dims Aw) {n. even n}) i). i0 < last (butlast rs)) then 1 else 0)"
proof -
def "is" == "weave {n. even n}
(digit_encode (sublist (Tensor.dims Aw) {n. even n}) i)
(digit_encode (sublist (Tensor.dims Aw) {n. odd n}) j)"
(digit_encode (nths (Tensor.dims Aw) {n. even n}) i)
(digit_encode (nths (Tensor.dims Aw) {n. odd n}) j)"
have lookup_eq: "Aw' $$ (i, j) = Tensor.lookup Aw is"
using Aw'_def matricize_def dims_Aw'(1)[symmetric, unfolded A_def] dims_Aw'(2)[symmetric, unfolded A_def Collect_neg_eq]
mat_index_mat(1)[OF `i < dim\<^sub>r Aw'` `j < dim\<^sub>c Aw'`] is_def Collect_neg_eq case_prod_conv
......@@ -719,45 +719,45 @@ proof -
have "even (order Aw)"
unfolding Aw_def using assms dims_output_witness even_numeral le_eq_less_or_eq numeral_2_eq_2 numeral_3_eq_3 deep no_zeros y_valid by fastforce
have sublist_dimsAw: "sublist (Tensor.dims Aw) (Collect even) = sublist (Tensor.dims Aw) {n. odd n}"
have nths_dimsAw: "nths (Tensor.dims Aw) (Collect even) = nths (Tensor.dims Aw) {n. odd n}"
proof -
have 0:"Tensor.dims (tensors_from_net (witness_l rs) $ y) = replicate (2 ^ (length rs - 2)) (last rs)"
using dims_output_witness[OF _ no_zeros y_valid] using deep by linarith
show ?thesis unfolding A_def
using sublist_replicate
by (metis (no_types, lifting) "0" Aw_def \<open>even (order Aw)\<close> length_replicate length_sublist_even)
using nths_replicate
by (metis (no_types, lifting) "0" Aw_def \<open>even (order Aw)\<close> length_replicate length_nths_even)
qed
have "i = j \<longleftrightarrow> sublist is (Collect even) = sublist is {n. odd n}"
have "i = j \<longleftrightarrow> nths is (Collect even) = nths is {n. odd n}"
proof
have eq_lengths: "length (digit_encode (sublist (Tensor.dims Aw) (Collect even)) i)
= length (digit_encode (sublist (Tensor.dims Aw) {n. odd n}) j)"
unfolding length_digit_encode by (metis \<open>even (order Aw)\<close> length_sublist_even)
then show "i = j \<Longrightarrow> sublist is (Collect even) = sublist is {n. odd n}" unfolding is_def
using sublist_weave[of "digit_encode (sublist (Tensor.dims Aw) (Collect even)) i"
"Collect even" "digit_encode (sublist (Tensor.dims Aw) {n. odd n}) j", unfolded eq_lengths, unfolded Collect_neg_eq[symmetric] card_even mult_2[symmetric] card_odd]
sublist_dimsAw by simp
show "sublist is (Collect even) = sublist is {n. odd n} \<Longrightarrow> i = j" unfolding is_def
using sublist_weave[of "digit_encode (sublist (Tensor.dims Aw) (Collect even)) i"
"Collect even" "digit_encode (sublist (Tensor.dims Aw) {n. odd n}) j", unfolded eq_lengths, unfolded Collect_neg_eq[symmetric] card_even mult_2[symmetric] card_odd]
using Divides.mod_less \<open>sublist (Tensor.dims Aw) (Collect even) = sublist (Tensor.dims Aw) {n. odd n}\<close>
have eq_lengths: "length (digit_encode (nths (Tensor.dims Aw) (Collect even)) i)
= length (digit_encode (nths (Tensor.dims Aw) {n. odd n}) j)"
unfolding length_digit_encode by (metis \<open>even (order Aw)\<close> length_nths_even)
then show "i = j \<Longrightarrow> nths is (Collect even) = nths is {n. odd n}" unfolding is_def
using nths_weave[of "digit_encode (nths (Tensor.dims Aw) (Collect even)) i"
"Collect even" "digit_encode (nths (Tensor.dims Aw) {n. odd n}) j", unfolded eq_lengths, unfolded Collect_neg_eq[symmetric] card_even mult_2[symmetric] card_odd]
nths_dimsAw by simp
show "nths is (Collect even) = nths is {n. odd n} \<Longrightarrow> i = j" unfolding is_def
using nths_weave[of "digit_encode (nths (Tensor.dims Aw) (Collect even)) i"
"Collect even" "digit_encode (nths (Tensor.dims Aw) {n. odd n}) j", unfolded eq_lengths, unfolded Collect_neg_eq[symmetric] card_even mult_2[symmetric] card_odd]
using Divides.mod_less \<open>nths (Tensor.dims Aw) (Collect even) = nths (Tensor.dims Aw) {n. odd n}\<close>
deep no_zeros y_valid assms digit_decode_encode dims_Aw' by metis
qed
have "i=j \<Longrightarrow> set (digit_encode (sublist (Tensor.dims Aw) {n. even n}) i) = set is"
unfolding is_def sublist_dimsAw
using set_weave[of "(digit_encode (sublist (Tensor.dims Aw) {n. odd n}) j)" "Collect even"
"(digit_encode (sublist (Tensor.dims Aw) {n. odd n}) j)",
have "i=j \<Longrightarrow> set (digit_encode (nths (Tensor.dims Aw) {n. even n}) i) = set is"
unfolding is_def nths_dimsAw
using set_weave[of "(digit_encode (nths (Tensor.dims Aw) {n. odd n}) j)" "Collect even"
"(digit_encode (nths (Tensor.dims Aw) {n. odd n}) j)",
unfolded mult_2[symmetric] card_even Collect_neg_eq[symmetric] card_odd]
Un_absorb card_even card_odd mult_2 by blast
then show ?thesis unfolding lookup_eq
using witness_tensor[OF `is \<lhd> Tensor.dims Aw`]
by (simp add: A_def \<open>(i = j) = (sublist is (Collect even) = sublist is {n. odd n})\<close>)
by (simp add: A_def \<open>(i = j) = (nths is (Collect even) = nths is {n. odd n})\<close>)
qed
definition "rows_with_1 = {i. (\<forall>i0\<in>set (digit_encode (sublist (Tensor.dims Aw) {n. even n}) i). i0 < last (butlast rs))}"
definition "rows_with_1 = {i. (\<forall>i0\<in>set (digit_encode (nths (Tensor.dims Aw) {n. even n}) i). i0 < last (butlast rs))}"
lemma card_low_digits:
assumes "m>0" "\<And>d. d\<in>set ds \<Longrightarrow> m \<le> d"
......@@ -822,62 +822,62 @@ qed
lemma card_rows_with_1: "card {i\<in>rows_with_1. i<dim\<^sub>r Aw'} = r ^ N_half"
proof -
have 1:"{i\<in>rows_with_1. i<dim\<^sub>r Aw'} = {i. i < prod_list (sublist (Tensor.dims Aw) (Collect even)) \<and>
(\<forall>i0\<in>set (digit_encode (sublist (Tensor.dims Aw) (Collect even)) i). i0 < r)}" (is "?A = ?B")
have 1:"{i\<in>rows_with_1. i<dim\<^sub>r Aw'} = {i. i < prod_list (nths (Tensor.dims Aw) (Collect even)) \<and>
(\<forall>i0\<in>set (digit_encode (nths (Tensor.dims Aw) (Collect even)) i). i0 < r)}" (is "?A = ?B")
proof (rule subset_antisym; rule subsetI)
fix i assume "i \<in> ?A"
then have "i < dim\<^sub>r Aw'" "\<forall>i0\<in>set (digit_encode (sublist (Tensor.dims Aw) {n. even n}) i). i0 < last (butlast rs)"
then have "i < dim\<^sub>r Aw'" "\<forall>i0\<in>set (digit_encode (nths (Tensor.dims Aw) {n. even n}) i). i0 < last (butlast rs)"
using rows_with_1_def by auto
then have "i < prod_list (sublist (dims Aw) (Collect even))" using dims_Aw' by linarith
then have "digit_encode (sublist (dims Aw) (Collect even)) i \<lhd> sublist (dims Aw) (Collect even)"
then have "i < prod_list (nths (dims Aw) (Collect even))" using dims_Aw' by linarith
then have "digit_encode (nths (dims Aw) (Collect even)) i \<lhd> nths (dims Aw) (Collect even)"
using digit_encode_valid_index by auto
have "\<forall>i0\<in>set (digit_encode (sublist (Tensor.dims Aw) {n. even n}) i). i0 < r"
have "\<forall>i0\<in>set (digit_encode (nths (Tensor.dims Aw) {n. even n}) i). i0 < r"
proof
fix i0 assume 1:"i0 \<in> set (digit_encode (sublist (dims Aw) (Collect even)) i)"
then obtain k where "k < length (digit_encode (sublist (dims Aw) (Collect even)) i)"
"digit_encode (sublist (dims Aw) (Collect even)) i ! k = i0" by (meson in_set_conv_nth)
fix i0 assume 1:"i0 \<in> set (digit_encode (nths (dims Aw) (Collect even)) i)"
then obtain k where "k < length (digit_encode (nths (dims Aw) (Collect even)) i)"
"digit_encode (nths (dims Aw) (Collect even)) i ! k = i0" by (meson in_set_conv_nth)
have "i0 < last (butlast rs)"
using \<open>\<forall>i0\<in>set (digit_encode (sublist (dims Aw) (Collect even)) i). i0 < last (butlast rs)\<close> 1 by blast
have "set (sublist (dims Aw) (Collect even)) \<subseteq> {last rs}" unfolding dims_Aw using subset_eq by fastforce
then have "sublist (dims Aw) (Collect even) ! k = last rs"
using \<open>digit_encode (sublist (dims Aw) (Collect even)) i \<lhd> sublist (dims Aw) (Collect even)\<close>
\<open>k < length (digit_encode (sublist (dims Aw) (Collect even)) i)\<close>
using \<open>\<forall>i0\<in>set (digit_encode (nths (dims Aw) (Collect even)) i). i0 < last (butlast rs)\<close> 1 by blast
have "set (nths (dims Aw) (Collect even)) \<subseteq> {last rs}" unfolding dims_Aw using subset_eq by fastforce
then have "nths (dims Aw) (Collect even) ! k = last rs"
using \<open>digit_encode (nths (dims Aw) (Collect even)) i \<lhd> nths (dims Aw) (Collect even)\<close>
\<open>k < length (digit_encode (nths (dims Aw) (Collect even)) i)\<close>
nth_mem valid_index_length by auto
then have "i0 < last rs"
using valid_index_lt \<open>digit_encode (sublist (dims Aw) (Collect even)) i ! k = i0\<close>
\<open>digit_encode (sublist (dims Aw) (Collect even)) i \<lhd> sublist (dims Aw) (Collect even)\<close>
\<open>k < length (digit_encode (sublist (dims Aw) (Collect even)) i)\<close> valid_index_length by fastforce
using valid_index_lt \<open>digit_encode (nths (dims Aw) (Collect even)) i ! k = i0\<close>
\<open>digit_encode (nths (dims Aw) (Collect even)) i \<lhd> nths (dims Aw) (Collect even)\<close>
\<open>k < length (digit_encode (nths (dims Aw) (Collect even)) i)\<close> valid_index_length by fastforce
then show "i0 < r" unfolding r_def by (simp add: \<open>i0 < last (butlast rs)\<close>)
qed
then show "i \<in> ?B" using \<open>i < prod_list (sublist (dims Aw) (Collect even))\<close> by blast
then show "i \<in> ?B" using \<open>i < prod_list (nths (dims Aw) (Collect even))\<close> by blast
next
fix i assume "i\<in>?B"
then show "i\<in>?A" by (simp add: dims_Aw' r_def rows_with_1_def)
qed
have 2:"\<And>d. d \<in> set (sublist (Tensor.dims Aw) (Collect even)) \<Longrightarrow> r \<le> d"
have 2:"\<And>d. d \<in> set (nths (Tensor.dims Aw) (Collect even)) \<Longrightarrow> r \<le> d"
proof -
fix d assume "d \<in> set (sublist (Tensor.dims Aw) (Collect even))"
then have "d \<in> set (Tensor.dims Aw)" using in_set_sublistD by fast
fix d assume "d \<in> set (nths (Tensor.dims Aw) (Collect even))"
then have "d \<in> set (Tensor.dims Aw)" using in_set_nthsD by fast
then have "d = last rs" using dims_Aw by simp
then show "r \<le> d" by (simp add: r_def)
qed
have 3:"0 < r" unfolding r_def by (metis deep diff_diff_cancel diff_zero dual_order.trans in_set_butlastD last_in_set length_butlast list.size(3) min_def nat_le_linear no_zeros not_numeral_le_zero numeral_le_one_iff rel_simps(3))
have 4: "length (sublist (Tensor.dims Aw) (Collect even)) = N_half"
unfolding length_sublist order_Aw using card_even[of N_half]
have 4: "length (nths (Tensor.dims Aw) (Collect even)) = N_half"
unfolding length_nths order_Aw using card_even[of N_half]
by (metis (mono_tags, lifting) Collect_cong)
then show ?thesis using card_low_digits[of "r" "sublist (Tensor.dims Aw) (Collect even)"] 1 2 3 4 by metis
then show ?thesis using card_low_digits[of "r" "nths (Tensor.dims Aw) (Collect even)"] 1 2 3 4 by metis
qed