Commit c6c3b3d6 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

typage des predicats inductifs

parent a21ff839
(* graph theory *)
theory Path
use import prelude.List
type vertex
logic edge(vertex, vertex)
inductive simple_path(vertex, vertex list, vertex) =
| Path_empty :
forall v:vertex. simple_path(v, Nil : vertex list, v)
| Path_cons :
forall src, v, dst : vertex. forall l : vertex list.
simple_path(v, l, dst) -> edge(src, v) -> not mem(v, l) ->
simple_path(src, Cons(v, l), dst)
end
......@@ -70,6 +70,11 @@ theory List
logic is_nil(x : 'a list) = x = Nil
logic mem(x: 'a, l : 'a list) = match l with
| Nil -> false
| Cons(y, r) -> x = y or mem(x, r)
end
end
theory Array
......
(* test file *)
theory T
use prelude.List
use graph.Path
end
theory A
type t
namespace S
......@@ -24,6 +29,8 @@ theory Test
| Even_nil : even_length(Nil : int list)
| Even_cons: forall x,y:'a, l:'a list.
even_length(l) -> even_length(Cons(x,Cons(y,l)))
lemma Ax : even_length(Cons(1,Cons(2,Nil)))
end
theory TestPrelude
......
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