Changeset 3524 for LTS/costs.ma


Ignore:
Timestamp:
Mar 11, 2015, 4:26:40 PM (6 years ago)
Author:
piccolo
Message:

rearrangments of lemmas, final statement in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/costs.ma

    r3500 r3524  
    3232record concrete_transition_sys : Type[2] ≝
    3333{ trans_sys :> abstract_status
    34 ; cost_mon : monoid
    35 ; cost_of : trans_sys → cost_mon
    3634}.
    3735
    38 record abstract_transition_sys (concrete_costs : Type[0]) : Type[1] ≝
     36record abstract_transition_sys : Type[1] ≝
    3937{ abs_state_t :> Type[0]
    4038; abs_instr : monoid
    4139; act_abs : monoid_action abs_instr abs_state_t
    42 ; abs_cost : abs_state_t → concrete_costs
    4340}.
    4441
    4542notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
    46 interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
     43interpretation "act_abs" 'sem f x = (act ?? (act_abs ?) f x).
    4744
    4845record galois_rel (C : concrete_transition_sys)
    49                    (A : abstract_transition_sys (cost_mon C)) : Type[0] ≝
     46                   (A : abstract_transition_sys) : Type[0] ≝
    5047{ rel_galois :2> C → A → Prop
    51 ; rel_galois_cost : ∀s,a.rel_galois … s a → abs_cost … a = cost_of … s
    5248}.
    5349
    5450record galois_connection : Type[2] ≝
    5551{ concr : concrete_transition_sys
    56 ; abs_d : abstract_transition_sys (cost_mon concr)
     52; abs_d : abstract_transition_sys
    5753; galois_rel:> galois_rel concr abs_d
    5854}.
Note: See TracChangeset for help on using the changeset viewer.