Changeset 3402


Ignore:
Timestamp:
Dec 6, 2013, 10:39:04 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3401 r3402  
    783783qed.
    784784
     785lemma domain_of_associative_list_append : ∀A,B.∀l1,l2 : associative_list A B.
     786domain_of_associative_list ?? (l1 @ l2) =
     787 (domain_of_associative_list ?? l1) @ (domain_of_associative_list ?? l2).
     788#A #B #l1 elim l1 // #x #xs #IH #l2 normalize //
     789qed.
     790
    785791lemma lab_map_in_domain: ∀p.∀i: Instructions p.
    786792 ∀x,n,l.
    787793  x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) →
    788794   x ∈ get_labels_of_code … i.
    789  cases daemon
     795#p #i elim i //
     796[ #seq * [|#lbl] #i1 #IH #x #n #l whd in match(call_post_trans ????);
     797  whd in match (get_labels_of_code ??); /2/ whd in match (memb ???);
     798  inversion(x==lbl) #Hlbl normalize nodelta [#_ whd in match (memb ???); >Hlbl % ]
     799  #H >memb_cons // @IH //
     800| #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l
     801  whd in match (call_post_trans ????); whd in match (memb ???);
     802  whd in match (get_labels_of_code ??); inversion(x == ltrue) #Hlbl normalize nodelta
     803  [ #_ whd in match (memb ???); >Hlbl % ] whd in match (memb ???);
     804  inversion(x == lfalse) #Hlbl1 normalize nodelta
     805  [ #_ whd in match (memb ???); >Hlbl normalize nodelta whd in match (memb ???);
     806    >Hlbl1 % ] #H >memb_cons // >memb_cons // >domain_of_associative_list_append in H;
     807    #H cases(memb_append … H) [ #H1 >memb_append_l1 // @IH1 [3: >H1 // |*:] ]
     808    >domain_of_associative_list_append #H1 cases(memb_append … H1)
     809    #H2 >memb_append_l2 // [ >memb_append_l1 | >memb_append_l2 ] //
     810    [ @IH2 | @IH3] /2 by eq_true_to_b/
     811| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l whd in match (call_post_trans ????);
     812  whd in match (get_labels_of_code ??); whd in match (memb ???); inversion(x == lfalse)
     813  #Hlfalse normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlfalse // ]
     814  whd in match (memb ???); inversion(x==ltrue) normalize nodelta #Hltrue
     815  [ #_ whd in match (memb ???); >Hltrue %] >domain_of_associative_list_append #H
     816  cases(memb_append … H) #H1 >memb_cons // >memb_cons // [ >memb_append_l1 | >memb_append_l2 ]
     817  // [ @IH1 | @IH2] /2/
     818| #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????);
     819  whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion (x == lbl)
     820  #Hlbl normalize nodelta [ #_ whd in match (memb ???); >Hlbl % ] #H >memb_cons // @IH /2/
     821| #lin #io #lout #i1 #IH #x #n #l whd in match (memb ???); inversion(x == lout) #Hlout
     822  normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlout % ]
     823  whd in match (memb ???); inversion(x==lin) #Hlin normalize nodelta
     824  [ #_ whd in match (memb ???); >Hlin % ] #H >memb_cons // >memb_cons // @IH /2/
     825]
    790826qed.
    791827
Note: See TracChangeset for help on using the changeset viewer.