author  oheimb 
Fri, 18 Feb 2000 20:24:56 +0100  
changeset 8260  87f21e25fcb6 
parent 8115  c802042066e8 
child 8423  3c19160b6432 
permissions  rwrr 
2441  1 
(* Title: HOL/Nat.ML 
923  2 
ID: $Id$ 
2608  3 
Author: Tobias Nipkow 
4 
Copyright 1997 TU Muenchen 

923  5 
*) 
6 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

7 
(** conversion rules for nat_rec **) 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

8 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

9 
val [nat_rec_0, nat_rec_Suc] = nat.recs; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

10 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

11 
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) 
5316  12 
val prems = Goal 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

13 
"[ !!n. f(n) == nat_rec c h n ] ==> f(0) = c"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

14 
by (simp_tac (simpset() addsimps prems) 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

15 
qed "def_nat_rec_0"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

16 

5316  17 
val prems = Goal 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

18 
"[ !!n. f(n) == nat_rec c h n ] ==> f(Suc(n)) = h n (f n)"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

19 
by (simp_tac (simpset() addsimps prems) 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

20 
qed "def_nat_rec_Suc"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

21 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

22 
val [nat_case_0, nat_case_Suc] = nat.cases; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

23 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

24 
Goal "n ~= 0 ==> EX m. n = Suc m"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

25 
by (exhaust_tac "n" 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

26 
by (REPEAT (Blast_tac 1)); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

27 
qed "not0_implies_Suc"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

28 

5316  29 
Goal "m<n ==> n ~= 0"; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

30 
by (exhaust_tac "n" 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

31 
by (ALLGOALS Asm_full_simp_tac); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

32 
qed "gr_implies_not0"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

33 

633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

34 
Goal "(n ~= 0) = (0 < n)"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

35 
by (exhaust_tac "n" 1); 
7089  36 
by Auto_tac; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

37 
qed "neq0_conv"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

38 
AddIffs [neq0_conv]; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

39 

5644  40 
Goal "(0 ~= n) = (0 < n)"; 
6301  41 
by (exhaust_tac "n" 1); 
7089  42 
by Auto_tac; 
5644  43 
qed "zero_neq_conv"; 
44 
AddIffs [zero_neq_conv]; 

45 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

46 
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *) 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

47 
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

48 

8115  49 
Goal "(0<n) = (EX m. n = Suc m)"; 
50 
by(fast_tac (claset() addIs [not0_implies_Suc]) 1); 

51 
qed "gr0_conv_Suc"; 

52 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

53 
Goal "(~(0 < n)) = (n=0)"; 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

54 
by (rtac iffI 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

55 
by (etac swap 1); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

56 
by (ALLGOALS Asm_full_simp_tac); 
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

57 
qed "not_gr0"; 
6109  58 
AddIffs [not_gr0]; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

59 

8260  60 
Goal "(Suc n <= m') > (? m. m' = Suc m)"; 
61 
by (induct_tac "m'" 1); 

62 
by Auto_tac; 

63 
qed_spec_mp "Suc_le_D"; 

64 

6805  65 
(*Useful in certain inductive arguments*) 
66 
Goal "(m < Suc n) = (m=0  (EX j. m = Suc j & j < n))"; 

67 
by (exhaust_tac "m" 1); 

68 
by Auto_tac; 

69 
qed "less_Suc_eq_0_disj"; 

70 

7058  71 
Goalw [Least_nat_def] 
72 
"[ ? n. P(Suc n); ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"; 

73 
by (rtac select_equality 1); 

74 
by (fold_goals_tac [Least_nat_def]); 

75 
by (safe_tac (claset() addSEs [LeastI])); 

76 
by (rename_tac "j" 1); 

77 
by (exhaust_tac "j" 1); 

78 
by (Blast_tac 1); 

79 
by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1); 

80 
by (rename_tac "k n" 1); 

81 
by (exhaust_tac "k" 1); 

82 
by (Blast_tac 1); 

83 
by (hyp_subst_tac 1); 

84 
by (rewtac Least_nat_def); 

85 
by (rtac (select_equality RS arg_cong RS sym) 1); 

7089  86 
by (blast_tac (claset() addDs [Suc_mono]) 1); 
87 
by (cut_inst_tac [("m","m")] less_linear 1); 

88 
by (blast_tac (claset() addIs [Suc_mono]) 1); 

7058  89 
qed "Least_Suc"; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

90 

7058  91 
val prems = Goal "[ P 0; P 1; !!k. P k ==> P (Suc (Suc k)) ] ==> P n"; 
92 
by (rtac less_induct 1); 

93 
by (exhaust_tac "n" 1); 

7089  94 
by (exhaust_tac "nat" 2); 
95 
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans]))); 

7058  96 
qed "nat_induct2"; 
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
5069
diff
changeset

97 

5069  98 
Goal "min 0 n = 0"; 
3023  99 
by (rtac min_leastL 1); 
5983  100 
by (Simp_tac 1); 
2608  101 
qed "min_0L"; 
1301  102 

5069  103 
Goal "min n 0 = 0"; 
3023  104 
by (rtac min_leastR 1); 
5983  105 
by (Simp_tac 1); 
2608  106 
qed "min_0R"; 
923  107 

5069  108 
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)"; 
3023  109 
by (Simp_tac 1); 
2608  110 
qed "min_Suc_Suc"; 
1660  111 

2608  112 
Addsimps [min_0L,min_0R,min_Suc_Suc]; 
6433  113 

114 
Goalw [max_def] "max 0 n = n"; 

115 
by (Simp_tac 1); 

116 
qed "max_0L"; 

117 

118 
Goalw [max_def] "max n 0 = n"; 

119 
by (Simp_tac 1); 

120 
qed "max_0R"; 

121 

122 
Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)"; 

123 
by (Simp_tac 1); 

124 
qed "max_Suc_Suc"; 

125 

126 
Addsimps [max_0L,max_0R,max_Suc_Suc]; 