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