# HG changeset patch # User nipkow # Date 1029167299 -7200 # Node ID ddf6ae639f21bde0efcd075ae2bb0411dc671d9e # Parent 44bdc150211bc709efab7556ef0219125e52b074 *** empty log message *** diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/Hyperreal/HyperBin.ML --- 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]); diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/Hyperreal/NSA.ML --- 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); diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/Integ/Bin.ML --- 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"; diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/Integ/Bin.thy --- 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))" diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/Integ/NatBin.thy --- 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 diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/Integ/nat_bin.ML --- 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"; diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/Tools/numeral_syntax.ML --- 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')]]; diff -r 44bdc150211b -r ddf6ae639f21 src/HOL/ex/BinEx.thy --- 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 \ Pls ==> w BIT False : normal" - BIT_T [simp]: "w: normal ==> w \ Min ==> w BIT True : normal" + Pls [simp]: "bin.Pls: normal" + Min [simp]: "bin.Min: normal" + BIT_F [simp]: "w: normal ==> w \ bin.Pls ==> w BIT False : normal" + BIT_T [simp]: "w: normal ==> w \ 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 \ Pls" +lemma NCons_True: "NCons w True \ bin.Pls" apply (induct w) apply auto done -lemma NCons_False: "NCons w False \ Min" +lemma NCons_False: "NCons w False \ bin.Min" apply (induct w) apply auto done @@ -338,7 +338,7 @@ apply simp_all done -lemma normal_Pls_eq_0: "w \ normal ==> (w = Pls) = (number_of w = (0::int))" +lemma normal_Pls_eq_0: "w \ 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 \ number_of (bin_add ?v3 (Pls BIT True)) +number_of ?v3 + 1 \ number_of (bin_add ?v3 (bin.Pls BIT True)) and eventually we arrive not at false but at -"\ neg (number_of (bin_add w (bin_minus (bin_add w (Pls BIT True)))))" +"\ neg (number_of (bin_add w (bin_minus (bin_add w (bin.Pls BIT True)))))" The simplification with eq_commute should now be obsolete. *)