Changeset 3576 for LTS/Traces.ma


Ignore:
Timestamp:
Jun 19, 2015, 1:56:43 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3549 r3576  
    277277                             ]
    278278].
     279
     280lemma eq_ActionLabel_elim : ∀P : bool → Prop.∀p,c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_ActionLabel p c1 c2).
     281#P #p * [#f #lab | * [| #lab] | * [| #lab] ] *
     282[1,4,7,10,13: #f' #lab' |2,5,8,14: * [2,4,6,8: #lab'] |*: * [2,4,6,8,10,12: #lab'] ] #H1 #H2
     283whd in match eq_ActionLabel; normalize nodelta
     284try(@H2 % #EQ destruct)
     285[ @eq_function_name_elim [ @eq_call_cost_lab_elim [| #H #_ lapply H -H ] ]  | @eq_return_cost_lab_elim | | @eq_fn_label_elim ]
     286normalize nodelta
     287[1,4,6,7,9: try(#EQ destruct) try(#EQ destruct) @H1 %
     288|*: * #H @H2 % #EQ destruct cases H %
     289]
     290qed.
     291
     292definition DeqActionLabel ≝ λp.mk_DeqSet (ActionLabel p) (eq_ActionLabel p) ?.
     293@hide_prf #x #y @eq_ActionLabel_elim [ #EQ destruct % // | * #H % #EQ destruct cases H %]
     294qed.
     295
     296unification hint  0 ≔ p ;
     297    X ≟ (DeqActionLabel p)
     298(* ---------------------------------------- *) ⊢
     299    (ActionLabel p) ≡ carr X.
     300
     301unification hint  0 ≔ p,p1,p2;
     302    X ≟ (DeqActionLabel p)
     303(* ---------------------------------------- *) ⊢
     304    eq_ActionLabel p p1 p2 ≡ eqb X p1 p2.
    279305
    280306definition is_cost_label : ∀p.ActionLabel p → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.