Changeset 3576 for LTS/Traces.ma

Timestamp:

Jun 19, 2015, 1:56:43 PM (4 years ago)

Author:

piccolo

Message:

 

File:

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

LTS/Traces.ma

@@ -277 +277 @@
                              ]
 ].
+
+lemma eq_ActionLabel_elim : ∀P : bool → Prop.∀p,c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_ActionLabel p c1 c2).
+#P #p * [#f #lab | * [| #lab] | * [| #lab] ] *
+[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
+whd in match eq_ActionLabel; normalize nodelta
+try(@H2 % #EQ destruct)
+[ @eq_function_name_elim [ @eq_call_cost_lab_elim [| #H #_ lapply H -H ] ]  | @eq_return_cost_lab_elim | | @eq_fn_label_elim ]
+normalize nodelta
+[1,4,6,7,9: try(#EQ destruct) try(#EQ destruct) @H1 %
+|*: * #H @H2 % #EQ destruct cases H %
+]
+qed.
+
+definition DeqActionLabel ≝ λp.mk_DeqSet (ActionLabel p) (eq_ActionLabel p) ?.
+@hide_prf #x #y @eq_ActionLabel_elim [ #EQ destruct % // | * #H % #EQ destruct cases H %]
+qed.
+
+unification hint  0 ≔ p ; 
+    X ≟ (DeqActionLabel p)
+(* ---------------------------------------- *) ⊢ 
+    (ActionLabel p) ≡ carr X.
+
+unification hint  0 ≔ p,p1,p2; 
+    X ≟ (DeqActionLabel p)
+(* ---------------------------------------- *) ⊢ 
+    eq_ActionLabel p p1 p2 ≡ eqb X p1 p2.
 
 definition is_cost_label : ∀p.ActionLabel p → Prop ≝