author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 21404  eb85850d3eb7 
child 29751  e2756594c414 
permissions  rwrr 
1246  1 
(* Title: FOL/ex/NatClass.thy 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 
*) 

5 

17245  6 
theory NatClass 
7 
imports FOL 

8 
begin 

9 

10 
text {* 

11 
This is an abstract version of theory @{text "Nat"}. Instead of 

12 
axiomatizing a single type @{text nat} we define the class of all 

13 
these types (up to isomorphism). 

14 

15 
Note: The @{text rec} operator had to be made \emph{monomorphic}, 

16 
because class axioms may not contain more than one type variable. 

17 
*} 

1246  18 

19 
consts 

17245  20 
0 :: 'a ("0") 
21 
Suc :: "'a => 'a" 

22 
rec :: "['a, 'a, ['a, 'a] => 'a] => 'a" 

1246  23 

24 
axclass 

17245  25 
nat < "term" 
26 
induct: "[ P(0); !!x. P(x) ==> P(Suc(x)) ] ==> P(n)" 

27 
Suc_inject: "Suc(m) = Suc(n) ==> m = n" 

28 
Suc_neq_0: "Suc(m) = 0 ==> R" 

29 
rec_0: "rec(0, a, f) = a" 

30 
rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" 

1246  31 

19819  32 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19819
diff
changeset

33 
add :: "['a::nat, 'a] => 'a" (infixl "+" 60) where 
19819  34 
"m + n = rec(m, n, %x y. Suc(y))" 
35 

36 
lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)" 

37 
apply (rule_tac n = k in induct) 

38 
apply (rule notI) 

39 
apply (erule Suc_neq_0) 

40 
apply (rule notI) 

41 
apply (erule notE) 

42 
apply (erule Suc_inject) 

43 
done 

44 

45 
lemma "(k+m)+n = k+(m+n)" 

46 
apply (rule induct) 

47 
back 

48 
back 

49 
back 

50 
back 

51 
back 

52 
back 

53 
oops 

54 

55 
lemma add_0 [simp]: "0+n = n" 

56 
apply (unfold add_def) 

57 
apply (rule rec_0) 

58 
done 

1246  59 

19819  60 
lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" 
61 
apply (unfold add_def) 

62 
apply (rule rec_Suc) 

63 
done 

64 

65 
lemma add_assoc: "(k+m)+n = k+(m+n)" 

66 
apply (rule_tac n = k in induct) 

67 
apply simp 

68 
apply simp 

69 
done 

70 

71 
lemma add_0_right: "m+0 = m" 

72 
apply (rule_tac n = m in induct) 

73 
apply simp 

74 
apply simp 

75 
done 

76 

77 
lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" 

78 
apply (rule_tac n = m in induct) 

79 
apply simp_all 

80 
done 

81 

82 
lemma 

83 
assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" 

84 
shows "f(i+j) = i+f(j)" 

85 
apply (rule_tac n = i in induct) 

86 
apply simp 

87 
apply (simp add: prem) 

88 
done 

1246  89 

90 
end 