Commit 70b9f3f6 authored by Stefan Berghofer's avatar Stefan Berghofer

Realize more of the list theories in Isabelle

parent f26a0859
......@@ -1104,7 +1104,7 @@ ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/set/, $(ISABELLELI
ISABELLELIBS_MAP_FILES = Map Occ MapPermut MapInjection
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELIBS_MAP_FILES)))
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/list/, $(ISABELLELIBS_LIST_FILES)))
drivers/isabelle-realizations.aux: Makefile
......
......@@ -110,6 +110,15 @@ theory list.NthNoOpt
syntax function nth "<app><const name=\"List.nth\"/>%2<app><const name=\"Int.nat\"/>%1</app></app>"
end
theory list.HdTlNoOpt
syntax function hd "<app><const name=\"List.hd\"/>%1</app>"
syntax function tl "<app><const name=\"List.tl\"/>%1</app>"
end
theory list.Distinct
syntax predicate distinct "<app><const name=\"List.distinct\"/>%1</app>"
end
theory option.Option
syntax type option "<type name=\"Option.option\">%1</type>"
......
......@@ -83,6 +83,15 @@ why3_open "list/HdTl.xml"
why3_end
why3_open "list/HdTlNoOpt.xml"
why3_vc hd_cons by simp
why3_vc tl_cons by simp
why3_end
section {* Relation between head, tail, and nth *}
why3_open "list/NthHdTl.xml"
......@@ -158,4 +167,119 @@ why3_vc reverse_reverse by simp
why3_end
section {* Reverse append *}
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_end
section {* Zip *}
why3_open "list/Combine.xml"
why3_end
section {* List with pairwise distinct elements *}
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 {* Number of occurrences in a list *}
why3_open "list/NumOcc.xml"
lemma num_occ_nonneg: "0 \<le> num_occ x xs"
by (induct xs) 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_end
section {* Permutation of lists *}
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
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment