Verified_Numerical_Methods/Vector_Scale.thy at main · isabelle-utp/Verified_Numerical_Methods · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
theory Vector_Scale
  imports "ITree_Numeric_VCG.ITree_Numeric_VCG"
begin

definition vec_lookup :: "'a vec['n::nat] \<Rightarrow> nat \<Rightarrow> 'a" (infixl \<open>!\<^sub>v\<close> 100) where
"vec_lookup v i = vec_list v ! i"

definition vec_update :: "'a::zero vec['n::nat] \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a vec['n::nat]" where
"vec_update v i x = Vec (list_update (vec_list v) i x)"

lemma vec_lookup_update [simp]:
  "i < CARD('n::nat) \<Longrightarrow> vec_lookup (vec_update (v :: ('a::zero) vec['n::nat]) j x) i = (if i = j then x else vec_lookup v i)"
  by (auto simp add: vec_lookup_def vec_update_def nth_ezlist)

definition vec_collection_lens :: "nat \<Rightarrow> 'a::zero \<Longrightarrow> 'a vec['n::nat]" where
[lens_defs]: "vec_collection_lens i = \<lparr> lens_get = (\<lambda> v. vec_lookup v i), lens_put = (\<lambda> s v. vec_update s i v) \<rparr>"

lemma vec_collection_lens_vwb [simp]:
  assumes "i < CARD('n::nat)"
  shows "vwb_lens (vec_collection_lens i :: 'a::zero \<Longrightarrow> 'a vec['n::nat])"
  using assms
  apply (unfold_locales)
  apply (simp_all add: vec_collection_lens_def vec_lookup_def vec_update_def)
  apply (metis length_list_update length_vec_list nth_ezlist nth_list_update_eq)
  apply (simp add: Vec_eq_iff nth_ezlist)
  done

adhoc_overloading collection_lens \<rightleftharpoons> vec_collection_lens

lemma nth_vec_list: "i < CARD('n::nat) \<Longrightarrow> (vec_list (xs :: 'a vec['n::nat])) ! i = xs $ of_nat' i"
  by (simp add: vec_list_def)

alphabet 'i st =
  i :: nat
  vc :: "real vec['i]"

instantiation st_ext :: (finite,default) default
begin
definition default_st_ext :: "('a, 'b) st_ext" where
"default_st_ext = \<lparr> i\<^sub>v = 0, vc\<^sub>v = 0, \<dots> = default \<rparr>"

instance ..

end

declare [[coercion vec_lookup]]

program vec_scale "(n :: real, X :: real vec['n::nat])" over "'n::nat st" =
  "vc := X;
   i := 0;
   while i < CARD('n) do
     vc[i] := n * X i;
     i := i + 1
   od"

program vec_scale_annotated "(n :: real, X :: real vec['n::nat])" over "'n::nat st" =
  "vc := X;
   i := 0;
   while i < CARD('n)
   invariant i \<le> CARD('n) \<and> (\<forall> k<i. vc k = n * X k)
   variant CARD('n) - i
   do
     vc[i] := n * X i;
     i := i + 1
   od"

lemma vec_scale_correct: "H[True] vec_scale_annotated(n, X) [vc = n *\<^sub>R X]"
  apply vcg
  apply (metis Vec_lookup_list nat_of_less_CARD real_scaleR_def vec_eq_iff vec_lookup_def
      vector_scaleR_component)
  done

end