Ignore:
Timestamp:
Dec 8, 2010, 11:40:42 AM (9 years ago)
Author:
campbell
Message:

Tidy up some decidability functions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r387 r388  
    325325##] nqed.
    326326
    327 nlemma is_not_void_true: ∀f. ¬fn_return f = Tvoid → ∃p. is_not_void (fn_return f) = OK ? p.
    328 #f; ncases f; #ty; #_; #_; #_; ncases ty;
    329 ##[ #H; napply False_ind; /2/;
    330 ##| #sz sg e; @ ?; //; ##| #sz e; @ ?; // ##| #sp ty e; @ ?; // ##| #sp ty n e; @ ?; // ##|
    331     #tys ty e; @ ?; // ##| #id fs e; @ ?; // ##| #id fs e; @ ?; // ##| #id e; @ ?; // ##]
    332 nqed.
    333 
    334327nlemma alloc_vars_complete: ∀env,m,l,env',m'.
    335328  alloc_variables env m l env' m' →
     
    368361    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    369362    napply refl;
    370 ##] nqed.   
    371 
     363##] nqed.
     364
     365nlemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f.
     366#P f p Q H; ncases f;
     367##[ napply H
     368##| #np; napply False_ind; napply (absurd ? p np);
     369##] nqed.
     370
     371nlemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f.
     372#P f p Q H; ncases f;
     373##[ #np; napply False_ind; napply (absurd ? np p);
     374##| napply H
     375##] nqed.
    372376
    373377ntheorem step_complete: ∀ge,s,tr,s'.
     
    436440##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl;
    437441##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?);
    438     nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?);
     442    napply (dec_false ? (type_eq_dec (fn_return f) Tvoid) H1); #pf';
     443    nwhd in ⊢ (??%?);
    439444    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
    440445    napply refl;
     
    552557  nwhd in ⊢ (???%);
    553558  ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
    554                     napply err_sig_does_not_interact; #x; napply err2_does_not_interact; // ##]
     559                    ncases (type_eq_dec (fn_return f) Tvoid); #x; //; napply err2_does_not_interact; // ##]
    555560  ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
    556561  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
Note: See TracChangeset for help on using the changeset viewer.