10 header {* Basic Definitions for Binary Integers *} |
10 header {* Basic Definitions for Binary Integers *} |
11 |
11 |
12 theory BinGeneral imports Num_Lemmas |
12 theory BinGeneral imports Num_Lemmas |
13 |
13 |
14 begin |
14 begin |
|
15 |
|
16 subsection {* BIT as a datatype constructor *} |
|
17 |
|
18 constdefs |
|
19 -- "alternative way of defining @{text bin_last}, @{text bin_rest}" |
|
20 bin_rl :: "int => int * bit" |
|
21 "bin_rl w == SOME (r, l). w = r BIT l" |
|
22 |
|
23 (** ways in which type Bin resembles a datatype **) |
|
24 |
|
25 lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c" |
|
26 apply (unfold Bit_def) |
|
27 apply (simp (no_asm_use) split: bit.split_asm) |
|
28 apply simp_all |
|
29 apply (drule_tac f=even in arg_cong, clarsimp)+ |
|
30 done |
|
31 |
|
32 lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard] |
|
33 |
|
34 lemma BIT_eq_iff [simp]: |
|
35 "(u BIT b = v BIT c) = (u = v \<and> b = c)" |
|
36 by (rule iffI) auto |
|
37 |
|
38 lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]] |
|
39 |
|
40 lemma less_Bits: |
|
41 "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)" |
|
42 unfolding Bit_def by (auto split: bit.split) |
|
43 |
|
44 lemma le_Bits: |
|
45 "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))" |
|
46 unfolding Bit_def by (auto split: bit.split) |
|
47 |
|
48 lemma neB1E [elim!]: |
|
49 assumes ne: "y \<noteq> bit.B1" |
|
50 assumes y: "y = bit.B0 \<Longrightarrow> P" |
|
51 shows "P" |
|
52 apply (rule y) |
|
53 apply (cases y rule: bit.exhaust, simp) |
|
54 apply (simp add: ne) |
|
55 done |
|
56 |
|
57 lemma bin_ex_rl: "EX w b. w BIT b = bin" |
|
58 apply (unfold Bit_def) |
|
59 apply (cases "even bin") |
|
60 apply (clarsimp simp: even_equiv_def) |
|
61 apply (auto simp: odd_equiv_def split: bit.split) |
|
62 done |
|
63 |
|
64 lemma bin_exhaust: |
|
65 assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q" |
|
66 shows "Q" |
|
67 apply (insert bin_ex_rl [of bin]) |
|
68 apply (erule exE)+ |
|
69 apply (rule Q) |
|
70 apply force |
|
71 done |
|
72 |
|
73 lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)" |
|
74 apply (unfold bin_rl_def) |
|
75 apply safe |
|
76 apply (cases w rule: bin_exhaust) |
|
77 apply auto |
|
78 done |
|
79 |
|
80 lemmas bin_rl_simps [THEN bin_rl_char [THEN iffD2], standard, simp] = |
|
81 Pls_0_eq Min_1_eq refl |
|
82 |
|
83 lemma bin_abs_lem: |
|
84 "bin = (w BIT b) ==> ~ bin = Numeral.Min --> ~ bin = Numeral.Pls --> |
|
85 nat (abs w) < nat (abs bin)" |
|
86 apply (clarsimp simp add: bin_rl_char) |
|
87 apply (unfold Pls_def Min_def Bit_def) |
|
88 apply (cases b) |
|
89 apply (clarsimp, arith) |
|
90 apply (clarsimp, arith) |
|
91 done |
|
92 |
|
93 lemma bin_induct: |
|
94 assumes PPls: "P Numeral.Pls" |
|
95 and PMin: "P Numeral.Min" |
|
96 and PBit: "!!bin bit. P bin ==> P (bin BIT bit)" |
|
97 shows "P bin" |
|
98 apply (rule_tac P=P and a=bin and f1="nat o abs" |
|
99 in wf_measure [THEN wf_induct]) |
|
100 apply (simp add: measure_def inv_image_def) |
|
101 apply (case_tac x rule: bin_exhaust) |
|
102 apply (frule bin_abs_lem) |
|
103 apply (auto simp add : PPls PMin PBit) |
|
104 done |
15 |
105 |
16 subsection {* Recursion combinator for binary integers *} |
106 subsection {* Recursion combinator for binary integers *} |
17 |
107 |
18 lemma brlem: "(bin = Numeral.Min) = (- bin + Numeral.pred 0 = 0)" |
108 lemma brlem: "(bin = Numeral.Min) = (- bin + Numeral.pred 0 = 0)" |
19 unfolding Min_def pred_def by arith |
109 unfolding Min_def pred_def by arith |