src/ZF/OrderType.ML
changeset 1032 54b9f670c67e
parent 984 4fb1d099ba45
child 1461 6bcb44e4d6e5
--- a/src/ZF/OrderType.ML	Thu Apr 13 11:30:57 1995 +0200
+++ b/src/ZF/OrderType.ML	Thu Apr 13 11:32:44 1995 +0200
@@ -417,6 +417,7 @@
 	   setloop rtac (InlI RSN (2,RepFun_eqI))) 1);
 qed "lt_oadd1";
 
+(*Thus also we obtain the rule  i++j = k ==> i le k *)
 goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le i++j";
 by (resolve_tac [all_lt_imp_le] 1);
 by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1));
@@ -453,7 +454,21 @@
 		     ordertype_sum_Memrel]) 1);
 qed "oadd_lt_mono2";
 
-goal OrderType.thy "!!i j. [| i++j = i++k; Ord(i); Ord(j); Ord(k) |] ==> j=k";
+goal OrderType.thy
+    "!!i j k. [| i++j < i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j<k";
+by (rtac Ord_linear_lt 1);
+by (REPEAT_SOME assume_tac);
+by (ALLGOALS
+    (fast_tac (ZF_cs addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
+qed "oadd_lt_cancel2";
+
+goal OrderType.thy
+    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
+by (fast_tac (ZF_cs addSIs [oadd_lt_mono2] addSEs [oadd_lt_cancel2]) 1);
+qed "oadd_lt_iff2";
+
+goal OrderType.thy
+    "!!i j k. [| i++j = i++k;  Ord(i);  Ord(j); Ord(k) |] ==> j=k";
 by (rtac Ord_linear_lt 1);
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS
@@ -567,6 +582,12 @@
 by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
 qed "oadd_le_mono";
 
+goal OrderType.thy
+    "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
+by (asm_simp_tac (ZF_ss addsimps [oadd_lt_iff2, oadd_succ RS sym, 
+				  Ord_succ]) 1);
+qed "oadd_le_iff2";
+
 
 (** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
     Probably simpler to define the difference recursively!
@@ -597,10 +618,9 @@
 by (fast_tac (ZF_cs addEs [lt_trans2, lt_trans]) 1);
 qed "ordertype_sum_Diff";
 
-goalw OrderType.thy [oadd_def]
+goalw OrderType.thy [oadd_def, odiff_def]
     "!!i j. i le j ==> 	\
-\           i ++ ordertype(j-i, Memrel(j)) = \
-\           ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
+\           i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
 by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1]));
 by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
 by (eresolve_tac [id_ord_iso_Memrel] 1);
@@ -609,13 +629,35 @@
 		      Diff_subset] 1));
 qed "oadd_ordertype_Diff";
 
-goal OrderType.thy
-    "!!i j. i le j ==> i ++ ordertype(j-i, Memrel(j)) = j";
+goal OrderType.thy "!!i j. i le j ==> i ++ (j--i) = j";
 by (asm_simp_tac (ZF_ss addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, 
 				  ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1);
-qed "oadd_inverse";
+qed "oadd_odiff_inverse";
+
+goalw OrderType.thy [odiff_def] 
+    "!!i j. [| Ord(i);  Ord(j) |] ==> Ord(i--j)";
+by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, 
+		      Diff_subset] 1));
+qed "Ord_odiff";
 
-(*By oadd_inject, the difference between i and j is unique.*)
+(*By oadd_inject, the difference between i and j is unique.  Note that we get
+  i++j = k  ==>  j = k--i.  *)
+goal OrderType.thy
+    "!!i j. [| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
+br oadd_inject 1;
+by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
+by (asm_simp_tac (ZF_ss addsimps [oadd_odiff_inverse, oadd_le_self]) 1);
+qed "odiff_oadd_inverse";
+
+val [i_lt_j, k_le_i] = goal OrderType.thy
+    "[| i<j;  k le i |] ==> i--k < j--k";
+by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1);
+by (simp_tac
+    (ZF_ss addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans,
+		     oadd_odiff_inverse]) 1);
+by (REPEAT (resolve_tac (Ord_odiff :: 
+			 ([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1));
+qed "odiff_lt_mono2";
 
 
 (**** Ordinal Multiplication ****)
@@ -842,11 +884,6 @@
 			  Ord_succD] 1));
 qed "omult_lt_mono";
 
-goal OrderType.thy
-      "!!i j. [| i' le i;  j' le j |] ==> i'++j' le i++j";
-by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
-qed "oadd_le_mono";
-
 goal OrderType.thy "!!i j. [| Ord(i);  0<j |] ==> i le j**i";
 by (forward_tac [lt_Ord2] 1);
 by (eres_inst_tac [("i","i")] trans_induct3 1);