equal
deleted
inserted
replaced
67 lemma Let_1 [simp]: "Let 1 f == f 1" |
67 lemma Let_1 [simp]: "Let 1 f == f 1" |
68 by (simp add: Let_def) |
68 by (simp add: Let_def) |
69 |
69 |
70 |
70 |
71 consts |
71 consts |
72 ring_of :: "bin => 'a::ring" |
|
73 |
|
74 NCons :: "[bin,bool]=>bin" |
72 NCons :: "[bin,bool]=>bin" |
75 bin_succ :: "bin=>bin" |
73 bin_succ :: "bin=>bin" |
76 bin_pred :: "bin=>bin" |
74 bin_pred :: "bin=>bin" |
77 bin_minus :: "bin=>bin" |
75 bin_minus :: "bin=>bin" |
78 bin_add :: "[bin,bin]=>bin" |
76 bin_add :: "[bin,bin]=>bin" |
82 primrec |
80 primrec |
83 NCons_Pls: "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)" |
81 NCons_Pls: "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)" |
84 NCons_Min: "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))" |
82 NCons_Min: "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))" |
85 NCons_BIT: "NCons (w BIT x) b = (w BIT x) BIT b" |
83 NCons_BIT: "NCons (w BIT x) b = (w BIT x) BIT b" |
86 |
84 |
87 |
|
88 primrec |
|
89 ring_of_Pls: "ring_of bin.Pls = 0" |
|
90 ring_of_Min: "ring_of bin.Min = - (1::'a::ring)" |
|
91 ring_of_BIT: "ring_of(w BIT x) = (if x then 1 else 0) + |
|
92 (ring_of w) + (ring_of w)" |
|
93 |
85 |
94 primrec |
86 primrec |
95 bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True" |
87 bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True" |
96 bin_succ_Min: "bin_succ bin.Min = bin.Pls" |
88 bin_succ_Min: "bin_succ bin.Min = bin.Pls" |
97 bin_succ_BIT: "bin_succ(w BIT x) = |
89 bin_succ_BIT: "bin_succ(w BIT x) = |