Changeset 1528 for src/utilities


Ignore:
Timestamp:
Nov 22, 2011, 11:58:43 AM (9 years ago)
Author:
campbell
Message:

Update most of Assembly.ma with new syntax and identifier maps.
Change positive.ma a little to reduce name clashes.

Location:
src/utilities/binary
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/division.ma

    r1523 r1528  
    9292theorem plus_minus_r:
    9393∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
    94 #m #n #p #le >(commutative_plus …)
    95 >(commutative_plus p ?) @plus_minus //; qed.
     94#m #n #p #le >(commutative_plus_pos …)
     95>(commutative_plus_pos p ?) @plus_minus //; qed.
    9696
    9797lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
     
    169169  | MinusPos r ⇒ n = m+r
    170170  ].
    171 #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);
     171#n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus_pos n m);
    172172normalize; cases (partial_minus n m); /2/; qed.
    173173
     
    275275cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
    276276>DIV in ⊢ (% → ?); #H #lt destruct;
    277 [ lapply (plus_to_minus … e0);
     277[ lapply (plus_to_minus_pos … e0);
    278278    >(commutative_times …) >(commutative_times dv'' …)
    279279    cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
  • src/utilities/binary/positive.ma

    r1523 r1528  
    217217] qed.
    218218
    219 theorem commutative_plus : commutative ? plus.
     219theorem commutative_plus_pos : commutative ? plus.
    220220#n elim n;
    221221[ #y cases y; normalize; //;
     
    224224
    225225theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.
    226 #n #m >(commutative_plus (succ n) m)
     226#n #m >(commutative_plus_pos (succ n) m)
    227227<(plus_n_succm …) //; qed.
    228228
     
    775775] qed.
    776776
    777 theorem minus_n_n: ∀n:Pos.one=n-n.
     777theorem minus_n_n_pos: ∀n:Pos.one=n-n.
    778778#n normalize; >(partial_minus_n_n n) //;
    779779qed.
     
    877877qed.
    878878
    879 theorem minus_to_plus :∀n,m,p:Pos.
     879theorem minus_to_plus_pos :∀n,m,p:Pos.
    880880  m < n → n-m = p → n = m+p.
    881881#n #m #p #lemn #eqp applyS plus_minus_m_m; //;
    882882qed.
    883883
    884 theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p.
     884theorem plus_to_minus_pos :∀n,m,p:Pos.n = m+p → n-m = p.
    885885(* /4/ done in 43.5 *)
    886886#n #m #p #eqp
Note: See TracChangeset for help on using the changeset viewer.