author  huffman 
Thu, 26 Feb 2009 08:44:44 0800  
changeset 30129  419116f1157a 
parent 29995  62efbd0ef132 
child 31212  a94aea0cef76 
permissions  rwrr 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

1 
(* Title: Bit.thy 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

2 
Author: Brian Huffman 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

3 
*) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

4 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

5 
header {* The Field of Integers mod 2 *} 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

6 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

7 
theory Bit 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

8 
imports Main 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

9 
begin 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

10 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

11 
subsection {* Bits as a datatype *} 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

12 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

13 
typedef (open) bit = "UNIV :: bool set" .. 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

14 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

15 
instantiation bit :: "{zero, one}" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

16 
begin 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

17 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

18 
definition zero_bit_def: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

19 
"0 = Abs_bit False" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

20 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

21 
definition one_bit_def: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

22 
"1 = Abs_bit True" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

23 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

24 
instance .. 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

25 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

26 
end 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

27 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

28 
rep_datatype (bit) "0::bit" "1::bit" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

29 
proof  
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

30 
fix P and x :: bit 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

31 
assume "P (0::bit)" and "P (1::bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

32 
then have "\<forall>b. P (Abs_bit b)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

33 
unfolding zero_bit_def one_bit_def 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

34 
by (simp add: all_bool_eq) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

35 
then show "P x" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

36 
by (induct x) simp 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

37 
next 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

38 
show "(0::bit) \<noteq> (1::bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

39 
unfolding zero_bit_def one_bit_def 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

40 
by (simp add: Abs_bit_inject) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

41 
qed 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

42 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

43 
lemma bit_not_0_iff [iff]: "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

44 
by (induct x) simp_all 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

45 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

46 
lemma bit_not_1_iff [iff]: "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

47 
by (induct x) simp_all 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

48 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

49 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

50 
subsection {* Type @{typ bit} forms a field *} 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

51 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

52 
instantiation bit :: "{field, division_by_zero}" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

53 
begin 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

54 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

55 
definition plus_bit_def: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

56 
"x + y = (case x of 0 \<Rightarrow> y  1 \<Rightarrow> (case y of 0 \<Rightarrow> 1  1 \<Rightarrow> 0))" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

57 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

58 
definition times_bit_def: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

59 
"x * y = (case x of 0 \<Rightarrow> 0  1 \<Rightarrow> y)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

60 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

61 
definition uminus_bit_def [simp]: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

62 
" x = (x :: bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

63 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

64 
definition minus_bit_def [simp]: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

65 
"x  y = (x + y :: bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

66 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

67 
definition inverse_bit_def [simp]: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

68 
"inverse x = (x :: bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

69 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

70 
definition divide_bit_def [simp]: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

71 
"x / y = (x * y :: bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

72 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

73 
lemmas field_bit_defs = 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

74 
plus_bit_def times_bit_def minus_bit_def uminus_bit_def 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

75 
divide_bit_def inverse_bit_def 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

76 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

77 
instance proof 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

78 
qed (unfold field_bit_defs, auto split: bit.split) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

79 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

80 
end 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

81 

30129  82 
lemma bit_add_self: "x + x = (0 :: bit)" 
83 
unfolding plus_bit_def by (simp split: bit.split) 

29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

84 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

85 
lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

86 
unfolding times_bit_def by (simp split: bit.split) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

87 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

88 
text {* Not sure whether the next two should be simp rules. *} 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

89 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

90 
lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

91 
unfolding plus_bit_def by (simp split: bit.split) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

92 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

93 
lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

94 
unfolding plus_bit_def by (simp split: bit.split) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

95 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

96 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

97 
subsection {* Numerals at type @{typ bit} *} 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

98 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

99 
instantiation bit :: number_ring 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

100 
begin 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

101 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

102 
definition number_of_bit_def: 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

103 
"(number_of w :: bit) = of_int w" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

104 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

105 
instance proof 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

106 
qed (rule number_of_bit_def) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

107 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

108 
end 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

109 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

110 
text {* All numerals reduce to either 0 or 1. *} 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

111 

29995  112 
lemma bit_minus1 [simp]: "1 = (1 :: bit)" 
113 
by (simp only: number_of_Min uminus_bit_def) 

114 

29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

115 
lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

116 
by (simp only: number_of_Bit0 add_0_left bit_add_self) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

117 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

118 
lemma bit_number_of_odd [simp]: "number_of (Int.Bit1 w) = (1 :: bit)" 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

119 
by (simp only: number_of_Bit1 add_assoc bit_add_self 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

120 
monoid_add_class.add_0_right) 
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

121 

6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

122 
end 