equal
deleted
inserted
replaced
1913 lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))" |
1913 lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))" |
1914 by (auto simp add: norm_real dist_norm) |
1914 by (auto simp add: norm_real dist_norm) |
1915 |
1915 |
1916 subsection{* Explicit vector construction from lists. *} |
1916 subsection{* Explicit vector construction from lists. *} |
1917 |
1917 |
1918 primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}" |
1918 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)" |
1919 where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n" |
|
1920 |
|
1921 lemma from_nat [simp]: "from_nat = of_nat" |
|
1922 by (rule ext, induct_tac x, simp_all) |
|
1923 |
|
1924 primrec |
|
1925 list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _" |
|
1926 where |
|
1927 "list_fun n [] = (\<lambda>x. 0)" |
|
1928 | "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x" |
|
1929 |
|
1930 definition "vector l = (\<chi> i. list_fun 1 l i)" |
|
1931 (*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*) |
|
1932 |
1919 |
1933 lemma vector_1: "(vector[x]) $1 = x" |
1920 lemma vector_1: "(vector[x]) $1 = x" |
1934 unfolding vector_def by simp |
1921 unfolding vector_def by simp |
1935 |
1922 |
1936 lemma vector_2: |
1923 lemma vector_2: |