# HG changeset patch # User pusch # Date 856879916 -3600 # Node ID 13cdbf95ed92797a408c15be7308f2eba08f3b30 # Parent 93ed51a916227ad4ddce723b2db0083b1fda0880 minor changes due to new primrec definitions for +,-,* diff -r 93ed51a91622 -r 13cdbf95ed92 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Tue Feb 25 15:11:12 1997 +0100 +++ b/src/HOL/Arith.ML Tue Feb 25 15:11:56 1997 +0100 @@ -19,13 +19,7 @@ by(Simp_tac 1); qed "pred_Suc"; -val [add_0,add_Suc] = nat_recs add_def; -val [mult_0,mult_Suc] = nat_recs mult_def; -store_thm("add_0",add_0); -store_thm("add_Suc",add_Suc); -store_thm("mult_0",mult_0); -store_thm("mult_Suc",mult_Suc); -Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc]; +Addsimps [pred_0,pred_Suc]; (** pred **) @@ -38,20 +32,18 @@ (** Difference **) -bind_thm("diff_0", diff_def RS def_nat_rec_0); - -qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def] +qed_goalw "diff_0_eq_0" Arith.thy [pred_def] "0 - n = 0" (fn _ => [nat_ind_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 [diff_def, pred_def] +qed_goalw "diff_Suc_Suc" Arith.thy [pred_def] "Suc(m) - Suc(n) = m - n" (fn _ => [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); -Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc]; +Addsimps [diff_0_eq_0, diff_Suc_Suc]; goal Arith.thy "!!k. 0 EX j. k = Suc(j)"; @@ -179,6 +171,10 @@ (*** Difference ***) +qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n" + (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); +Addsimps [pred_Suc_diff]; + qed_goal "diff_self_eq_0" Arith.thy "m - m = 0" (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); Addsimps [diff_self_eq_0];