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

Deep Learning: add types in defs

--HG--
branch : deep_learning
parent 5b050023d51e
...@@ -466,8 +466,10 @@ assumes y_valid:"y < rs ! 0" ...@@ -466,8 +466,10 @@ assumes y_valid:"y < rs ! 0"
begin begin
definition "A ws = tensors_from_net (insert_weights shared_weights (deep_model_l rs) ws) $ y" definition A :: "(nat \<Rightarrow> real) \<Rightarrow> real tensor"
definition "A' ws = ten2mat (A ws)" where "A ws = tensors_from_net (insert_weights shared_weights (deep_model_l rs) ws) $ y"
definition A' :: "(nat \<Rightarrow> real) \<Rightarrow> real mat"
where "A' ws = ten2mat (A ws)"
lemma dims_tensor_deep_model: lemma dims_tensor_deep_model:
......
...@@ -6,7 +6,8 @@ theory DL_Deep_Model_Poly ...@@ -6,7 +6,8 @@ theory DL_Deep_Model_Poly
imports DL_Deep_Model Polynomials.More_MPoly_Type Jordan_Normal_Form.Determinant imports DL_Deep_Model Polynomials.More_MPoly_Type Jordan_Normal_Form.Determinant
begin begin
definition "polyfun N f = (\<exists>p. vars p \<subseteq> N \<and> (\<forall>x. insertion x p = f x))" definition polyfun :: "nat set \<Rightarrow> ((nat \<Rightarrow> 'a::comm_semiring_1) \<Rightarrow> 'a) \<Rightarrow> bool"
where "polyfun N f = (\<exists>p. vars p \<subseteq> N \<and> (\<forall>x. insertion x p = f x))"
lemma polyfunI: "(\<And>P. (\<And>p. vars p \<subseteq> N \<Longrightarrow> (\<And>x. insertion x p = f x) \<Longrightarrow> P) \<Longrightarrow> P) \<Longrightarrow> polyfun N f" lemma polyfunI: "(\<And>P. (\<And>p. vars p \<subseteq> N \<Longrightarrow> (\<And>x. insertion x p = f x) \<Longrightarrow> P) \<Longrightarrow> P) \<Longrightarrow> polyfun N f"
unfolding polyfun_def by metis unfolding polyfun_def by metis
......
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