author  huffman 
Sun, 25 Mar 2012 20:15:39 +0200  
changeset 47108  2a1953f0d20d 
parent 45701  615da8b8d758 
child 49834  b27bbb021df1 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Bit.thy 
2 
Author: Brian Huffman 

29994
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 

45701  28 
rep_datatype "0::bit" "1::bit" 
29994
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 

36409  52 
instantiation bit :: field_inverse_zero 
29994
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: 
31212  56 
"x + y = bit_case y (bit_case 1 0 y) x" 
29994
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: 
31212  59 
"x * y = bit_case 0 y x" 
29994
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 
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

100 

29995  101 
lemma bit_minus1 [simp]: "1 = (1 :: bit)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

102 
by (simp only: minus_one [symmetric] uminus_bit_def) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

103 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

104 
lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

105 
by (simp only: neg_numeral_def uminus_bit_def) 
29995  106 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

107 
lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

108 
by (simp only: numeral_Bit0 bit_add_self) 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
diff
changeset

109 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

110 
lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset

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

112 

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

113 
end 