lib/isabelle/Why3_List.thy

   1 theory Why3_List
   2 imports Why3_Setup
   3 begin
   4
   5 section \<open> Length of a list \<close>
   6
   7 why3_open "list/Length.xml"
   8
   9 why3_vc lengthqtdef by (cases l) simp_all
  10
  11 why3_vc Length_nil by simp
  12
  13 why3_vc Length_nonnegative by simp
  14
  15 why3_end
  16
  17
  18 section \<open> Membership in a list \<close>
  19
  20 why3_open "list/Mem.xml"
  21
  22 why3_vc memqtdef by (simp split: list.split)
  23
  24 why3_end
  25
  26
  27 section \<open> Nth element of a list \<close>
  28
  29 why3_open "list/Nth.xml"
  30
  31 lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> nth i xs = Some (xs ! nat i)"
  32   by (induct xs arbitrary: i) (auto simp add: nat_diff_distrib)
  33
  34 why3_vc is_noneqtspec
  35   by (simp add: is_none_def split: option.split)
  36
  37 why3_end
  38
  39
  40 why3_open "list/NthNoOpt.xml"
  41
  42 why3_vc nth_cons_0 by simp
  43
  44 why3_vc nth_cons_n
  45   using assms
  46   by (simp add: nat_diff_distrib)
  47
  48 why3_end
  49
  50
  51 why3_open "list/NthLength.xml"
  52
  53 why3_vc nth_none_1
  54   using assms
  55   by (induct l arbitrary: i) simp_all
  56
  57 why3_vc nth_none_2
  58   using assms
  59   by (induct l arbitrary: i) simp_all
  60
  61 why3_vc nth_none_3
  62   using assms
  63 proof (induct l arbitrary: i)
  64   case Nil
  65   then show ?case by simp arith
  66 next
  67   case (Cons x xs)
  68   show ?case
  69   proof (cases "i < 0")
  70     case False
  71     with Cons have "0 < i" by (simp split: if_split_asm)
  72     with Cons have "Nth.nth (i - 1) xs = None" by simp
  73     then have "i - 1 < 0 \<or> int (length xs) \<le> i - 1"
  74       by (rule Cons)
  75     with `0 < i` show ?thesis by auto
  76   qed simp
  77 qed
  78
  79 why3_vc is_noneqtspec
  80   by (simp add: is_none_def split: option.split)
  81
  82 why3_end
  83
  84
  85 section \<open> Head and tail \<close>
  86
  87 why3_open "list/HdTl.xml"
  88
  89 why3_vc is_noneqtspec
  90   by (simp add: is_none_def split: option.split)
  91
  92 why3_end
  93
  94
  95 why3_open "list/HdTlNoOpt.xml"
  96
  97 why3_vc hd_cons by simp
  98
  99 why3_vc tl_cons by simp
 100
 101 why3_end
 102
 103
 104 section \<open> Relation between head, tail, and nth \<close>
 105
 106 why3_open "list/NthHdTl.xml"
 107
 108 why3_vc Nth_tl
 109   using assms
 110   by (simp add: tl_def split: list.split_asm)
 111
 112 why3_vc Nth0_head
 113   by (simp add: hd_def split: list.split)
 114
 115 why3_vc is_noneqtspec
 116   by (simp add: is_none_def split: option.split)
 117
 118 why3_end
 119
 120
 121 section \<open> Appending two lists \<close>
 122
 123 why3_open "list/Append.xml"
 124
 125 why3_vc infix_plplqtdef by (simp split: list.split)
 126
 127 why3_vc Append_assoc by simp
 128
 129 why3_vc Append_l_nil by simp
 130
 131 why3_vc Append_length by simp
 132
 133 why3_vc mem_append by simp
 134
 135 why3_vc mem_decomp
 136   using assms
 137   by (simp add: in_set_conv_decomp)
 138
 139 why3_end
 140
 141
 142 why3_open "list/NthLengthAppend.xml"
 143
 144 why3_vc nth_append_1
 145 proof (cases "0 \<le> i")
 146   case True
 147   with assms have "nat i < length l1" by simp
 148   with True show ?thesis
 149     by (simp add: nth_eq nth_append)
 150 next
 151   case False
 152   then show ?thesis by (simp add: nth_none_1)
 153 qed
 154
 155 why3_vc nth_append_2
 156 proof (cases "nat i < length (l1 @ l2)")
 157   case True
 158   with assms show ?thesis
 159     by (auto simp add: nth_eq nth_append nat_diff_distrib)
 160 next
 161   case False
 162   with assms show ?thesis by (simp add: nth_none_2)
 163 qed
 164
 165 why3_vc is_noneqtspec
 166   by (simp add: is_none_def split: option.split)
 167
 168 why3_end
 169
 170
 171 section \<open> Reversing a list \<close>
 172
 173 why3_open "list/Reverse.xml"
 174
 175 why3_vc reverseqtdef by (simp split: list.split)
 176
 177 why3_vc Reverse_length by simp
 178
 179 why3_vc reverse_append by simp
 180
 181 why3_vc reverse_reverse by simp
 182
 183 why3_vc reverse_mem by simp
 184
 185 why3_vc reverse_cons by simp
 186
 187 why3_vc cons_reverse by simp
 188
 189 why3_end
 190
 191
 192 section \<open> Reverse append \<close>
 193
 194 why3_open "list/RevAppend.xml"
 195
 196 why3_vc rev_append_append_l
 197   by (induct r arbitrary: t) simp_all
 198
 199 why3_vc rev_append_append_r
 200 proof (induct s arbitrary: r)
 201   case (Cons x xs)
 202   show ?case by (simp add: Cons [symmetric])
 203 qed simp
 204
 205 why3_vc rev_append_length
 206   by (induct s arbitrary: t) simp_all
 207
 208 why3_vc rev_append_def
 209   by (induct r arbitrary: s) simp_all
 210
 211 why3_end
 212
 213
 214 section \<open> Zip \<close>
 215
 216 why3_open "list/Combine.xml"
 217
 218 why3_end
 219
 220
 221 section \<open> List with pairwise distinct elements \<close>
 222
 223 why3_open "list/Distinct.xml"
 224
 225 why3_vc distinct_zero by simp
 226
 227 why3_vc distinct_one by simp
 228
 229 why3_vc distinct_many using assms by simp
 230
 231 why3_vc distinct_append using assms by auto
 232
 233 why3_end
 234
 235
 236 section \<open> Number of occurrences in a list \<close>
 237
 238 why3_open "list/NumOcc.xml"
 239
 240 why3_vc Num_Occ_NonNeg
 241   by (induct l) simp_all
 242
 243 why3_vc Mem_Num_Occ
 244 proof (induct l)
 245   case (Cons y ys)
 246   from Num_Occ_NonNeg [of y ys]
 247   have "0 < 1 + num_occ y ys" by simp
 248   with Cons show ?case by simp
 249 qed simp
 250
 251 why3_vc Append_Num_Occ
 252   by (induct l1) simp_all
 253
 254 why3_vc reverse_num_occ
 255   by (induct l) (simp_all add: Append_Num_Occ)
 256
 257 why3_end
 258
 259
 260 section \<open> Permutation of lists \<close>
 261
 262 why3_open "list/Permut.xml"
 263
 264 why3_vc Permut_refl by (simp add: permut_def)
 265
 266 why3_vc Permut_sym using assms by (simp add: permut_def)
 267
 268 why3_vc Permut_trans using assms by (simp add: permut_def)
 269
 270 why3_vc Permut_cons using assms by (simp add: permut_def)
 271
 272 why3_vc Permut_swap by (simp add: permut_def)
 273
 274 why3_vc Permut_cons_append by (simp add: permut_def Append_Num_Occ)
 275
 276 why3_vc Permut_assoc by (simp add: permut_def)
 277
 278 why3_vc Permut_append using assms by (simp add: permut_def Append_Num_Occ)
 279
 280 why3_vc Permut_append_swap by (simp add: permut_def Append_Num_Occ)
 281
 282 why3_vc Permut_mem using assms by (simp add: permut_def Mem_Num_Occ)
 283
 284 why3_vc Permut_length
 285   using assms
 286 proof (induct l1 arbitrary: l2)
 287   case Nil
 288   then show ?case
 289   proof (cases l2)
 290     case (Cons x xs)
 291     with Nil Num_Occ_NonNeg [of x xs]
 292     show ?thesis by (auto simp add: permut_def dest: spec [of _ x])
 293   qed simp
 294 next
 295   case (Cons x xs)
 296   from `permut (x # xs) l2` have "x \<in> set l2"
 297     by (rule Permut_mem) simp
 298   then obtain ys zs where "l2 = ys @ x # zs"
 299     by (auto simp add: in_set_conv_decomp)
 300   with Cons have "permut (x # xs) (ys @ x # zs)" by simp
 301   moreover have "permut (ys @ x # zs) ((x # zs) @ ys)"
 302     by (rule Permut_append_swap)
 303   ultimately have "permut (x # xs) ((x # zs) @ ys)"
 304     by (rule Permut_trans)
 305   then have "permut xs (zs @ ys)" by (simp add: permut_def)
 306   then have "int (length xs) = int (length (zs @ ys))" by (rule Cons)
 307   with `l2 = ys @ x # zs` show ?case by simp
 308 qed
 309
 310 why3_end
 311
 312 end