moved rev_append to theories

parent 6798a8f2
......@@ -58,80 +58,6 @@ module Hanoi
end
theory ListRevAppend
use import list.List
use import list.Append
function rev_append (s t: list 'a) : list 'a =
match s with
| Cons x r -> rev_append r (Cons x t)
| Nil -> t
end
lemma rev_append_append_l:
forall r s t: list 'a.
rev_append (r ++ s) t = rev_append s (rev_append r t)
lemma rev_append_append_r:
forall r s t: list 'a.
rev_append r (s ++ t) = rev_append (rev_append s r) t
use import int.Int
use import list.Length
lemma rev_append_length:
forall s t: list 'a.
length (rev_append s t) = length s + length t
(*
use import list.Reverse
lemma rev_append_rev:
forall s: list 'a. reverse s = rev_append s Nil
*)
end
theory ListRevSorted
type t
predicate le t t
predicate ge (x y: t) = le y x
use import list.List
clone list.Sorted as Incr with type t = t, predicate le = le
clone list.Sorted as Decr with type t = t, predicate le = ge
predicate compat (s t: list t) =
match s, t with
| Cons x _, Cons y _ -> le x y
| _, _ -> true
end
use import ListRevAppend
lemma rev_append_sorted_incr:
forall s t: list t.
Incr.sorted (rev_append s t) <->
Decr.sorted s /\ Incr.sorted t /\ compat s t
lemma rev_append_sorted_decr:
forall s t: list t.
Decr.sorted (rev_append s t) <->
Incr.sorted s /\ Decr.sorted t /\ compat t s
(*
use import list.Reverse
lemma rev_sorted_incr:
forall s: list t. Incr.sorted (reverse s) <-> Decr.sorted s
lemma rev_sorted_decr:
forall s: list t. Decr.sorted (reverse s) <-> Incr.sorted s
*)
end
module Tower_of_Hanoi
(* a generalized version where the disks are arbitrary integers *)
......@@ -139,8 +65,8 @@ module Tower_of_Hanoi
use import list.List
use import list.Length
use import ListRevAppend
clone import ListRevSorted with type t = int, predicate le = (<)
use import list.RevAppend
clone import list.RevSorted with type t = int, predicate le = (<)
type tower = {
mutable rod : list int;
......
......@@ -176,19 +176,60 @@ theory NthLengthAppend
end
(** {2 Reverse append} *)
theory RevAppend
use import List
function rev_append (s t: list 'a) : list 'a =
match s with
| Cons x r -> rev_append r (Cons x t)
| Nil -> t
end
use import Append
lemma rev_append_append_l:
forall r s t: list 'a.
rev_append (r ++ s) t = rev_append s (rev_append r t)
lemma rev_append_append_r:
forall r s t: list 'a.
rev_append r (s ++ t) = rev_append (rev_append s r) t
use import int.Int
use import Length
lemma rev_append_length:
forall s t: list 'a.
length (rev_append s t) = length s + length t
end
(** {2 Reversing a list} *)
theory Reverse
use export List
use import Append
use import RevAppend
function reverse (l: list 'a) : list 'a = match l with
| Nil -> Nil
| Cons x r -> reverse r ++ Cons x Nil
end
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)
......@@ -237,6 +278,46 @@ theory SortedInt
end
theory RevSorted
type t
predicate le t t
predicate ge (x y: t) = le y x
use import List
clone Sorted as Incr with type t = t, predicate le = le
clone Sorted as Decr with type t = t, predicate le = ge
predicate compat (s t: list t) =
match s, t with
| Cons x _, Cons y _ -> le x y
| _, _ -> true
end
use import RevAppend
lemma rev_append_sorted_incr:
forall s t: list t.
Incr.sorted (rev_append s t) <->
Decr.sorted s /\ Incr.sorted t /\ compat s t
lemma rev_append_sorted_decr:
forall s t: list t.
Decr.sorted (rev_append s t) <->
Incr.sorted s /\ Decr.sorted t /\ compat t s
(*
use import Reverse
lemma rev_sorted_incr:
forall s: list t. Incr.sorted (reverse s) <-> Decr.sorted s
lemma rev_sorted_decr:
forall s: list t. Decr.sorted (reverse s) <-> Incr.sorted s
*)
end
(** {2 Number of occurrences in a list} *)
theory NumOcc
......
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