equal
deleted
inserted
replaced
21 assumes inner_Basis: |
21 assumes inner_Basis: |
22 "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)" |
22 "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)" |
23 assumes euclidean_all_zero_iff: |
23 assumes euclidean_all_zero_iff: |
24 "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)" |
24 "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)" |
25 |
25 |
26 abbreviation dimension :: "('a::euclidean_space) itself \<Rightarrow> nat" where |
26 syntax "_type_dimension" :: "type \<Rightarrow> nat" ("(1DIM/(1'(_')))") |
27 "dimension TYPE('a) \<equiv> card (Basis :: 'a set)" |
27 translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)" |
28 |
28 typed_print_translation \<open> |
29 syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))") |
29 [(@{const_syntax card}, |
30 |
30 fn ctxt => fn _ => fn [Const (@{const_syntax Basis}, Type (@{type_name set}, [T]))] => |
31 translations "DIM('t)" == "CONST dimension (TYPE('t))" |
31 Syntax.const @{syntax_const "_type_dimension"} $ Syntax_Phases.term_of_typ ctxt T)] |
|
32 \<close> |
32 |
33 |
33 lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1" |
34 lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1" |
34 unfolding norm_eq_sqrt_inner by (simp add: inner_Basis) |
35 unfolding norm_eq_sqrt_inner by (simp add: inner_Basis) |
35 |
36 |
36 lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1" |
37 lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1" |