mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
55 lines
1.2 KiB
Plaintext
55 lines
1.2 KiB
Plaintext
theory Order
|
|
type t
|
|
predicate (<=) t t
|
|
|
|
axiom le_refl : forall x : t. x <= x
|
|
axiom le_asym : forall x y : t. x <= y -> y <= x -> x = y
|
|
axiom le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
|
|
end
|
|
|
|
theory List
|
|
type list 'a = Nil | Cons 'a (list 'a)
|
|
|
|
predicate mem (x: 'a) (l: list 'a) = match l with
|
|
| Nil -> false
|
|
| Cons y r -> x = y \/ mem x r
|
|
end
|
|
|
|
end
|
|
|
|
theory SortedList
|
|
use List
|
|
clone import Order as O with axiom .
|
|
|
|
inductive sorted (l : list t) =
|
|
| sorted_nil :
|
|
sorted Nil
|
|
| sorted_one :
|
|
forall x:t. sorted (Cons x Nil)
|
|
| sorted_two :
|
|
forall x y : t, l : list t.
|
|
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
|
|
|
|
lemma sorted_inf:
|
|
forall x y: t, l: list t. x <= y -> sorted (Cons y l) ->
|
|
sorted (Cons x l)
|
|
|
|
|
|
lemma sorted_mem:
|
|
forall x: t, l: list t. sorted (Cons x l) ->
|
|
forall y: t. mem y l -> x <= y
|
|
(* by induction on l *)
|
|
|
|
end
|
|
|
|
theory SortedIntList
|
|
use int.Int
|
|
use List
|
|
clone SortedList with
|
|
type O.t = int, predicate O.(<=) = (<=),
|
|
lemma O.le_refl, lemma O.le_asym, lemma O.le_trans
|
|
|
|
goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil)))
|
|
end
|
|
|