Last change
on this file since 2970 was
2949,
checked in by sacerdot, 8 years ago

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

File size:
924 bytes

Rev  Line  

[2174]  1  include "common/Graphs.ma". 

 2  

 3  record 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  

 11  definition valuation ≝ λlatt : property_lattice.label → latt. 

 12  definition rhs ≝ λlatt : property_lattice.valuation latt → latt. 

 13  definition equations ≝ λlatt : property_lattice.label → rhs latt. 

 14  

[2949]  15  record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝ 

 16  { fix_lfp :> valuation latt 

[2174]  17  ; fix_correct : 

 18  ∀l : label. 

[2949]  19  (* inclusion suffices for correctness *) 

 20  l_included latt (eqs l fix_lfp) (fix_lfp l) 

[2174]  21  }. 

 22  

[2949]  23  definition fixpoint_computer : Type[1] ≝ ∀latt,eqs.fixpoint latt eqs. 

 24  

 25  coercion 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.