Changeset 1528 for src/utilities/binary

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:

• division.ma (modified) (3 diffs)
• positive.ma (modified) (4 diffs)

src/utilities/binary/division.ma

@@ -92 +92 @@
 theorem plus_minus_r:
 ∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
-#m #n #p #le >(commutative_plus …)
->(commutative_plus p ?) @plus_minus //; qed.
+#m #n #p #le >(commutative_plus_pos …)
+>(commutative_plus_pos p ?) @plus_minus //; qed.
 
 lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
@@ -169 +169 @@
   | MinusPos r ⇒ n = m+r
   ].
-#n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);
+#n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus_pos n m);
 normalize; cases (partial_minus n m); /2/; qed.
 
@@ -275 +275 @@
 cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
 >DIV in ⊢ (% → ?); #H #lt destruct;
-[ lapply (plus_to_minus … e0);
+[ lapply (plus_to_minus_pos … e0);
     >(commutative_times …) >(commutative_times dv'' …)
     cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt

src/utilities/binary/positive.ma

@@ -217 +217 @@
 ] qed.
 
-theorem commutative_plus : commutative ? plus.
+theorem commutative_plus_pos : commutative ? plus.
 #n elim n;
 [ #y cases y; normalize; //;
@@ -224 +224 @@
 
 theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.
-#n #m >(commutative_plus (succ n) m)
+#n #m >(commutative_plus_pos (succ n) m)
 <(plus_n_succm …) //; qed.
 
@@ -775 +775 @@
 ] qed.
 
-theorem minus_n_n: ∀n:Pos.one=n-n.
+theorem minus_n_n_pos: ∀n:Pos.one=n-n.
 #n normalize; >(partial_minus_n_n n) //;
 qed.
@@ -877 +877 @@
 qed.
 
-theorem minus_to_plus :∀n,m,p:Pos.
+theorem minus_to_plus_pos :∀n,m,p:Pos.
   m < n → n-m = p → n = m+p.
 #n #m #p #lemn #eqp applyS plus_minus_m_m; //;
 qed.
 
-theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p.
+theorem plus_to_minus_pos :∀n,m,p:Pos.n = m+p → n-m = p.
 (* /4/ done in 43.5 *)
 #n #m #p #eqp