From d472a8c49258253f0d6611a3fc799f10f859aa76 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Thu, 11 Apr 2013 16:36:12 +0200 Subject: [PATCH] partially revert the previous commit --- theories/list.why | 62 ++++++++++++++++++++--------------------------- 1 file changed, 26 insertions(+), 36 deletions(-) diff --git a/theories/list.why b/theories/list.why index 31853c809..1a3bc4530 100644 --- a/theories/list.why +++ b/theories/list.why @@ -176,6 +176,32 @@ theory NthLengthAppend end +(** {2 Reversing a list} *) + +theory Reverse + + use export List + use import Append + + function reverse (l: list 'a) : list 'a = match l with + | Nil -> Nil + | Cons x r -> reverse r ++ Cons x Nil + end + + lemma reverse_append: + forall l1 l2: list 'a, x: 'a. + (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2) + + lemma reverse_reverse: + forall l: list 'a. reverse (reverse l) = l + + use import Length + + lemma Reverse_length: + forall l: list 'a. length (reverse l) = length l + +end + (** {2 Reverse append} *) theory RevAppend @@ -207,42 +233,6 @@ theory RevAppend end -(** {2 Reversing a list} *) - -theory Reverse - - use export List - use import Append - use import RevAppend - - function reverse (l: list 'a) : list 'a = rev_append l Nil - - lemma rev_append_def: - forall l1 l2: list 'a. - rev_append l1 l2 = reverse l1 ++ l2 - - lemma reverse_cons: - forall x: 'a, r: list 'a. - reverse (Cons x r) = reverse r ++ Cons x Nil - - lemma reverse_append: - forall l1 l2: list 'a. - reverse (l1 ++ l2) = (reverse l2) ++ (reverse l1) - - lemma reverse_cons_append: - forall l1 l2: list 'a, x: 'a. - (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2) - - lemma reverse_reverse: - forall l: list 'a. reverse (reverse l) = l - - use import Length - - lemma Reverse_length: - forall l: list 'a. length (reverse l) = length l - -end - (** {2 Sorted lists for some order as parameter} *) theory Sorted -- 2.24.1