Changeset 2949 for src/utilities


Ignore:
Timestamp:
Mar 25, 2013, 9:48:01 PM (7 years ago)
Author:
sacerdot
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/fixpoints.ma

    r2700 r2949  
    1313definition equations ≝ λlatt : property_lattice.label → rhs latt.
    1414
    15 record fixpoint (latt : property_lattice) : Type[0] ≝
    16 { fix_lfp :1> equations latt → valuation latt
     15record fixpoint (latt : property_lattice) (eqs: equations latt) : Type[0] ≝
     16{ fix_lfp :> valuation latt
    1717; fix_correct :
    18   ∀eqs : equations latt.
    19   let sol ≝ fix_lfp eqs in
    2018  ∀l : label.
    21   l_included latt (eqs l sol) (sol l) (* inclusion suffices for correctness *)
     19   (* inclusion suffices for correctness *)
     20   l_included latt (eqs l fix_lfp) (fix_lfp l)
    2221}.
    2322
    24 definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt.
     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 TracChangeset for help on using the changeset viewer.