finite_tarski.mlw 1.69 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12
(**

Proof of Tarski fixed point theorem (existence of least fixed point)
for finite sets, using lemma functions.

Authors:  Martin Clochard
          Léon Gondelman
*)


module Tarski

13
  use set.Fset
14
  clone export relations.PartialOrder with axiom .
15

16
  constant a : set t
17

18
  constant e : t
19 20
  axiom minimality: mem e a /\ forall x. mem x a -> rel e x

21
  function f t : t
22 23 24 25 26 27 28 29
  axiom range: forall x. mem x a -> mem (f x) a
  axiom monotone: forall x y. mem x a -> mem y a -> rel x y -> rel (f x) (f y)

  predicate fixpoint (x:t) = mem x a /\ f x = x

end

module Tarski_rec
30
  use set.Fset
31
  clone export Tarski with axiom .
32 33 34

  let lemma least_fix_point () : unit
   ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
MARCHE Claude's avatar
MARCHE Claude committed
35
   = let rec ghost aux (x: t) (b: set t) : t
36 37 38 39 40 41 42 43 44 45 46
       requires { mem x a /\ subset b a }
       requires { forall y. mem y a -> rel x y -> mem y b }
       requires { forall y. fixpoint y -> rel x y }
       requires { rel x (f x) }
       ensures  { fixpoint result /\ forall x. fixpoint x -> rel result x }
       variant  { cardinal b }
     = let y = f x in if x = y then x else aux y (remove x b)
     in let _witness = aux e a in ()
end

module Tarski_while
47
  use set.Fset
48
  clone export Tarski with axiom .
49
  use ref.Ref
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66

  let lemma least_fix_point () : unit
   ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
   =
     let x = ref e in
     let b = ref a in
     while (f !x) <> !x do
      invariant { mem !x a /\ subset !b a}
      invariant { forall y. mem y a -> rel !x y -> mem y !b }
      invariant { forall y. fixpoint y -> rel !x y }
      invariant { rel !x (f !x) }
      variant   { cardinal !b }
      b := remove !x !b;
      x := f !x
     done

end