1theory Complex_Types
2imports "HOL-SPARK.SPARK"
3begin
4
5datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
6
7record two_fields =
8  Field1 :: "int \<times> day \<Rightarrow> int"
9  Field2 :: int
10
11spark_types
12  complex_types__day = day
13  complex_types__record_type = two_fields
14
15definition
16  initialized3 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
17  "initialized3 A i k = (\<forall>j\<in>{0..<k}. A (i, val j) = 0)"
18
19definition
20  initialized2 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> bool" where
21  "initialized2 A i = (\<forall>j\<in>{0..<i}. initialized3 A j 7)"
22
23definition
24  initialized :: "(int \<Rightarrow> two_fields) \<Rightarrow> int \<Rightarrow> bool" where
25  "initialized A i = (\<forall>j\<in>{0..<i}.
26     initialized2 (Field1 (A j)) 10 \<and> Field2 (A j) = 0)"
27
28spark_proof_functions
29  complex_types__initialized = initialized
30  complex_types__initialized2 = initialized2
31  complex_types__initialized3 = initialized3
32
33(*<*)
34spark_open \<open>complex_types_app/initialize\<close>
35
36spark_vc procedure_initialize_1
37  by (simp add: initialized_def)
38
39spark_vc procedure_initialize_2
40proof -
41  from
42    \<open>initialized a loop__1__i\<close>
43    \<open>initialized2 (Field1 (a loop__1__i)) 9\<close>
44    \<open>initialized3 (Field1 (a loop__1__i)) 9 (pos Sun)\<close>
45  show ?C1
46    apply (auto simp add: initialized_def initialized2_def initialized3_def)
47    apply (case_tac "j = 9")
48    apply auto
49    apply (case_tac "ja = 6")
50    apply auto
51    done
52  from H5
53  show ?C2 by simp
54qed
55
56spark_vc procedure_initialize_3
57  by (simp add: initialized2_def)
58
59spark_vc procedure_initialize_4
60proof -
61  from \<open>initialized a loop__1__i\<close>
62  show ?C1 by (simp add: initialized_def)
63  from
64    \<open>initialized2 (Field1 (a loop__1__i)) loop__2__j\<close>
65    \<open>initialized3 (Field1 (a loop__1__i)) loop__2__j (pos Sun)\<close>
66  show ?C2
67    apply (auto simp add: initialized2_def initialized3_def)
68    apply (case_tac "j = loop__2__j")
69    apply auto
70    apply (case_tac "ja = 6")
71    apply auto
72    done
73  from H5
74  show ?C3 by simp
75qed
76
77spark_vc procedure_initialize_5
78  by (simp add: initialized3_def)
79
80spark_vc procedure_initialize_6
81proof -
82  from \<open>initialized a loop__1__i\<close>
83  show ?C1 by (simp add: initialized_def)
84  from \<open>initialized2 (Field1 (a loop__1__i)) loop__2__j\<close>
85  show ?C2 by (simp add: initialized2_def initialized3_def)
86  from
87    \<open>initialized3 (Field1 (a loop__1__i)) loop__2__j (pos loop__3__k)\<close>
88    \<open>loop__3__k < Sun\<close>
89    rangeI [of pos loop__3__k]
90  show ?C3
91    apply (auto simp add: initialized3_def succ_def less_pos pos_val range_pos)
92    apply (case_tac "j = pos loop__3__k")
93    apply (auto simp add: val_pos)
94    done
95  from H5
96  show ?C4 by simp
97qed
98
99spark_vc procedure_initialize_9
100  using
101    \<open>initialized a 9\<close>
102    \<open>initialized2 (Field1 (a 9)) 9\<close>
103    \<open>initialized3 (Field1 (a 9)) 9 (pos Sun)\<close>
104  apply (auto simp add: initialized_def initialized2_def initialized3_def)
105  apply (case_tac "j = 9")
106  apply auto
107  apply (case_tac "ja = 6")
108  apply auto
109  done
110
111spark_end
112(*>*)
113
114end
115