new theories graph.Path and int.IntInf

parent 4cf882ea
(* graph theory *)
(* Graph theory *)
theory Path
type graph
use export list.List
use export list.Append
type vertex
predicate edge graph vertex vertex
predicate edge vertex vertex
inductive path graph vertex vertex =
| Path_empty :
forall g : graph, v : vertex. path g v v
| Path_append:
forall g : graph, v1 v2 src dst : vertex.
path g src v1 -> edge g v1 v2 -> path g v2 dst ->
path g src dst
(* path v0 [v0; v1; ...; vn-1] vn
means a path from v0 to vn composed of n edges (vi,vi+1) *)
inductive path vertex (list vertex) vertex =
| Path_empty:
forall x: vertex. path x Nil x
| Path_cons:
forall x y z: vertex, l: list vertex.
edge x y -> path y l z -> path x (Cons x l) z
lemma path_right_extension:
forall x y z: vertex, l: list vertex.
path x l y -> edge y z -> path x (l ++ Cons y Nil) z
lemma path_trans:
forall x y z: vertex, l1 l2: list vertex.
path x l1 y -> path y l2 z -> path x (l1 ++ l2) z
lemma empty_path:
forall x y: vertex. path x Nil y -> x = y
lemma path_left_extension :
forall g : graph, v1 v2 v3 : vertex.
edge g v1 v2 -> path g v2 v3 -> path g v1 v3
theory IntPathWeight
clone export Path
use export int.Int
lemma path_right_extension :
forall g : graph, v1 v2 v3 : vertex.
path g v1 v2 -> edge g v2 v3 -> path g v1 v3
function weight vertex vertex : int
(* the total weight of a path [path _ l dst] *)
function path_weight (l: list vertex) (dst: vertex) : int = match l with
| Nil -> 0
| Cons x Nil -> weight x dst
| Cons x ((Cons y _) as r) -> weight x y + path_weight r dst
lemma path_weight_right_extension:
forall x y z: vertex, l: list vertex.
path_weight (l ++ Cons x Nil) y = path_weight l x + weight x y
theory SimplePath
use import list.List
......@@ -53,3 +79,10 @@ theory SimplePath
exists l : list vertex. l <> Nil /\ simple_path g v l v
Local Variables:
compile-command: "make -C .. theories/graph.gui"
......@@ -278,6 +278,41 @@ theory Iter
(* integers extended with infinity *)
theory IntInf
use import Int
type t = Finite int | Infinite
function add (x: t) (y: t) : t =
match x with
| Infinite -> Infinite
| Finite x ->
match y with
| Infinite -> Infinite
| Finite y -> Finite (x + y)
predicate lt (x y: t) =
match x with
| Infinite -> false
| Finite x ->
match y with
| Infinite -> true
| Finite y -> x < y
predicate le (x y: t) = lt x y \/ x = y
clone export relations.TotalOrder with type t = t, predicate rel = le,
lemma Refl, lemma Antisymm, lemma Trans, lemma Total
theory Induction
use import Int
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