finite_tarski.mlw 1.69 KB
 Léon Gondelman committed Sep 18, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 13 `````` use set.Fset `````` Andrei Paskevich committed Jun 14, 2018 14 `````` clone export relations.PartialOrder with axiom . `````` Léon Gondelman committed Sep 18, 2014 15 `````` `````` Andrei Paskevich committed Jun 10, 2017 16 `````` constant a : set t `````` Léon Gondelman committed Sep 18, 2014 17 `````` `````` Andrei Paskevich committed Jun 10, 2017 18 `````` constant e : t `````` Léon Gondelman committed Sep 18, 2014 19 20 `````` axiom minimality: mem e a /\ forall x. mem x a -> rel e x `````` Andrei Paskevich committed Jun 10, 2017 21 `````` function f t : t `````` Léon Gondelman committed Sep 18, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 30 `````` use set.Fset `````` Andrei Paskevich committed Jun 14, 2018 31 `````` clone export Tarski with axiom . `````` Léon Gondelman committed Sep 18, 2014 32 33 34 `````` let lemma least_fix_point () : unit ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x } `````` MARCHE Claude committed Mar 18, 2016 35 `````` = let rec ghost aux (x: t) (b: set t) : t `````` Léon Gondelman committed Sep 18, 2014 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 `````` Andrei Paskevich committed Jun 15, 2018 47 `````` use set.Fset `````` Andrei Paskevich committed Jun 14, 2018 48 `````` clone export Tarski with axiom . `````` Andrei Paskevich committed Jun 15, 2018 49 `````` use ref.Ref `````` Léon Gondelman committed Sep 18, 2014 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``````