--- a/src/HOL/Algebra/abstract/Ring2.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Wed Jan 02 15:14:02 2008 +0100
@@ -23,7 +23,7 @@
subsection {* Ring axioms *}
-axclass ring < zero, one, plus, minus, times, inverse, power, Divides.div
+axclass ring < zero, one, plus, minus, uminus, times, inverse, power, Divides.div
a_assoc: "(a + b) + c = a + (b + c)"
l_zero: "0 + a = a"
--- a/src/HOL/Algebra/poly/PolyHomo.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy Wed Jan 02 15:14:02 2008 +0100
@@ -181,6 +181,6 @@
"EVAL (y::'a::domain)
(EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
- by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
+ by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
end
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Jan 02 15:14:02 2008 +0100
@@ -77,32 +77,95 @@
text {* Ring operations *}
-instance up :: (zero) zero ..
-instance up :: (one) one ..
-instance up :: (plus) plus ..
-instance up :: (minus) minus ..
-instance up :: (times) times ..
-instance up :: (Divides.div) Divides.div ..
-instance up :: (inverse) inverse ..
-instance up :: (power) power ..
+instantiation up :: (zero) zero
+begin
+
+definition
+ up_zero_def: "0 = monom 0 0"
+
+instance ..
+
+end
+
+instantiation up :: ("{one, zero}") one
+begin
+
+definition
+ up_one_def: "1 = monom 1 0"
+
+instance ..
+
+end
+
+instantiation up :: ("{plus, zero}") plus
+begin
+
+definition
+ up_add_def: "p + q = Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
+
+instance ..
-defs
- up_add_def: "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)"
- up_mult_def: "p * q == Abs_UP (%n::nat. setsum
+end
+
+instantiation up :: ("{one, times, uminus, zero}") uminus
+begin
+
+definition
+ (* note: - 1 is different from -1; latter is of class number *)
+ up_uminus_def:"- p = (- 1) *s p"
+ (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
+
+instance ..
+
+end
+
+instantiation up :: ("{one, plus, times, minus, uminus, zero}") minus
+begin
+
+definition
+ up_minus_def: "(a :: 'a up) - b = a + (-b)"
+
+instance ..
+
+end
+
+instantiation up :: ("{times, comm_monoid_add}") times
+begin
+
+definition
+ up_mult_def: "p * q = Abs_UP (%n::nat. setsum
(%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
- up_zero_def: "0 == monom 0 0"
- up_one_def: "1 == monom 1 0"
- up_uminus_def:"- p == (- 1) *s p"
- (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *)
- (* note: - 1 is different from -1; latter is of class number *)
+
+instance ..
+
+end
+
+instance up :: (type) Divides.div ..
+
+instantiation up :: ("{times, one, comm_monoid_add}") inverse
+begin
+
+definition
+ up_inverse_def: "inverse (a :: 'a up) = (if a dvd 1 then
+ THE x. a * x = 1 else 0)"
- up_minus_def: "(a::'a::{plus, minus} up) - b == a + (-b)"
- up_inverse_def: "inverse (a::'a::{zero, one, Divides.div, inverse} up) ==
- (if a dvd 1 then THE x. a*x = 1 else 0)"
- up_divide_def: "(a::'a::{times, inverse} up) / b == a * inverse b"
- up_power_def: "(a::'a::{one, times, power} up) ^ n ==
- nat_rec 1 (%u b. b * a) n"
+definition
+ up_divide_def: "(a :: 'a up) / b = a * inverse b"
+
+instance ..
+
+end
+instantiation up :: ("{times, one, comm_monoid_add}") power
+begin
+
+primrec power_up where
+ "(a \<Colon> 'a up) ^ 0 = 1"
+ | "(a \<Colon> 'a up) ^ Suc n = a ^ n * a"
+
+instance ..
+
+end
subsection {* Effect of operations on coefficients *}
@@ -294,7 +357,7 @@
by (simp add: up_divide_def)
fix n
show "p ^ n = nat_rec 1 (%u b. b * p) n"
- by (simp add: up_power_def)
+ by (induct n) simp_all
qed
(* Further properties of monom *)
--- a/src/HOL/HOL.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/HOL.thy Wed Jan 02 15:14:02 2008 +0100
@@ -221,8 +221,10 @@
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
class minus = type +
+ fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
+
+class uminus = type +
fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
- and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
class times = type +
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
--- a/src/HOL/Hyperreal/StarDef.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Hyperreal/StarDef.thy Wed Jan 02 15:14:02 2008 +0100
@@ -469,12 +469,19 @@
end
-instantiation star :: (minus) minus
+instantiation star :: (uminus) uminus
begin
definition
star_minus_def: "uminus \<equiv> *f* uminus"
+instance ..
+
+end
+
+instantiation star :: (minus) minus
+begin
+
definition
star_diff_def: "(op -) \<equiv> *f2* (op -)"
--- a/src/HOL/Import/HOL/realax.imp Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Import/HOL/realax.imp Wed Jan 02 15:14:02 2008 +0100
@@ -27,7 +27,7 @@
"treal_add" > "HOL4Real.realax.treal_add"
"treal_1" > "HOL4Real.realax.treal_1"
"treal_0" > "HOL4Real.realax.treal_0"
- "real_neg" > "HOL.minus_class.uminus" :: "real => real"
+ "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
"real_mul" > "HOL.times_class.times" :: "real => real => real"
"real_lt" > "HOL.ord_class.less" :: "real => real => bool"
"real_add" > "HOL.plus_class.plus" :: "real => real => real"
--- a/src/HOL/IntDef.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/IntDef.thy Wed Jan 02 15:14:02 2008 +0100
@@ -22,7 +22,7 @@
int = "UNIV//intrel"
by (auto simp add: quotient_def)
-instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}"
+instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
begin
definition
--- a/src/HOL/OrderedGroup.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/OrderedGroup.thy Wed Jan 02 15:14:02 2008 +0100
@@ -121,7 +121,7 @@
subsection {* Groups *}
-class group_add = minus + monoid_add +
+class group_add = minus + uminus + monoid_add +
assumes left_minus [simp]: "- a + a = 0"
assumes diff_minus: "a - b = a + (- b)"
begin
@@ -219,7 +219,7 @@
end
-class ab_group_add = minus + comm_monoid_add +
+class ab_group_add = minus + uminus + comm_monoid_add +
assumes ab_left_minus: "- a + a = 0"
assumes ab_diff_minus: "a - b = a + (- b)"
begin
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Wed Jan 02 15:14:02 2008 +0100
@@ -104,7 +104,7 @@
definition
norm_pres_extensions ::
- "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
+ "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
\<Rightarrow> 'a graph set" where
"norm_pres_extensions E p F f
= {g. \<exists>H h. g = graph H h
--- a/src/HOL/Real/HahnBanach/Linearform.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Wed Jan 02 15:14:02 2008 +0100
@@ -13,6 +13,7 @@
*}
locale linearform = var V + var f +
+ constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Wed Jan 02 15:14:02 2008 +0100
@@ -19,6 +19,7 @@
fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>")
locale seminorm = var V + norm_syntax +
+ constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
--- a/src/HOL/Real/HahnBanach/Subspace.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Wed Jan 02 15:14:02 2008 +0100
@@ -17,6 +17,7 @@
*}
locale subspace = var U + var V +
+ constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
assumes non_empty [iff, intro]: "U \<noteq> {}"
and subset [iff]: "U \<subseteq> V"
and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
--- a/src/HOL/Real/Rational.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/Rational.thy Wed Jan 02 15:14:02 2008 +0100
@@ -6,7 +6,7 @@
header {* Rational numbers *}
theory Rational
-imports Abstract_Rat
+imports "~~/src/HOL/Library/Abstract_Rat"
uses ("rat_arith.ML")
begin
@@ -163,7 +163,7 @@
subsubsection {* Standard operations on rational numbers *}
-instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+instantiation rat :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
begin
definition
--- a/src/HOL/Real/RealDef.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Real/RealDef.thy Wed Jan 02 15:14:02 2008 +0100
@@ -25,7 +25,7 @@
real_of_preal :: "preal => real" where
"real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
-instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
begin
definition
--- a/src/HOL/Ring_and_Field.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Ring_and_Field.thy Wed Jan 02 15:14:02 2008 +0100
@@ -516,10 +516,10 @@
end
-class abs_if = minus + ord + zero + abs +
- assumes abs_if: "\<bar>a\<bar> = (if a < 0 then (- a) else a)"
-
-class sgn_if = sgn + zero + one + minus + ord +
+class abs_if = minus + uminus + ord + zero + abs +
+ assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
+
+class sgn_if = minus + uminus + zero + one + ord + sgn +
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
--- a/src/HOL/Set.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Set.thy Wed Jan 02 15:14:02 2008 +0100
@@ -352,10 +352,17 @@
begin
definition
- Compl_def [code func del]: "- A = {x. ~x:A}"
+ set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
+
+instance ..
+
+end
+
+instantiation set :: (type) uminus
+begin
definition
- set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
+ Compl_def [code func del]: "- A = {x. ~x:A}"
instance ..
--- a/src/HOL/Tools/Qelim/cooper_data.ML Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Wed Jan 02 15:14:02 2008 +0100
@@ -19,28 +19,28 @@
val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
addcongs [if_weak_cong, @{thm "let_weak_cong"}];*)
val allowed_consts =
- [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
- @{term "op - :: int => _"}, @{term "op - :: nat => _"},
- @{term "op * :: int => _"}, @{term "op * :: nat => _"},
- @{term "op div :: int => _"}, @{term "op div :: nat => _"},
- @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
+ [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
+ @{term "op - :: int => _"}, @{term "op - :: nat => _"},
+ @{term "op * :: int => _"}, @{term "op * :: nat => _"},
+ @{term "op div :: int => _"}, @{term "op div :: nat => _"},
+ @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
@{term "Numeral.Bit"},
@{term "op &"}, @{term "op |"}, @{term "op -->"},
- @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
+ @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
- @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
- @{term "abs :: int => _"}, (*@ {term "abs :: nat => _"}, *)
- @{term "max :: int => _"}, @{term "max :: nat => _"},
- @{term "min :: int => _"}, @{term "min :: nat => _"},
- @{term "HOL.uminus :: int => _"}, @{term "HOL.uminus :: nat => _"},
- @{term "Not"}, @{term "Suc"},
- @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
- @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
+ @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"},
+ @{term "abs :: int => _"},
+ @{term "max :: int => _"}, @{term "max :: nat => _"},
+ @{term "min :: int => _"}, @{term "min :: nat => _"},
+ @{term "HOL.uminus :: int => _"}, (*@ {term "HOL.uminus :: nat => _"},*)
+ @{term "Not"}, @{term "Suc"},
+ @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
+ @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
@{term "nat"}, @{term "int"},
@{term "Numeral.bit.B0"},@{term "Numeral.bit.B1"},
@{term "Numeral.Bit"}, @{term "Numeral.Pls"}, @{term "Numeral.Min"},
- @{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"},
+ @{term "Numeral.number_of :: int => int"}, @{term "Numeral.number_of :: int => nat"},
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
@{term "True"}, @{term "False"}];
--- a/src/HOL/Word/BinOperations.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/BinOperations.thy Wed Jan 02 15:14:02 2008 +0100
@@ -17,16 +17,28 @@
text "bit-wise logical operations on the int type"
-instance int :: bit
- int_not_def: "bitNOT \<equiv> bin_rec Numeral.Min Numeral.Pls
+instantiation int :: bit
+begin
+
+definition
+ int_not_def: "bitNOT = bin_rec Numeral.Min Numeral.Pls
(\<lambda>w b s. s BIT (NOT b))"
- int_and_def: "bitAND \<equiv> bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y)
+
+definition
+ int_and_def: "bitAND = bin_rec (\<lambda>x. Numeral.Pls) (\<lambda>y. y)
(\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
- int_or_def: "bitOR \<equiv> bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min)
+
+definition
+ int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Numeral.Min)
(\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
- int_xor_def: "bitXOR \<equiv> bin_rec (\<lambda>x. x) bitNOT
+
+definition
+ int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
(\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
- ..
+
+instance ..
+
+end
lemma int_not_simps [simp]:
"NOT Numeral.Pls = Numeral.Min"
--- a/src/HOL/Word/BitSyntax.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/BitSyntax.thy Wed Jan 02 15:14:02 2008 +0100
@@ -45,12 +45,24 @@
subsection {* Bitwise operations on type @{typ bit} *}
-instance bit :: bit
- NOT_bit_def: "NOT x \<equiv> case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0"
- AND_bit_def: "x AND y \<equiv> case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y"
- OR_bit_def: "x OR y :: bit \<equiv> NOT (NOT x AND NOT y)"
- XOR_bit_def: "x XOR y :: bit \<equiv> (x AND NOT y) OR (NOT x AND y)"
- ..
+instantiation bit :: bit
+begin
+
+definition
+ NOT_bit_def: "NOT x = (case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0)"
+
+definition
+ AND_bit_def: "x AND y = (case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y)"
+
+definition
+ OR_bit_def: "(x OR y \<Colon> bit) = NOT (NOT x AND NOT y)"
+
+definition
+ XOR_bit_def: "(x XOR y \<Colon> bit) = (x AND NOT y) OR (NOT x AND y)"
+
+instance ..
+
+end
lemma bit_simps [simp]:
"NOT bit.B0 = bit.B1"
--- a/src/HOL/Word/WordArith.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/WordArith.thy Wed Jan 02 15:14:02 2008 +0100
@@ -25,7 +25,7 @@
interpretation signed: linorder ["word_sle" "word_sless"]
by (rule signed_linorder)
-lemmas word_arith_wis [THEN meta_eq_to_obj_eq] =
+lemmas word_arith_wis =
word_add_def word_mult_def word_minus_def
word_succ_def word_pred_def word_0_wi word_1_wi
@@ -207,7 +207,7 @@
(* now, to get the weaker results analogous to word_div/mod_def *)
lemmas word_arith_alts =
- word_sub_wi [unfolded succ_def pred_def, THEN meta_eq_to_obj_eq, standard]
+ word_sub_wi [unfolded succ_def pred_def, standard]
word_arith_wis [unfolded succ_def pred_def, standard]
lemmas word_sub_alt = word_arith_alts (1)
@@ -247,9 +247,9 @@
len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
lemmas uint_div_alt = word_div_def
- [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
+ [THEN trans [OF uint_cong int_word_uint], standard]
lemmas uint_mod_alt = word_mod_def
- [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
+ [THEN trans [OF uint_cong int_word_uint], standard]
lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
unfolding word_pred_def number_of_eq
@@ -791,7 +791,7 @@
instance word :: (len0) order ..
instance word :: (len) recpower
- by (intro_classes) (simp_all add: word_pow)
+ by (intro_classes) simp_all
(* note that iszero_def is only for class comm_semiring_1_cancel,
which requires word length >= 1, ie 'a :: len word *)
@@ -990,7 +990,7 @@
lemmas un_ui_le = trans
[OF word_le_nat_alt [symmetric]
- word_le_def [THEN meta_eq_to_obj_eq],
+ word_le_def,
standard]
lemma unat_sub_if_size:
--- a/src/HOL/Word/WordDefinition.thy Wed Jan 02 12:22:38 2008 +0100
+++ b/src/HOL/Word/WordDefinition.thy Wed Jan 02 15:14:02 2008 +0100
@@ -13,28 +13,27 @@
typedef (open word) 'a word
= "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
-instance word :: (len0) number ..
-instance word :: (type) minus ..
-instance word :: (type) plus ..
-instance word :: (type) one ..
-instance word :: (type) zero ..
-instance word :: (type) times ..
-instance word :: (type) Divides.div ..
-instance word :: (type) power ..
-instance word :: (type) ord ..
-instance word :: (type) size ..
-instance word :: (type) inverse ..
-instance word :: (type) bit ..
+instantiation word :: (len0) size
+begin
+
+definition
+ word_size: "size (w :: 'a word) = len_of TYPE('a)"
+
+instance ..
+
+end
+
+definition
+ -- {* representation of words using unsigned or signed bins,
+ only difference in these is the type class *}
+ word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
+where
+ "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
subsection "Type conversions and casting"
constdefs
- -- {* representation of words using unsigned or signed bins,
- only difference in these is the type class *}
- word_of_int :: "int => 'a :: len0 word"
- "word_of_int w == Abs_word (bintrunc (len_of TYPE ('a)) w)"
-
-- {* uint and sint cast a word to an integer,
uint treats the word as unsigned,
sint treats the most-significant-bit as a sign bit *}
@@ -81,10 +80,6 @@
word_reverse :: "'a :: len0 word => 'a word"
"word_reverse w == of_bl (rev (to_bl w))"
-defs (overloaded)
- word_size: "size (w :: 'a :: len0 word) == len_of TYPE('a)"
- word_number_of_def: "number_of w == word_of_int w"
-
constdefs
word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b"
"word_int_case f w == f (uint w)"
@@ -97,20 +92,82 @@
subsection "Arithmetic operations"
-defs (overloaded)
- word_1_wi: "(1 :: ('a :: len0) word) == word_of_int 1"
- word_0_wi: "(0 :: ('a :: len0) word) == word_of_int 0"
+instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
+begin
+
+definition
+ word_0_wi: "0 = word_of_int 0"
+
+definition
+ word_1_wi: "1 = word_of_int 1"
+
+definition
+ word_add_def: "a + b = word_of_int (uint a + uint b)"
+
+definition
+ word_sub_wi: "a - b = word_of_int (uint a - uint b)"
+
+definition
+ word_minus_def: "- a = word_of_int (- uint a)"
+
+definition
+ word_mult_def: "a * b = word_of_int (uint a * uint b)"
+
+definition
+ word_div_def: "a div b = word_of_int (uint a div uint b)"
+
+definition
+ word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
+
+primrec power_word where
+ "(a\<Colon>'a word) ^ 0 = 1"
+ | "(a\<Colon>'a word) ^ Suc n = a * a ^ n"
+
+definition
+ word_number_of_def: "number_of w = word_of_int w"
+
+definition
+ word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
- word_le_def: "a <= b == uint a <= uint b"
- word_less_def: "x < y == x <= y & x ~= (y :: 'a :: len0 word)"
+definition
+ word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
+
+definition
+ word_and_def:
+ "(a::'a word) AND b = word_of_int (uint a AND uint b)"
+
+definition
+ word_or_def:
+ "(a::'a word) OR b = word_of_int (uint a OR uint b)"
+
+definition
+ word_xor_def:
+ "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
+
+definition
+ word_not_def:
+ "NOT (a::'a word) = word_of_int (NOT (uint a))"
+
+instance ..
+
+end
+
+abbreviation
+ word_power :: "'a\<Colon>len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
+where
+ "word_power == op ^"
+
+definition
+ word_succ :: "'a :: len0 word => 'a word"
+where
+ "word_succ a = word_of_int (Numeral.succ (uint a))"
+
+definition
+ word_pred :: "'a :: len0 word => 'a word"
+where
+ "word_pred a = word_of_int (Numeral.pred (uint a))"
constdefs
- word_succ :: "'a :: len0 word => 'a word"
- "word_succ a == word_of_int (Numeral.succ (uint a))"
-
- word_pred :: "'a :: len0 word => 'a word"
- "word_pred a == word_of_int (Numeral.pred (uint a))"
-
udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
"a udvd b == EX n>=0. uint b = n * uint a"
@@ -120,37 +177,10 @@
word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
"(x <s y) == (x <=s y & x ~= y)"
-consts
- word_power :: "'a :: len0 word => nat => 'a word"
-primrec
- "word_power a 0 = 1"
- "word_power a (Suc n) = a * word_power a n"
-
-defs (overloaded)
- word_pow: "power == word_power"
- word_add_def: "a + b == word_of_int (uint a + uint b)"
- word_sub_wi: "a - b == word_of_int (uint a - uint b)"
- word_minus_def: "- a == word_of_int (- uint a)"
- word_mult_def: "a * b == word_of_int (uint a * uint b)"
- word_div_def: "a div b == word_of_int (uint a div uint b)"
- word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
-
subsection "Bit-wise operations"
defs (overloaded)
- word_and_def:
- "(a::'a::len0 word) AND b == word_of_int (uint a AND uint b)"
-
- word_or_def:
- "(a::'a::len0 word) OR b == word_of_int (uint a OR uint b)"
-
- word_xor_def:
- "(a::'a::len0 word) XOR b == word_of_int (uint a XOR uint b)"
-
- word_not_def:
- "NOT (a::'a::len0 word) == word_of_int (NOT (uint a))"
-
word_test_bit_def:
"test_bit (a::'a::len0 word) == bin_nth (uint a)"
@@ -269,7 +299,7 @@
lemmas of_nth_def = word_set_bits_def
lemmas word_size_gt_0 [iff] =
- xtr1 [OF word_size [THEN meta_eq_to_obj_eq] len_gt_0, standard]
+ xtr1 [OF word_size len_gt_0, standard]
lemmas lens_gt_0 = word_size_gt_0 len_gt_0
lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
@@ -701,9 +731,9 @@
done
lemmas num_abs_bintr = sym [THEN trans,
- OF num_of_bintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
+ OF num_of_bintr word_number_of_def, standard]
lemmas num_abs_sbintr = sym [THEN trans,
- OF num_of_sbintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
+ OF num_of_sbintr word_number_of_def, standard]
(** cast - note, no arg for new length, as it's determined by type of result,
thus in "cast w = w, the type means cast to length of w! **)