30 |
30 |
31 Addsimps [less_not_sym RS True_eq]; |
31 Addsimps [less_not_sym RS True_eq]; |
32 |
32 |
33 goal Arith.thy "i < j --> pred i < j"; |
33 goal Arith.thy "i < j --> pred i < j"; |
34 by(nat_ind_tac "j" 1); |
34 by(nat_ind_tac "j" 1); |
35 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
35 by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq]))); |
36 by(nat_ind_tac "j1" 1); |
36 by(nat_ind_tac "j1" 1); |
37 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
37 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
38 qed_spec_mp "less_imp_pred_less"; |
38 qed_spec_mp "less_imp_pred_less"; |
39 |
39 |
40 goal Arith.thy "i<j --> ~ pred j < i"; |
40 goal Arith.thy "i<j --> ~ pred j < i"; |
41 by(nat_ind_tac "j" 1); |
41 by(nat_ind_tac "j" 1); |
42 by(ALLGOALS(asm_simp_tac(simpset_of "Arith"))); |
42 by(ALLGOALS(asm_simp_tac(simpset_of "Arith" addsimps [less_Suc_eq]))); |
43 by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1); |
43 by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1); |
44 qed_spec_mp "less_imp_not_pred_less"; |
44 qed_spec_mp "less_imp_not_pred_less"; |
45 Addsimps [less_imp_not_pred_less]; |
45 Addsimps [less_imp_not_pred_less]; |
46 |
46 |
47 goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i"; |
47 goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i"; |
48 by(nat_ind_tac "j" 1); |
48 by(nat_ind_tac "j" 1); |
49 by(ALLGOALS(simp_tac(simpset_of "Nat"))); |
49 by(ALLGOALS(simp_tac(simpset_of "Nat"))); |
|
50 by(simp_tac(simpset_of "Nat" addsimps [less_Suc_eq])1); |
50 by(fast_tac (HOL_cs addDs [less_not_sym]) 1); |
51 by(fast_tac (HOL_cs addDs [less_not_sym]) 1); |
51 qed_spec_mp "less_interval1"; |
52 qed_spec_mp "less_interval1"; |
52 |
53 |
53 |
54 |
54 (*** decr and free ***) |
55 (*** decr and free ***) |
177 qed "decr_Fun"; |
178 qed "decr_Fun"; |
178 Addsimps [decr_Fun]; |
179 Addsimps [decr_Fun]; |
179 |
180 |
180 goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)"; |
181 goal Eta.thy "!i. ~free t (Suc i) --> decr t i = decr t (Suc i)"; |
181 by(db.induct_tac "t" 1); |
182 by(db.induct_tac "t" 1); |
182 by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def]))); |
183 by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [le_def, less_Suc_eq]))); |
183 by(fast_tac (HOL_cs addDs [less_interval1]) 1); |
|
184 by(fast_tac HOL_cs 1); |
184 by(fast_tac HOL_cs 1); |
185 qed "decr_not_free"; |
185 qed "decr_not_free"; |
186 Addsimps [decr_not_free]; |
186 Addsimps [decr_not_free]; |
187 |
187 |
188 goal Eta.thy "!s t. s -e> t --> (!i. lift s i -e> lift t i)"; |
188 goal Eta.thy "!s t. s -e> t --> (!i. lift s i -e> lift t i)"; |