mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
313 lines
5.9 KiB
Plaintext
313 lines
5.9 KiB
Plaintext
theory Why3_List
|
|
imports Why3_Setup
|
|
begin
|
|
|
|
section \<open> Length of a list \<close>
|
|
|
|
why3_open "list/Length.xml"
|
|
|
|
why3_vc lengthqtdef by (cases l) simp_all
|
|
|
|
why3_vc Length_nil by simp
|
|
|
|
why3_vc Length_nonnegative by simp
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Membership in a list \<close>
|
|
|
|
why3_open "list/Mem.xml"
|
|
|
|
why3_vc memqtdef by (simp split: list.split)
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Nth element of a list \<close>
|
|
|
|
why3_open "list/Nth.xml"
|
|
|
|
lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> nth i xs = Some (xs ! nat i)"
|
|
by (induct xs arbitrary: i) (auto simp add: nat_diff_distrib)
|
|
|
|
why3_vc is_noneqtspec
|
|
by (simp add: is_none_def split: option.split)
|
|
|
|
why3_end
|
|
|
|
|
|
why3_open "list/NthNoOpt.xml"
|
|
|
|
why3_vc nth_cons_0 by simp
|
|
|
|
why3_vc nth_cons_n
|
|
using assms
|
|
by (simp add: nat_diff_distrib)
|
|
|
|
why3_end
|
|
|
|
|
|
why3_open "list/NthLength.xml"
|
|
|
|
why3_vc nth_none_1
|
|
using assms
|
|
by (induct l arbitrary: i) simp_all
|
|
|
|
why3_vc nth_none_2
|
|
using assms
|
|
by (induct l arbitrary: i) simp_all
|
|
|
|
why3_vc nth_none_3
|
|
using assms
|
|
proof (induct l arbitrary: i)
|
|
case Nil
|
|
then show ?case by simp arith
|
|
next
|
|
case (Cons x xs)
|
|
show ?case
|
|
proof (cases "i < 0")
|
|
case False
|
|
with Cons have "0 < i" by (simp split: if_split_asm)
|
|
with Cons have "Nth.nth (i - 1) xs = None" by simp
|
|
then have "i - 1 < 0 \<or> int (length xs) \<le> i - 1"
|
|
by (rule Cons)
|
|
with `0 < i` show ?thesis by auto
|
|
qed simp
|
|
qed
|
|
|
|
why3_vc is_noneqtspec
|
|
by (simp add: is_none_def split: option.split)
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Head and tail \<close>
|
|
|
|
why3_open "list/HdTl.xml"
|
|
|
|
why3_vc is_noneqtspec
|
|
by (simp add: is_none_def split: option.split)
|
|
|
|
why3_end
|
|
|
|
|
|
why3_open "list/HdTlNoOpt.xml"
|
|
|
|
why3_vc hd_cons by simp
|
|
|
|
why3_vc tl_cons by simp
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Relation between head, tail, and nth \<close>
|
|
|
|
why3_open "list/NthHdTl.xml"
|
|
|
|
why3_vc Nth_tl
|
|
using assms
|
|
by (simp add: tl_def split: list.split_asm)
|
|
|
|
why3_vc Nth0_head
|
|
by (simp add: hd_def split: list.split)
|
|
|
|
why3_vc is_noneqtspec
|
|
by (simp add: is_none_def split: option.split)
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Appending two lists \<close>
|
|
|
|
why3_open "list/Append.xml"
|
|
|
|
why3_vc infix_plplqtdef by (simp split: list.split)
|
|
|
|
why3_vc Append_assoc by simp
|
|
|
|
why3_vc Append_l_nil by simp
|
|
|
|
why3_vc Append_length by simp
|
|
|
|
why3_vc mem_append by simp
|
|
|
|
why3_vc mem_decomp
|
|
using assms
|
|
by (simp add: in_set_conv_decomp)
|
|
|
|
why3_end
|
|
|
|
|
|
why3_open "list/NthLengthAppend.xml"
|
|
|
|
why3_vc nth_append_1
|
|
proof (cases "0 \<le> i")
|
|
case True
|
|
with assms have "nat i < length l1" by simp
|
|
with True show ?thesis
|
|
by (simp add: nth_eq nth_append)
|
|
next
|
|
case False
|
|
then show ?thesis by (simp add: nth_none_1)
|
|
qed
|
|
|
|
why3_vc nth_append_2
|
|
proof (cases "nat i < length (l1 @ l2)")
|
|
case True
|
|
with assms show ?thesis
|
|
by (auto simp add: nth_eq nth_append nat_diff_distrib)
|
|
next
|
|
case False
|
|
with assms show ?thesis by (simp add: nth_none_2)
|
|
qed
|
|
|
|
why3_vc is_noneqtspec
|
|
by (simp add: is_none_def split: option.split)
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Reversing a list \<close>
|
|
|
|
why3_open "list/Reverse.xml"
|
|
|
|
why3_vc reverseqtdef by (simp split: list.split)
|
|
|
|
why3_vc Reverse_length by simp
|
|
|
|
why3_vc reverse_append by simp
|
|
|
|
why3_vc reverse_reverse by simp
|
|
|
|
why3_vc reverse_mem by simp
|
|
|
|
why3_vc reverse_cons by simp
|
|
|
|
why3_vc cons_reverse by simp
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Reverse append \<close>
|
|
|
|
why3_open "list/RevAppend.xml"
|
|
|
|
why3_vc rev_append_append_l
|
|
by (induct r arbitrary: t) simp_all
|
|
|
|
why3_vc rev_append_append_r
|
|
proof (induct s arbitrary: r)
|
|
case (Cons x xs)
|
|
show ?case by (simp add: Cons [symmetric])
|
|
qed simp
|
|
|
|
why3_vc rev_append_length
|
|
by (induct s arbitrary: t) simp_all
|
|
|
|
why3_vc rev_append_def
|
|
by (induct r arbitrary: s) simp_all
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Zip \<close>
|
|
|
|
why3_open "list/Combine.xml"
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> List with pairwise distinct elements \<close>
|
|
|
|
why3_open "list/Distinct.xml"
|
|
|
|
why3_vc distinct_zero by simp
|
|
|
|
why3_vc distinct_one by simp
|
|
|
|
why3_vc distinct_many using assms by simp
|
|
|
|
why3_vc distinct_append using assms by auto
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Number of occurrences in a list \<close>
|
|
|
|
why3_open "list/NumOcc.xml"
|
|
|
|
why3_vc Num_Occ_NonNeg
|
|
by (induct l) simp_all
|
|
|
|
why3_vc Mem_Num_Occ
|
|
proof (induct l)
|
|
case (Cons y ys)
|
|
from Num_Occ_NonNeg [of y ys]
|
|
have "0 < 1 + num_occ y ys" by simp
|
|
with Cons show ?case by simp
|
|
qed simp
|
|
|
|
why3_vc Append_Num_Occ
|
|
by (induct l1) simp_all
|
|
|
|
why3_vc reverse_num_occ
|
|
by (induct l) (simp_all add: Append_Num_Occ)
|
|
|
|
why3_end
|
|
|
|
|
|
section \<open> Permutation of lists \<close>
|
|
|
|
why3_open "list/Permut.xml"
|
|
|
|
why3_vc Permut_refl by (simp add: permut_def)
|
|
|
|
why3_vc Permut_sym using assms by (simp add: permut_def)
|
|
|
|
why3_vc Permut_trans using assms by (simp add: permut_def)
|
|
|
|
why3_vc Permut_cons using assms by (simp add: permut_def)
|
|
|
|
why3_vc Permut_swap by (simp add: permut_def)
|
|
|
|
why3_vc Permut_cons_append by (simp add: permut_def Append_Num_Occ)
|
|
|
|
why3_vc Permut_assoc by (simp add: permut_def)
|
|
|
|
why3_vc Permut_append using assms by (simp add: permut_def Append_Num_Occ)
|
|
|
|
why3_vc Permut_append_swap by (simp add: permut_def Append_Num_Occ)
|
|
|
|
why3_vc Permut_mem using assms by (simp add: permut_def Mem_Num_Occ)
|
|
|
|
why3_vc Permut_length
|
|
using assms
|
|
proof (induct l1 arbitrary: l2)
|
|
case Nil
|
|
then show ?case
|
|
proof (cases l2)
|
|
case (Cons x xs)
|
|
with Nil Num_Occ_NonNeg [of x xs]
|
|
show ?thesis by (auto simp add: permut_def dest: spec [of _ x])
|
|
qed simp
|
|
next
|
|
case (Cons x xs)
|
|
from `permut (x # xs) l2` have "x \<in> set l2"
|
|
by (rule Permut_mem) simp
|
|
then obtain ys zs where "l2 = ys @ x # zs"
|
|
by (auto simp add: in_set_conv_decomp)
|
|
with Cons have "permut (x # xs) (ys @ x # zs)" by simp
|
|
moreover have "permut (ys @ x # zs) ((x # zs) @ ys)"
|
|
by (rule Permut_append_swap)
|
|
ultimately have "permut (x # xs) ((x # zs) @ ys)"
|
|
by (rule Permut_trans)
|
|
then have "permut xs (zs @ ys)" by (simp add: permut_def)
|
|
then have "int (length xs) = int (length (zs @ ys))" by (rule Cons)
|
|
with `l2 = ys @ x # zs` show ?case by simp
|
|
qed
|
|
|
|
why3_end
|
|
|
|
end
|