Changeset 15 for C-semantics/extralib.ma


Ignore:
Timestamp:
Jul 22, 2010, 4:50:06 PM (10 years ago)
Author:
campbell
Message:

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/extralib.ma

    r14 r15  
    119119nlemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    120120#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
    121 /3/; nqed.
     121/3/; ncases x; /3/; nqed.
    122122
    123123nlemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    124124#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
    125 /3/; #H; nrewrite > H; //; nqed.
     125ncases x; /3/; nqed.
    126126
    127127ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
     
    169169interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
    170170
    171 ndefinition Zleb : Z → Z → bool ≝
    172 λx,y:Z.
     171nlet rec Zleb (x:Z) (y:Z) : bool ≝
    173172  match x with
    174173  [ OZ ⇒
     
    188187    | neg m ⇒ leb m n ]].
    189188   
    190 ndefinition Zltb : Z → Z → bool ≝
    191 λx,y:Z.
     189nlet rec Zltb (x:Z) (y:Z) : bool ≝
    192190  match x with
    193191  [ OZ ⇒
     
    267265##] nqed.
    268266
    269 ndefinition Z_times : Z → Z → Z ≝
    270 λx,y. match x with
     267nlet rec Z_times (x:Z) (y:Z) : Z ≝
     268match x with
    271269[ OZ ⇒ OZ
    272270| pos n ⇒
     
    697695        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
    698696            nrewrite > (pos_compare_lt … l'); //;
    699         ##| /2/;
     697        ##| napply Zminus_Zlt; //;
    700698        ##]
    701699      ##]
Note: See TracChangeset for help on using the changeset viewer.