# HG changeset patch
# User paulson
# Date 932027596 -7200
# Node ID 6def5ce146e23266602c1628ae99178da6309b05
# Parent  b46ccfee8e59656c524f237ed68d18ff100cd603
qed_goal -> Goal;  new theorems nat_le_0, nat_le_eq_zle and zdiff_int

diff -r b46ccfee8e59 -r 6def5ce146e2 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Thu Jul 15 10:27:54 1999 +0200
+++ b/src/HOL/Integ/Bin.ML	Thu Jul 15 10:33:16 1999 +0200
@@ -12,86 +12,86 @@
 
 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
 
-qed_goal "NCons_Pls_0" thy
-    "NCons Pls False = Pls"
- (fn _ => [(Simp_tac 1)]);
+Goal "NCons Pls False = Pls";
+by (Simp_tac 1);
+qed "NCons_Pls_0";
 
-qed_goal "NCons_Pls_1" thy
-    "NCons Pls True = Pls BIT True"
- (fn _ => [(Simp_tac 1)]);
+Goal "NCons Pls True = Pls BIT True";
+by (Simp_tac 1);
+qed "NCons_Pls_1";
 
-qed_goal "NCons_Min_0" thy
-    "NCons Min False = Min BIT False"
- (fn _ => [(Simp_tac 1)]);
+Goal "NCons Min False = Min BIT False";
+by (Simp_tac 1);
+qed "NCons_Min_0";
 
-qed_goal "NCons_Min_1" thy
-    "NCons Min True = Min"
- (fn _ => [(Simp_tac 1)]);
+Goal "NCons Min True = Min";
+by (Simp_tac 1);
+qed "NCons_Min_1";
 
-qed_goal "bin_succ_1" thy
-    "bin_succ(w BIT True) = (bin_succ w) BIT False"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_succ(w BIT True) = (bin_succ w) BIT False";
+by (Simp_tac 1);
+qed "bin_succ_1";
 
-qed_goal "bin_succ_0" thy
-    "bin_succ(w BIT False) =  NCons w True"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_succ(w BIT False) =  NCons w True";
+by (Simp_tac 1);
+qed "bin_succ_0";
 
-qed_goal "bin_pred_1" thy
-    "bin_pred(w BIT True) = NCons w False"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_pred(w BIT True) = NCons w False";
+by (Simp_tac 1);
+qed "bin_pred_1";
 
-qed_goal "bin_pred_0" thy
-    "bin_pred(w BIT False) = (bin_pred w) BIT True"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_pred(w BIT False) = (bin_pred w) BIT True";
+by (Simp_tac 1);
+qed "bin_pred_0";
 
-qed_goal "bin_minus_1" thy
-    "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)";
+by (Simp_tac 1);
+qed "bin_minus_1";
 
-qed_goal "bin_minus_0" thy
-    "bin_minus(w BIT False) = (bin_minus w) BIT False"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_minus(w BIT False) = (bin_minus w) BIT False";
+by (Simp_tac 1);
+qed "bin_minus_0";
 
 
 (*** bin_add: binary addition ***)
 
-qed_goal "bin_add_BIT_11" thy
-    "bin_add (v BIT True) (w BIT True) = \
-\    NCons (bin_add v (bin_succ w)) False"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_add (v BIT True) (w BIT True) = \
+\    NCons (bin_add v (bin_succ w)) False";
+by (Simp_tac 1);
+qed "bin_add_BIT_11";
 
-qed_goal "bin_add_BIT_10" thy
-    "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True";
+by (Simp_tac 1);
+qed "bin_add_BIT_10";
 
-qed_goal "bin_add_BIT_0" thy
-    "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
- (fn _ => [Auto_tac]);
+Goal "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y";
+by Auto_tac;
+qed "bin_add_BIT_0";
 
 Goal "bin_add w Pls = w";
 by (induct_tac "w" 1);
 by Auto_tac;
 qed "bin_add_Pls_right";
 
-qed_goal "bin_add_BIT_Min" thy
-    "bin_add (v BIT x) Min = bin_pred (v BIT x)"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_add (v BIT x) Min = bin_pred (v BIT x)";
+by (Simp_tac 1);
+qed "bin_add_BIT_Min";
 
-qed_goal "bin_add_BIT_BIT" thy
-    "bin_add (v BIT x) (w BIT y) = \
-\    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_add (v BIT x) (w BIT y) = \
+\    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)";
+by (Simp_tac 1);
+qed "bin_add_BIT_BIT";
 
 
 (*** bin_mult: binary multiplication ***)
 
-qed_goal "bin_mult_1" thy
-    "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w";
+by (Simp_tac 1);
+qed "bin_mult_1";
 
-qed_goal "bin_mult_0" thy
-    "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False";
+by (Simp_tac 1);
+qed "bin_mult_0";
 
 
 (**** The carry/borrow functions, bin_succ and bin_pred ****)
@@ -99,22 +99,22 @@
 
 (**** number_of ****)
 
-qed_goal "number_of_NCons" thy
-    "number_of(NCons w b) = (number_of(w BIT b)::int)"
- (fn _ =>[(induct_tac "w" 1),
-          (ALLGOALS Asm_simp_tac) ]);
+Goal "number_of(NCons w b) = (number_of(w BIT b)::int)";
+by (induct_tac "w" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "number_of_NCons";
 
 Addsimps [number_of_NCons];
 
-qed_goal "number_of_succ" thy
-    "number_of(bin_succ w) = int 1 + number_of w"
- (fn _ =>[induct_tac "w" 1,
-          (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
+Goal "number_of(bin_succ w) = int 1 + number_of w";
+by (induct_tac "w" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
+qed "number_of_succ";
 
-qed_goal "number_of_pred" thy
-    "number_of(bin_pred w) = - (int 1) + number_of w"
- (fn _ =>[induct_tac "w" 1,
-          (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
+Goal "number_of(bin_pred w) = - (int 1) + number_of w";
+by (induct_tac "w" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
+qed "number_of_pred";
 
 Goal "number_of(bin_minus w) = (- (number_of w)::int)";
 by (induct_tac "w" 1);
@@ -665,12 +665,14 @@
     (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
 qed "nat_0_le"; 
 
-Goal "z < #0 ==> nat z = 0"; 
-by (asm_full_simp_tac
-    (simpset() addsimps [neg_eq_less_0, zle_def, neg_nat]) 1); 
-qed "nat_less_0"; 
+Goal "z <= #0 ==> nat z = 0"; 
+by (case_tac "z = #0" 1);
+by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
+by (asm_full_simp_tac 
+    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
+qed "nat_le_0"; 
 
-Addsimps [nat_0_le, nat_less_0];
+Addsimps [nat_0_le, nat_le_0];
 
 Goal "#0 <= w ==> (nat w = m) = (w = int m)";
 by Auto_tac;
@@ -740,6 +742,17 @@
 	      simpset() addsimps [neg_eq_less_0, zle_def]));
 qed "nat_less_eq_zless";
 
+Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)";
+by (auto_tac (claset(), 
+	      simpset() addsimps [linorder_not_less RS sym, 
+				  zless_nat_conj]));
+qed "nat_le_eq_zle";
+
+(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
+Goal "n<=m --> int m - int n = int (m-n)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by Auto_tac;
+qed_spec_mp "zdiff_int";
 
 (*Towards canonical simplification*)
 Addsimps zadd_ac;