# HG changeset patch # User nipkow # Date 881235877 -3600 # Node ID 40e5c97e988d575d81593316a91e0564b66b4d19 # Parent 6f2986464280b66be6857ef5f02f8cc7891e5878 pred n -> n-1 diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Arith.ML --- 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-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-(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)"; diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Arith.thy --- 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" diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Lambda/Eta.ML --- 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); diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Lambda/Lambda.ML --- 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 (Var j)[u/i] = Var(pred j)"; +goal Lambda.thy "!!s. i (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])); diff -r 6f2986464280 -r 40e5c97e988d src/HOL/Lambda/Lambda.thy --- 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))"