equal
deleted
inserted
replaced
24 Goal "n ~= 0 ==> EX m. n = Suc m"; |
24 Goal "n ~= 0 ==> EX m. n = Suc m"; |
25 by (case_tac "n" 1); |
25 by (case_tac "n" 1); |
26 by (REPEAT (Blast_tac 1)); |
26 by (REPEAT (Blast_tac 1)); |
27 qed "not0_implies_Suc"; |
27 qed "not0_implies_Suc"; |
28 |
28 |
29 Goal "m<n ==> n ~= 0"; |
29 Goal "!!n::nat. m<n ==> n ~= 0"; |
30 by (case_tac "n" 1); |
30 by (case_tac "n" 1); |
31 by (ALLGOALS Asm_full_simp_tac); |
31 by (ALLGOALS Asm_full_simp_tac); |
32 qed "gr_implies_not0"; |
32 qed "gr_implies_not0"; |
33 |
33 |
34 Goal "(n ~= 0) = (0 < n)"; |
34 Goal "!!n::nat. (n ~= 0) = (0 < n)"; |
35 by (case_tac "n" 1); |
35 by (case_tac "n" 1); |
36 by Auto_tac; |
36 by Auto_tac; |
37 qed "neq0_conv"; |
37 qed "neq0_conv"; |
38 AddIffs [neq0_conv]; |
38 AddIffs [neq0_conv]; |
39 |
39 |
40 Goal "(0 ~= n) = (0 < n)"; |
40 Goal "!!n::nat. (0 ~= n) = (0 < n)"; |
41 by (case_tac "n" 1); |
41 by (case_tac "n" 1); |
42 by Auto_tac; |
42 by Auto_tac; |
43 qed "zero_neq_conv"; |
43 qed "zero_neq_conv"; |
44 AddIffs [zero_neq_conv]; |
44 AddIffs [zero_neq_conv]; |
45 |
45 |
48 |
48 |
49 Goal "(0<n) = (EX m. n = Suc m)"; |
49 Goal "(0<n) = (EX m. n = Suc m)"; |
50 by(fast_tac (claset() addIs [not0_implies_Suc]) 1); |
50 by(fast_tac (claset() addIs [not0_implies_Suc]) 1); |
51 qed "gr0_conv_Suc"; |
51 qed "gr0_conv_Suc"; |
52 |
52 |
53 Goal "(~(0 < n)) = (n=0)"; |
53 Goal "!!n::nat. (~(0 < n)) = (n=0)"; |
54 by (rtac iffI 1); |
54 by (rtac iffI 1); |
55 by (etac swap 1); |
55 by (etac swap 1); |
56 by (ALLGOALS Asm_full_simp_tac); |
56 by (ALLGOALS Asm_full_simp_tac); |
57 qed "not_gr0"; |
57 qed "not_gr0"; |
58 AddIffs [not_gr0]; |
58 AddIffs [not_gr0]; |
93 by (case_tac "n" 1); |
93 by (case_tac "n" 1); |
94 by (case_tac "nat" 2); |
94 by (case_tac "nat" 2); |
95 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans]))); |
95 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans]))); |
96 qed "nat_induct2"; |
96 qed "nat_induct2"; |
97 |
97 |
98 Goal "min 0 n = 0"; |
98 Goal "min 0 n = (0::nat)"; |
99 by (rtac min_leastL 1); |
99 by (rtac min_leastL 1); |
100 by (Simp_tac 1); |
100 by (Simp_tac 1); |
101 qed "min_0L"; |
101 qed "min_0L"; |
102 |
102 |
103 Goal "min n 0 = 0"; |
103 Goal "min n 0 = (0::nat)"; |
104 by (rtac min_leastR 1); |
104 by (rtac min_leastR 1); |
105 by (Simp_tac 1); |
105 by (Simp_tac 1); |
106 qed "min_0R"; |
106 qed "min_0R"; |
107 |
107 |
108 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)"; |
108 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)"; |
109 by (Simp_tac 1); |
109 by (Simp_tac 1); |
110 qed "min_Suc_Suc"; |
110 qed "min_Suc_Suc"; |
111 |
111 |
112 Addsimps [min_0L,min_0R,min_Suc_Suc]; |
112 Addsimps [min_0L,min_0R,min_Suc_Suc]; |
113 |
113 |
114 Goalw [max_def] "max 0 n = n"; |
114 Goalw [max_def] "max 0 n = (n::nat)"; |
115 by (Simp_tac 1); |
115 by (Simp_tac 1); |
116 qed "max_0L"; |
116 qed "max_0L"; |
117 |
117 |
118 Goalw [max_def] "max n 0 = n"; |
118 Goalw [max_def] "max n 0 = (n::nat)"; |
119 by (Simp_tac 1); |
119 by (Simp_tac 1); |
120 qed "max_0R"; |
120 qed "max_0R"; |
121 |
121 |
122 Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)"; |
122 Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)"; |
123 by (Simp_tac 1); |
123 by (Simp_tac 1); |