--- a/src/HOL/Hyperreal/HyperBin.ML Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML Mon Aug 12 17:48:19 2002 +0200
@@ -619,14 +619,14 @@
(*As above, for the special case of zero*)
Addsimps
- (map (simplify (simpset()) o inst "w" "Pls")
+ (map (simplify (simpset()) o inst "w" "bin.Pls")
[hypreal_of_real_eq_number_of_iff,
hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff,
number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]);
(*As above, for the special case of one*)
Addsimps
- (map (simplify (simpset()) o inst "w" "Pls BIT True")
+ (map (simplify (simpset()) o inst "w" "bin.Pls BIT True")
[hypreal_of_real_eq_number_of_iff,
hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff,
number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]);
--- a/src/HOL/Hyperreal/NSA.ML Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/Hyperreal/NSA.ML Mon Aug 12 17:48:19 2002 +0200
@@ -935,10 +935,10 @@
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
Addsimps
(map (simplify (simpset()))
- [inst "v" "Pls" number_of_approx_iff,
- inst "v" "Pls BIT True" number_of_approx_iff,
- inst "w" "Pls" number_of_approx_iff,
- inst "w" "Pls BIT True" number_of_approx_iff]);
+ [inst "v" "bin.Pls" number_of_approx_iff,
+ inst "v" "bin.Pls BIT True" number_of_approx_iff,
+ inst "w" "bin.Pls" number_of_approx_iff,
+ inst "w" "bin.Pls BIT True" number_of_approx_iff]);
Goal "~ (0 @= 1)";
@@ -970,8 +970,8 @@
(*And also for 0 and 1.*)
Addsimps
(map (simplify (simpset()))
- [inst "w" "Pls" hypreal_of_real_approx_number_of_iff,
- inst "w" "Pls BIT True" hypreal_of_real_approx_number_of_iff]);
+ [inst "w" "bin.Pls" hypreal_of_real_approx_number_of_iff,
+ inst "w" "bin.Pls BIT True" hypreal_of_real_approx_number_of_iff]);
Goal "[| r: Reals; s: Reals; r @= x; s @= x|] ==> r = s";
by (blast_tac (claset() addIs [(SReal_approx_iff RS iffD1),
@@ -1737,7 +1737,7 @@
(*the theorem above for the special cases of zero and one*)
Addsimps
(map (simplify (simpset()))
- [inst "w" "Pls" st_number_of, inst "w" "Pls BIT True" st_number_of]);
+ [inst "w" "bin.Pls" st_number_of, inst "w" "bin.Pls BIT True" st_number_of]);
Goal "y: HFinite ==> st(-y) = -st(y)";
by (forward_tac [HFinite_minus_iff RS iffD2] 1);
--- a/src/HOL/Integ/Bin.ML Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/Integ/Bin.ML Mon Aug 12 17:48:19 2002 +0200
@@ -12,19 +12,19 @@
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
-Goal "NCons Pls False = Pls";
+Goal "NCons bin.Pls False = bin.Pls";
by (Simp_tac 1);
qed "NCons_Pls_0";
-Goal "NCons Pls True = Pls BIT True";
+Goal "NCons bin.Pls True = bin.Pls BIT True";
by (Simp_tac 1);
qed "NCons_Pls_1";
-Goal "NCons Min False = Min BIT False";
+Goal "NCons bin.Min False = bin.Min BIT False";
by (Simp_tac 1);
qed "NCons_Min_0";
-Goal "NCons Min True = Min";
+Goal "NCons bin.Min True = bin.Min";
by (Simp_tac 1);
qed "NCons_Min_1";
@@ -68,12 +68,12 @@
by Auto_tac;
qed "bin_add_BIT_0";
-Goal "bin_add w Pls = w";
+Goal "bin_add w bin.Pls = w";
by (induct_tac "w" 1);
by Auto_tac;
qed "bin_add_Pls_right";
-Goal "bin_add w Min = bin_pred w";
+Goal "bin_add w bin.Min = bin_pred w";
by (induct_tac "w" 1);
by Auto_tac;
qed "bin_add_Min_right";
@@ -246,11 +246,11 @@
addsimps zcompare_rls @ [number_of_add, number_of_minus]) 1);
qed "eq_number_of_eq";
-Goalw [iszero_def] "iszero ((number_of Pls)::int)";
+Goalw [iszero_def] "iszero ((number_of bin.Pls)::int)";
by (Simp_tac 1);
qed "iszero_number_of_Pls";
-Goalw [iszero_def] "~ iszero ((number_of Min)::int)";
+Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";
by (Simp_tac 1);
qed "nonzero_number_of_Min";
@@ -284,11 +284,11 @@
(*But if Numeral0 is rewritten to 0 then this rule can't be applied:
Numeral0 IS (number_of Pls) *)
-Goal "~ neg (number_of Pls)";
+Goal "~ neg (number_of bin.Pls)";
by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1);
qed "not_neg_number_of_Pls";
-Goal "neg (number_of Min)";
+Goal "neg (number_of bin.Min)";
by (simp_tac (simpset() addsimps [neg_eq_less_0, int_0_less_1]) 1);
qed "neg_number_of_Min";
--- a/src/HOL/Integ/Bin.thy Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/Integ/Bin.thy Mon Aug 12 17:48:19 2002 +0200
@@ -29,43 +29,43 @@
(*NCons inserts a bit, suppressing leading 0s and 1s*)
primrec
- NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
- NCons_Min "NCons Min b = (if b then Min else (Min BIT b))"
+ NCons_Pls "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
+ NCons_Min "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
instance
int :: number
primrec (*the type constraint is essential!*)
- number_of_Pls "number_of Pls = 0"
- number_of_Min "number_of Min = - (1::int)"
+ number_of_Pls "number_of bin.Pls = 0"
+ number_of_Min "number_of bin.Min = - (1::int)"
number_of_BIT "number_of(w BIT x) = (if x then 1 else 0) +
(number_of w) + (number_of w)"
primrec
- bin_succ_Pls "bin_succ Pls = Pls BIT True"
- bin_succ_Min "bin_succ Min = Pls"
+ bin_succ_Pls "bin_succ bin.Pls = bin.Pls BIT True"
+ bin_succ_Min "bin_succ bin.Min = bin.Pls"
bin_succ_BIT "bin_succ(w BIT x) =
(if x then bin_succ w BIT False
else NCons w True)"
primrec
- bin_pred_Pls "bin_pred Pls = Min"
- bin_pred_Min "bin_pred Min = Min BIT False"
+ bin_pred_Pls "bin_pred bin.Pls = bin.Min"
+ bin_pred_Min "bin_pred bin.Min = bin.Min BIT False"
bin_pred_BIT "bin_pred(w BIT x) =
(if x then NCons w False
else (bin_pred w) BIT True)"
primrec
- bin_minus_Pls "bin_minus Pls = Pls"
- bin_minus_Min "bin_minus Min = Pls BIT True"
+ bin_minus_Pls "bin_minus bin.Pls = bin.Pls"
+ bin_minus_Min "bin_minus bin.Min = bin.Pls BIT True"
bin_minus_BIT "bin_minus(w BIT x) =
(if x then bin_pred (NCons (bin_minus w) False)
else bin_minus w BIT False)"
primrec
- bin_add_Pls "bin_add Pls w = w"
- bin_add_Min "bin_add Min w = bin_pred w"
+ bin_add_Pls "bin_add bin.Pls w = w"
+ bin_add_Min "bin_add bin.Min w = bin_pred w"
bin_add_BIT
"bin_add (v BIT x) w =
(case w of Pls => v BIT x
@@ -75,8 +75,8 @@
(x~=y))"
primrec
- bin_mult_Pls "bin_mult Pls w = Pls"
- bin_mult_Min "bin_mult Min w = bin_minus w"
+ bin_mult_Pls "bin_mult bin.Pls w = bin.Pls"
+ bin_mult_Min "bin_mult bin.Min w = bin_minus w"
bin_mult_BIT "bin_mult (v BIT x) w =
(if x then (bin_add (NCons (bin_mult v w) False) w)
else (NCons (bin_mult v w) False))"
--- a/src/HOL/Integ/NatBin.thy Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/Integ/NatBin.thy Mon Aug 12 17:48:19 2002 +0200
@@ -26,10 +26,10 @@
declare split_div[of _ _ "number_of k", standard, arith_split]
declare split_mod[of _ _ "number_of k", standard, arith_split]
-lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
+lemma nat_number_of_Pls: "number_of bin.Pls = (0::nat)"
by (simp add: number_of_Pls nat_number_of_def)
-lemma nat_number_of_Min: "number_of Min = (0::nat)"
+lemma nat_number_of_Min: "number_of bin.Min = (0::nat)"
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
apply (simp add: neg_nat)
done
--- a/src/HOL/Integ/nat_bin.ML Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/Integ/nat_bin.ML Mon Aug 12 17:48:19 2002 +0200
@@ -449,8 +449,8 @@
[number_of_BIT, lemma1, lemma2, eq_commute]) 1);
qed "eq_number_of_BIT_BIT";
-Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
-\ (x=False & (((number_of v) ::int) = number_of Pls))";
+Goal "((number_of (v BIT x) ::int) = number_of bin.Pls) = \
+\ (x=False & (((number_of v) ::int) = number_of bin.Pls))";
by (simp_tac (simpset_of Int.thy addsimps
[number_of_BIT, number_of_Pls, eq_commute]) 1);
by (res_inst_tac [("x", "number_of v")] spec 1);
@@ -460,8 +460,8 @@
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
qed "eq_number_of_BIT_Pls";
-Goal "((number_of (v BIT x) ::int) = number_of Min) = \
-\ (x=True & (((number_of v) ::int) = number_of Min))";
+Goal "((number_of (v BIT x) ::int) = number_of bin.Min) = \
+\ (x=True & (((number_of v) ::int) = number_of bin.Min))";
by (simp_tac (simpset_of Int.thy addsimps
[number_of_BIT, number_of_Min, eq_commute]) 1);
by (res_inst_tac [("x", "number_of v")] spec 1);
@@ -470,7 +470,7 @@
by Auto_tac;
qed "eq_number_of_BIT_Min";
-Goal "(number_of Pls ::int) ~= number_of Min";
+Goal "(number_of bin.Pls ::int) ~= number_of bin.Min";
by Auto_tac;
qed "eq_number_of_Pls_Min";
--- a/src/HOL/Tools/numeral_syntax.ML Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Mon Aug 12 17:48:19 2002 +0200
@@ -29,14 +29,10 @@
| prefix_len pred (x :: xs) =
if pred x then 1 + prefix_len pred xs else 0;
-(*we consider all "spellings"; Min is likely to be declared elsewhere*)
-fun bin_of (Const ("Pls", _)) = []
- | bin_of (Const ("bin.Pls", _)) = []
+fun bin_of (Const ("bin.Pls", _)) = []
| bin_of (Const ("Numeral.bin.Pls", _)) = []
- | bin_of (Const ("Min", _)) = [~1]
| bin_of (Const ("bin.Min", _)) = [~1]
| bin_of (Const ("Numeral.bin.Min", _)) = [~1]
- | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
@@ -78,7 +74,9 @@
(* theory setup *)
val setup =
- [Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
+ [Theory.hide_consts false
+ ["Numeral.bin.Pls", "Numeral.bin.Min"],
+Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
--- a/src/HOL/ex/BinEx.thy Mon Aug 12 17:48:15 2002 +0200
+++ b/src/HOL/ex/BinEx.thy Mon Aug 12 17:48:19 2002 +0200
@@ -278,10 +278,10 @@
consts normal :: "bin set"
inductive normal
intros
- Pls [simp]: "Pls: normal"
- Min [simp]: "Min: normal"
- BIT_F [simp]: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
- BIT_T [simp]: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
+ Pls [simp]: "bin.Pls: normal"
+ Min [simp]: "bin.Min: normal"
+ BIT_F [simp]: "w: normal ==> w \<noteq> bin.Pls ==> w BIT False : normal"
+ BIT_T [simp]: "w: normal ==> w \<noteq> bin.Min ==> w BIT True : normal"
text {*
\medskip Binary arithmetic on normalized operands yields normalized
@@ -303,12 +303,12 @@
apply (auto simp add: NCons_Pls NCons_Min)
done
-lemma NCons_True: "NCons w True \<noteq> Pls"
+lemma NCons_True: "NCons w True \<noteq> bin.Pls"
apply (induct w)
apply auto
done
-lemma NCons_False: "NCons w False \<noteq> Min"
+lemma NCons_False: "NCons w False \<noteq> bin.Min"
apply (induct w)
apply auto
done
@@ -338,7 +338,7 @@
apply simp_all
done
-lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (0::int))"
+lemma normal_Pls_eq_0: "w \<in> normal ==> (w = bin.Pls) = (number_of w = (0::int))"
apply (erule normal.induct)
apply auto
done
@@ -362,11 +362,11 @@
But on the way we get
Procedure "int_add_eval_numerals" produced rewrite rule:
-number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (Pls BIT True))
+number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (bin.Pls BIT True))
and eventually we arrive not at false but at
-"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (Pls BIT True)))))"
+"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (bin.Pls BIT True)))))"
The simplification with eq_commute should now be obsolete.
*)