source: src/utilities/fixpoints.ma @ 3257

Last change on this file since 3257 was 2949, checked in by sacerdot, 7 years ago

Some advance/repairing in ERTLptrToLTLProof. In particular, we know take in
account that the fixpoint computation only returns a pre-fixpoint.

File size: 924 bytes
Line 
1include "common/Graphs.ma".
2
3record property_lattice : Type[1] ≝
4{ l_property  :> Type[0]
5; l_bottom    : l_property
6; l_equal : l_property → l_property → bool
7; l_included : l_property → l_property → bool
8; l_is_maximal : l_property → bool
9}.
10
11definition valuation ≝ λlatt : property_lattice.label → latt.
12definition rhs ≝ λlatt : property_lattice.valuation latt → latt.
13definition equations ≝ λlatt : property_lattice.label → rhs latt.
14
15record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝
16{ fix_lfp :> valuation latt
17; fix_correct :
18  ∀l : label.
19   (* inclusion suffices for correctness *)
20   l_included latt (eqs l fix_lfp) (fix_lfp l)
21}.
22
23definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs.
24
25coercion apply_fixpoint:
26 ∀latt,eqs.∀f:fixpoint latt eqs. label → latt ≝
27 λlatt,eqs,f,l. fix_lfp … f l
28 on _f: fixpoint ? ? to label → ?.
Note: See TracBrowser for help on using the repository browser.