typed definitions
authornipkow
Sun Jan 06 12:32:01 2019 +0100 (4 months ago)
changeset 6960086e8e7347ac0
parent 69599 caa7e406056d
child 69606 157990515be1
typed definitions
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Sat Jan 05 20:12:02 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Jan 06 12:32:01 2019 +0100
     1.3 @@ -13,7 +13,8 @@
     1.4  
     1.5  subsection \<open>General notion of a topology as a value\<close>
     1.6  
     1.7 -definition%important "istopology L \<longleftrightarrow>
     1.8 +definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
     1.9 +"istopology L \<longleftrightarrow>
    1.10    L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
    1.11  
    1.12  typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
    1.13 @@ -113,7 +114,8 @@
    1.14  
    1.15  subsubsection \<open>Closed sets\<close>
    1.16  
    1.17 -definition%important "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
    1.18 +definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.19 +"closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
    1.20  
    1.21  lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
    1.22    by (metis closedin_def)
    1.23 @@ -230,7 +232,8 @@
    1.24  
    1.25  subsection \<open>Subspace topology\<close>
    1.26  
    1.27 -definition%important "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
    1.28 +definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
    1.29 +"subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
    1.30  
    1.31  lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
    1.32    (is "istopology ?L")
     2.1 --- a/src/HOL/Analysis/Inner_Product.thy	Sat Jan 05 20:12:02 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Sun Jan 06 12:32:01 2019 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     Brian Huffman
     2.5  *)
     2.6  
     2.7 -section \<open>Inner Product Spaces and the Gradient Derivative\<close>
     2.8 +section \<open>Inner Product Spaces and Gradient Derivative\<close>
     2.9  
    2.10  theory Inner_Product
    2.11  imports Complex_Main
     3.1 --- a/src/HOL/Analysis/L2_Norm.thy	Sat Jan 05 20:12:02 2019 +0100
     3.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Sun Jan 06 12:32:01 2019 +0100
     3.3 @@ -8,7 +8,8 @@
     3.4  imports Complex_Main
     3.5  begin
     3.6  
     3.7 -definition %important "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
     3.8 +definition%important L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
     3.9 +"L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
    3.10  
    3.11  lemma L2_set_cong:
    3.12    "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
     4.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Jan 05 20:12:02 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Jan 06 12:32:01 2019 +0100
     4.3 @@ -183,7 +183,9 @@
     4.4  
     4.5  subsection \<open>Bilinear functions\<close>
     4.6  
     4.7 -definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
     4.8 +definition%important
     4.9 +bilinear :: "('a::real_vector \<Rightarrow> 'b::real_vector \<Rightarrow> 'c::real_vector) \<Rightarrow> bool" where
    4.10 +"bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
    4.11  
    4.12  lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
    4.13    by (simp add: bilinear_def linear_iff)
    4.14 @@ -239,7 +241,8 @@
    4.15  
    4.16  subsection \<open>Adjoints\<close>
    4.17  
    4.18 -definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    4.19 +definition%important adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
    4.20 +"adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    4.21  
    4.22  lemma adjoint_unique:
    4.23    assumes "\<forall>x y. inner (f x) y = inner x (g y)"