--- a/src/HOL/Arith.ML Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Arith.ML Thu Dec 04 12:44:37 1997 +0100
@@ -9,56 +9,38 @@
(*** Basic rewrite rules for the arithmetic operators ***)
-goalw Arith.thy [pred_def] "pred 0 = 0";
-by (Simp_tac 1);
-qed "pred_0";
-
-goalw Arith.thy [pred_def] "pred(Suc n) = n";
-by (Simp_tac 1);
-qed "pred_Suc";
-
-Addsimps [pred_0,pred_Suc];
-
-(** pred **)
-
-val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
-by (res_inst_tac [("n","n")] natE 1);
-by (cut_facts_tac prems 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "Suc_pred";
-Addsimps [Suc_pred];
-
-goal Arith.thy "pred(n) <= (n::nat)";
-by (res_inst_tac [("n","n")] natE 1);
-by (ALLGOALS Asm_simp_tac);
-qed "pred_le";
-AddIffs [pred_le];
-
-goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
-by (simp_tac (simpset() addsplits [expand_nat_case]) 1);
-qed_spec_mp "pred_le_mono";
-
-goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
-by (exhaust_tac "n" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "pred_less";
-Addsimps [pred_less];
(** Difference **)
-qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
+qed_goal "diff_0_eq_0" Arith.thy
"0 - n = 0"
(fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
(*Must simplify BEFORE the induction!! (Else we get a critical pair)
Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *)
-qed_goalw "diff_Suc_Suc" Arith.thy [pred_def]
+qed_goal "diff_Suc_Suc" Arith.thy
"Suc(m) - Suc(n) = m - n"
(fn _ =>
[Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
Addsimps [diff_0_eq_0, diff_Suc_Suc];
+(* Could be (and is, below) generalized in various ways;
+ However, none of the generalizations are currently in the simpset,
+ and I dread to think what happens if I put them in *)
+goal Arith.thy "!!n. 0 < n ==> Suc(n-1) = n";
+by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
+qed "Suc_pred";
+Addsimps [Suc_pred];
+
+(* Generalize? *)
+goal Arith.thy "!!n. 0<n ==> n-1 < n";
+by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
+qed "pred_less";
+Addsimps [pred_less];
+
+Delsimps [diff_Suc];
+
(**** Inductive properties of the operators ****)
@@ -120,17 +102,25 @@
by (induct_tac "m" 1);
by (ALLGOALS Asm_simp_tac);
qed "add_is_0";
-Addsimps [add_is_0];
+AddIffs [add_is_0];
-goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
-by (induct_tac "m" 1);
+goal Arith.thy "(0<m+n) = (0<m | 0<n)";
+by(simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
+qed "add_gr_0";
+AddIffs [add_gr_0];
+
+(* FIXME: really needed?? *)
+goal Arith.thy "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)";
+by (exhaust_tac "m" 1);
by (ALLGOALS (fast_tac (claset() addss (simpset()))));
qed "pred_add_is_0";
Addsimps [pred_add_is_0];
+(* Could be generalized, eg to "!!n. k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
+by (exhaust_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
+ addsplits [expand_nat_case])));
qed "add_pred";
Addsimps [add_pred];
@@ -336,9 +326,6 @@
(*** Difference ***)
-qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n"
- (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
-Addsimps [pred_Suc_diff];
qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
@@ -359,7 +346,6 @@
qed "le_add_diff_inverse2";
Addsimps [le_add_diff_inverse, le_add_diff_inverse2];
-Delsimps [diff_Suc];
(*** More results about difference ***)
@@ -387,6 +373,14 @@
by (ALLGOALS Asm_simp_tac);
qed "diff_diff_left";
+(* This is a trivial consequence of diff_diff_left;
+ could be got rid of if diff_diff_left were in the simpset...
+*)
+goal Arith.thy "(Suc m - n)-1 = m - n";
+by(simp_tac (simpset() addsimps [diff_diff_left]) 1);
+qed "pred_Suc_diff";
+Addsimps [pred_Suc_diff];
+
(*This and the next few suggested by Florian Kammueller*)
goal Arith.thy "!!i::nat. i-j-k = i-k-j";
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
@@ -654,7 +648,7 @@
by (atac 1);
by (etac le_trans 1);
by (res_inst_tac [("m1","n")] (pred_Suc_diff RS subst) 1);
-by (rtac pred_le 1);
+by (simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
qed_spec_mp "diff_le_mono";
goal Arith.thy "!!n::nat. m<=n ==> (l-n) <= (l-m)";
--- a/src/HOL/Arith.thy Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Arith.thy Thu Dec 04 12:44:37 1997 +0100
@@ -11,13 +11,8 @@
instance
nat :: {plus, minus, times, power}
-consts
- pred :: nat => nat
- (* size of a datatype value; overloaded *)
- size :: 'a => nat
-
-defs
- pred_def "pred(m) == case m of 0 => 0 | Suc n => n"
+(* size of a datatype value; overloaded *)
+consts size :: 'a => nat
primrec "op +" nat
add_0 "0 + n = n"
@@ -25,7 +20,10 @@
primrec "op -" nat
diff_0 "m - 0 = m"
- diff_Suc "m - Suc n = pred(m - n)"
+ diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+
+syntax pred :: nat => nat
+translations "pred m" => "m - 1"
primrec "op *" nat
mult_0 "0 * n = 0"
--- a/src/HOL/Lambda/Eta.ML Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Lambda/Eta.ML Thu Dec 04 12:44:37 1997 +0100
@@ -33,11 +33,11 @@
Addsimps [subst_not_free RS eqTrueI];
goal Eta.thy "!i k. free (lift t k) i = \
-\ (i < k & free t i | k < i & free t (pred i))";
+\ (i < k & free t i | k < i & free t (i-1))";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
by (Blast_tac 2);
-by (simp_tac (simpset() addsimps [pred_def] addsplits [expand_nat_case]) 1);
+by (simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed "free_lift";
@@ -49,7 +49,7 @@
by (Asm_simp_tac 2);
by (Blast_tac 2);
by (asm_full_simp_tac (addsplit (simpset())) 2);
-by (simp_tac (simpset() addsimps [pred_def,subst_Var]
+by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
addsplits [expand_if,expand_nat_case]) 1);
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
@@ -173,7 +173,7 @@
by (etac nat_neqE 1);
by (res_inst_tac [("x","Var nat")] exI 1);
by (Asm_simp_tac 1);
- by (res_inst_tac [("x","Var(pred nat)")] exI 1);
+ by (res_inst_tac [("x","Var(nat-1)")] exI 1);
by (Asm_simp_tac 1);
by (rtac notE 1);
by (assume_tac 2);
--- a/src/HOL/Lambda/Lambda.ML Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Lambda/Lambda.ML Thu Dec 04 12:44:37 1997 +0100
@@ -52,7 +52,7 @@
by (asm_full_simp_tac(addsplit(simpset())) 1);
qed "subst_eq";
-goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)";
+goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(j-1)";
by (asm_full_simp_tac(addsplit(simpset())) 1);
qed "subst_gt";
@@ -75,7 +75,7 @@
goal Lambda.thy "!i j s. j < Suc i --> \
\ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
by (dB.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [pred_def,subst_Var,lift_lift]
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
addsplits [expand_if,expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
@@ -105,7 +105,7 @@
\ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac
- (simpset() addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
+ (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
addsplits [expand_if,expand_nat_case]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
--- a/src/HOL/Lambda/Lambda.thy Thu Dec 04 09:05:59 1997 +0100
+++ b/src/HOL/Lambda/Lambda.thy Thu Dec 04 12:44:37 1997 +0100
@@ -24,7 +24,7 @@
"lift (Abs s) k = Abs(lift s (Suc k))"
primrec subst dB
- subst_Var "(Var i)[s/k] = (if k < i then Var(pred i)
+ subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
else if i = k then s else Var i)"
subst_App "(t @ u)[s/k] = t[s/k] @ u[s/k]"
subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
@@ -35,7 +35,7 @@
"liftn n (Abs s) k = Abs(liftn n s (Suc k))"
primrec substn dB
- "substn (Var i) s k = (if k < i then Var(pred i)
+ "substn (Var i) s k = (if k < i then Var(i-1)
else if i = k then liftn k s 0 else Var i)"
"substn (t @ u) s k = (substn t s k) @ (substn u s k)"
"substn (Abs t) s k = Abs (substn t s (Suc k))"