Changeset 3524 for LTS/costs.ma

Timestamp:

Mar 11, 2015, 4:26:40 PM (6 years ago)

Author:

piccolo

Message:

rearrangments of lemmas, final statement in place

File:

• LTS/costs.ma (modified) (1 diff)

LTS/costs.ma

@@ -32 +32 @@
 record concrete_transition_sys : Type[2] ≝ 
 { trans_sys :> abstract_status
-; cost_mon : monoid
-; cost_of : trans_sys → cost_mon
 }.
 
-record abstract_transition_sys (concrete_costs : Type[0]) : Type[1] ≝ 
+record abstract_transition_sys : Type[1] ≝ 
 { abs_state_t :> Type[0]
 ; abs_instr : monoid
 ; act_abs : monoid_action abs_instr abs_state_t
-; abs_cost : abs_state_t → concrete_costs
 }.
 
 notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
-interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
+interpretation "act_abs" 'sem f x = (act ?? (act_abs ?) f x).
 
 record galois_rel (C : concrete_transition_sys) 
-                   (A : abstract_transition_sys (cost_mon C)) : Type[0] ≝ 
+                   (A : abstract_transition_sys) : Type[0] ≝ 
 { rel_galois :2> C → A → Prop
-; rel_galois_cost : ∀s,a.rel_galois … s a → abs_cost … a = cost_of … s
 }.
 
 record galois_connection : Type[2] ≝ 
 { concr : concrete_transition_sys
-; abs_d : abstract_transition_sys (cost_mon concr)
+; abs_d : abstract_transition_sys
 ; galois_rel:> galois_rel concr abs_d
 }.