Commit e5985e30 authored by Alexander Bentkamp's avatar Alexander Bentkamp
Browse files

Deep Learning: remove out-dated TODOs

parent d9c6f5142370
......@@ -322,9 +322,6 @@ next
using `\<not>j<M` by (simp add: lookup_tensor0[OF assms(2)] `is \<noteq> [j, j]`)
(* TODO: move? *)
lemma list_of_vec_map: "list_of_vec xs = map (op $ xs) [0..<dim\<^sub>v xs]" by transfer auto
lemma lookup_tensors_ht_l1:
assumes "j < r1"
and "is \<lhd> [M,M]"
......@@ -26,6 +26,8 @@ lemma vec_of_list_index: "vec_of_list xs $ j = xs ! j"
lemma list_of_vec_index: "list_of_vec v ! j = v $ j"
by (metis vec_list vec_of_list_index)
lemma list_of_vec_map: "list_of_vec xs = map (op $ xs) [0..<dim\<^sub>v xs]" by transfer auto
definition "component_mult v w = vec (min (dim\<^sub>v v) (dim\<^sub>v w)) (\<lambda>i. v $ i * w $ i)"
definition vec_set::"'a vec \<Rightarrow> 'a set" ("set\<^sub>v")
This diff is collapsed.
......@@ -13,7 +13,6 @@ of the Lebesgue measure as follows. This version of the Lebesgue measure measure
from nat to real whose values are undefined for arguments higher than n. These "Extensional Function Spaces"
are defined in HOL/Library/FuncSet. \<close>
(* TODO: make abbrev *)
definition lborel_f :: "nat \<Rightarrow> (nat \<Rightarrow> real) measure" where
"lborel_f n = (\<Pi>\<^sub>M b\<in>{..<n}. lborel)"
......@@ -81,8 +81,7 @@ lift_definition smult :: "'a::{times,zero} \<Rightarrow> 'a mpoly \<Rightarrow>
is "\<lambda>a. (Groups.times a) :: ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) \<Rightarrow> _" .
(* left lemmas in subsection \<open>Pseudo-division of polynomials\<close>,
because I couldn't disentangle them and the notion of monomials.
TODO: investigate the !two! subsection \<open>Monomials\<close> in this thy. *)
because I couldn't disentangle them and the notion of monomials. *)
subsection \<open>Multiplicative structure\<close>
......@@ -394,23 +393,6 @@ lemma total_degree_one [simp]:
"total_degree 1 = 0"
by transfer simp
subsection \<open>Monomials\<close>
lemma mapping_of_monom [simp]:
"mapping_of (monom m a) = PP_Poly_Mapping.single m a"
by(fact monom.rep_eq)
text \<open>Naive construction of monomials\<close>
definition M :: "nat list \<Rightarrow> 'a::zero \<Rightarrow> 'a mpoly"
"M ms = monom (PP_Poly_Mapping.nth ms)"
declare [[code abort: monom]]
value "M [1,2,3] (2::int) + M [2,0,1] 3 + M [2,0,1] 7"
subsection \<open>Pseudo-division of polynomials\<close>
lemma smult_conv_mult: "smult s p = monom 0 s * p"
......@@ -294,8 +294,6 @@ proof -
ultimately show ?thesis using coeff_eq by auto
(* TODO: Beweis durch transfer möglich? *)
lemma mpoly_induct [case_names monom sum]:
assumes monom:"\<And>m a. P (monom m a)"
and sum:"(\<And>p1 p2 m a. P p1 \<Longrightarrow> P p2 \<Longrightarrow> p2 = (monom m a) \<Longrightarrow> m \<notin> keys (mapping_of p1) \<Longrightarrow> P (p1+p2))"
......@@ -80,6 +80,8 @@ shows "is1 @ is2 \<lhd> ds1 @ ds2"
using valid_index_lt[OF is2_valid] valid_index_lt[OF is1_valid] valid_index_length[OF is1_valid] valid_index_length[OF is2_valid] length_append
by (auto simp add: `length is1 = length ds1`)
lemma valid_index_list_all2_iff: "is \<lhd> ds \<longleftrightarrow> list_all2 (op <) is ds"
by (metis list_all2_conv_all_nth list_all2_nthD valid_indexI valid_index_length valid_index_lt)
definition fixed_length_sublist::"'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list" where
"fixed_length_sublist xs l i = (take l (drop (l*i) xs))"
This diff is collapsed.
......@@ -10,8 +10,6 @@ inductive cprank_max1::"'a::ring_1 tensor \<Rightarrow> bool" where
order1: "order A \<le> 1 \<Longrightarrow> cprank_max1 A" |
higher_order: "order A = 1 \<Longrightarrow> cprank_max1 B \<Longrightarrow> cprank_max1 (A \<otimes> B)"
(* TODO: Alternativen: über prod_list, oder immer order1 mit cprank1 multiplizieren (besser, da induct stärker). *)
lemma cprank_max1_order0: "cprank_max1 B \<Longrightarrow> order A = 0 \<Longrightarrow> cprank_max1 (A \<otimes> B)"
proof (induction B rule:cprank_max1.induct)
case order1
......@@ -6,8 +6,6 @@ theory Tensor_Unit_Vec
imports Tensor_Product
(* TODO:eventually remove completely, as it is mostly not necessary.*)
definition unit_vec::"nat \<Rightarrow> nat \<Rightarrow> 'a::ring_1 tensor"
where "unit_vec n i = tensor_from_lookup [n] (\<lambda>x. if x=[i] then 1 else 0)"
......@@ -23,7 +21,6 @@ proof -
then show ?thesis by auto
(* TODO:needed?*)
lemma subtensor_prod_with_unit_vec:
fixes A::"'a::ring_1 tensor"
assumes "j<n"
......@@ -39,7 +36,6 @@ proof -
by (metis (no_types, lifting) tensor_from_lookup_eqI)
(* TODO:needed?*)
lemma subtensor_decomposition:
assumes "dims A \<noteq> []"
shows "listsum (dims A) (map (\<lambda>i. unit_vec (hd (dims A)) i \<otimes> subtensor A i) [0..<hd (dims A)]) = A" (is "?LS = A")
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment