*** empty log message ***
authornipkow
Mon Aug 12 17:48:19 2002 +0200 (2002-08-12)
changeset 13491ddf6ae639f21
parent 13490 44bdc150211b
child 13492 6aae8eb39a18
*** empty log message ***
src/HOL/Hyperreal/HyperBin.ML
src/HOL/Hyperreal/NSA.ML
src/HOL/Integ/Bin.ML
src/HOL/Integ/Bin.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/nat_bin.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/ex/BinEx.thy
     1.1 --- a/src/HOL/Hyperreal/HyperBin.ML	Mon Aug 12 17:48:15 2002 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperBin.ML	Mon Aug 12 17:48:19 2002 +0200
     1.3 @@ -619,14 +619,14 @@
     1.4  
     1.5  (*As above, for the special case of zero*)
     1.6  Addsimps
     1.7 -  (map (simplify (simpset()) o inst "w" "Pls")
     1.8 +  (map (simplify (simpset()) o inst "w" "bin.Pls")
     1.9     [hypreal_of_real_eq_number_of_iff,
    1.10      hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff,
    1.11      number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]);
    1.12  
    1.13  (*As above, for the special case of one*)
    1.14  Addsimps
    1.15 -  (map (simplify (simpset()) o inst "w" "Pls BIT True")
    1.16 +  (map (simplify (simpset()) o inst "w" "bin.Pls BIT True")
    1.17     [hypreal_of_real_eq_number_of_iff,
    1.18      hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff,
    1.19      number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]);
     2.1 --- a/src/HOL/Hyperreal/NSA.ML	Mon Aug 12 17:48:15 2002 +0200
     2.2 +++ b/src/HOL/Hyperreal/NSA.ML	Mon Aug 12 17:48:19 2002 +0200
     2.3 @@ -935,10 +935,10 @@
     2.4  (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
     2.5  Addsimps
     2.6   (map (simplify (simpset()))
     2.7 -      [inst "v" "Pls" number_of_approx_iff,
     2.8 -       inst "v" "Pls BIT True" number_of_approx_iff,
     2.9 -       inst "w" "Pls" number_of_approx_iff,
    2.10 -       inst "w" "Pls BIT True" number_of_approx_iff]);
    2.11 +      [inst "v" "bin.Pls" number_of_approx_iff,
    2.12 +       inst "v" "bin.Pls BIT True" number_of_approx_iff,
    2.13 +       inst "w" "bin.Pls" number_of_approx_iff,
    2.14 +       inst "w" "bin.Pls BIT True" number_of_approx_iff]);
    2.15  
    2.16  
    2.17  Goal "~ (0 @= 1)";
    2.18 @@ -970,8 +970,8 @@
    2.19  (*And also for 0 and 1.*)
    2.20  Addsimps
    2.21   (map (simplify (simpset()))
    2.22 -      [inst "w" "Pls" hypreal_of_real_approx_number_of_iff,
    2.23 -       inst "w" "Pls BIT True" hypreal_of_real_approx_number_of_iff]);
    2.24 +      [inst "w" "bin.Pls" hypreal_of_real_approx_number_of_iff,
    2.25 +       inst "w" "bin.Pls BIT True" hypreal_of_real_approx_number_of_iff]);
    2.26  
    2.27  Goal "[| r: Reals; s: Reals; r @= x; s @= x|] ==> r = s";
    2.28  by (blast_tac (claset() addIs [(SReal_approx_iff RS iffD1),
    2.29 @@ -1737,7 +1737,7 @@
    2.30  (*the theorem above for the special cases of zero and one*)
    2.31  Addsimps
    2.32    (map (simplify (simpset()))
    2.33 -   [inst "w" "Pls" st_number_of, inst "w" "Pls BIT True" st_number_of]);
    2.34 +   [inst "w" "bin.Pls" st_number_of, inst "w" "bin.Pls BIT True" st_number_of]);
    2.35  
    2.36  Goal "y: HFinite ==> st(-y) = -st(y)";
    2.37  by (forward_tac [HFinite_minus_iff RS iffD2] 1);
     3.1 --- a/src/HOL/Integ/Bin.ML	Mon Aug 12 17:48:15 2002 +0200
     3.2 +++ b/src/HOL/Integ/Bin.ML	Mon Aug 12 17:48:19 2002 +0200
     3.3 @@ -12,19 +12,19 @@
     3.4  
     3.5  (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
     3.6  
     3.7 -Goal "NCons Pls False = Pls";
     3.8 +Goal "NCons bin.Pls False = bin.Pls";
     3.9  by (Simp_tac 1);
    3.10  qed "NCons_Pls_0";
    3.11  
    3.12 -Goal "NCons Pls True = Pls BIT True";
    3.13 +Goal "NCons bin.Pls True = bin.Pls BIT True";
    3.14  by (Simp_tac 1);
    3.15  qed "NCons_Pls_1";
    3.16  
    3.17 -Goal "NCons Min False = Min BIT False";
    3.18 +Goal "NCons bin.Min False = bin.Min BIT False";
    3.19  by (Simp_tac 1);
    3.20  qed "NCons_Min_0";
    3.21  
    3.22 -Goal "NCons Min True = Min";
    3.23 +Goal "NCons bin.Min True = bin.Min";
    3.24  by (Simp_tac 1);
    3.25  qed "NCons_Min_1";
    3.26  
    3.27 @@ -68,12 +68,12 @@
    3.28  by Auto_tac;
    3.29  qed "bin_add_BIT_0";
    3.30  
    3.31 -Goal "bin_add w Pls = w";
    3.32 +Goal "bin_add w bin.Pls = w";
    3.33  by (induct_tac "w" 1);
    3.34  by Auto_tac;
    3.35  qed "bin_add_Pls_right";
    3.36  
    3.37 -Goal "bin_add w Min = bin_pred w";
    3.38 +Goal "bin_add w bin.Min = bin_pred w";
    3.39  by (induct_tac "w" 1);
    3.40  by Auto_tac;
    3.41  qed "bin_add_Min_right";
    3.42 @@ -246,11 +246,11 @@
    3.43                   addsimps zcompare_rls @ [number_of_add, number_of_minus]) 1); 
    3.44  qed "eq_number_of_eq"; 
    3.45  
    3.46 -Goalw [iszero_def] "iszero ((number_of Pls)::int)"; 
    3.47 +Goalw [iszero_def] "iszero ((number_of bin.Pls)::int)"; 
    3.48  by (Simp_tac 1); 
    3.49  qed "iszero_number_of_Pls"; 
    3.50  
    3.51 -Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; 
    3.52 +Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)"; 
    3.53  by (Simp_tac 1);
    3.54  qed "nonzero_number_of_Min"; 
    3.55  
    3.56 @@ -284,11 +284,11 @@
    3.57  
    3.58  (*But if Numeral0 is rewritten to 0 then this rule can't be applied:
    3.59    Numeral0 IS (number_of Pls) *)
    3.60 -Goal "~ neg (number_of Pls)";
    3.61 +Goal "~ neg (number_of bin.Pls)";
    3.62  by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1);  
    3.63  qed "not_neg_number_of_Pls"; 
    3.64  
    3.65 -Goal "neg (number_of Min)"; 
    3.66 +Goal "neg (number_of bin.Min)"; 
    3.67  by (simp_tac (simpset() addsimps [neg_eq_less_0, int_0_less_1]) 1);
    3.68  qed "neg_number_of_Min"; 
    3.69  
     4.1 --- a/src/HOL/Integ/Bin.thy	Mon Aug 12 17:48:15 2002 +0200
     4.2 +++ b/src/HOL/Integ/Bin.thy	Mon Aug 12 17:48:19 2002 +0200
     4.3 @@ -29,43 +29,43 @@
     4.4  
     4.5  (*NCons inserts a bit, suppressing leading 0s and 1s*)
     4.6  primrec
     4.7 -  NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
     4.8 -  NCons_Min "NCons Min b = (if b then Min else (Min BIT b))"
     4.9 +  NCons_Pls "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
    4.10 +  NCons_Min "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
    4.11    NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
    4.12  
    4.13  instance
    4.14    int :: number
    4.15  
    4.16  primrec (*the type constraint is essential!*)
    4.17 -  number_of_Pls  "number_of Pls = 0"
    4.18 -  number_of_Min  "number_of Min = - (1::int)"
    4.19 +  number_of_Pls  "number_of bin.Pls = 0"
    4.20 +  number_of_Min  "number_of bin.Min = - (1::int)"
    4.21    number_of_BIT  "number_of(w BIT x) = (if x then 1 else 0) +
    4.22  	                               (number_of w) + (number_of w)" 
    4.23  
    4.24  primrec
    4.25 -  bin_succ_Pls  "bin_succ Pls = Pls BIT True" 
    4.26 -  bin_succ_Min  "bin_succ Min = Pls"
    4.27 +  bin_succ_Pls  "bin_succ bin.Pls = bin.Pls BIT True" 
    4.28 +  bin_succ_Min  "bin_succ bin.Min = bin.Pls"
    4.29    bin_succ_BIT  "bin_succ(w BIT x) =
    4.30    	            (if x then bin_succ w BIT False
    4.31  	                  else NCons w True)"
    4.32  
    4.33  primrec
    4.34 -  bin_pred_Pls  "bin_pred Pls = Min"
    4.35 -  bin_pred_Min  "bin_pred Min = Min BIT False"
    4.36 +  bin_pred_Pls  "bin_pred bin.Pls = bin.Min"
    4.37 +  bin_pred_Min  "bin_pred bin.Min = bin.Min BIT False"
    4.38    bin_pred_BIT  "bin_pred(w BIT x) =
    4.39  	            (if x then NCons w False
    4.40  		          else (bin_pred w) BIT True)"
    4.41   
    4.42  primrec
    4.43 -  bin_minus_Pls  "bin_minus Pls = Pls"
    4.44 -  bin_minus_Min  "bin_minus Min = Pls BIT True"
    4.45 +  bin_minus_Pls  "bin_minus bin.Pls = bin.Pls"
    4.46 +  bin_minus_Min  "bin_minus bin.Min = bin.Pls BIT True"
    4.47    bin_minus_BIT  "bin_minus(w BIT x) =
    4.48  	             (if x then bin_pred (NCons (bin_minus w) False)
    4.49  		           else bin_minus w BIT False)"
    4.50  
    4.51  primrec
    4.52 -  bin_add_Pls  "bin_add Pls w = w"
    4.53 -  bin_add_Min  "bin_add Min w = bin_pred w"
    4.54 +  bin_add_Pls  "bin_add bin.Pls w = w"
    4.55 +  bin_add_Min  "bin_add bin.Min w = bin_pred w"
    4.56    bin_add_BIT
    4.57      "bin_add (v BIT x) w = 
    4.58         (case w of Pls => v BIT x
    4.59 @@ -75,8 +75,8 @@
    4.60  	                  (x~=y))"
    4.61  
    4.62  primrec
    4.63 -  bin_mult_Pls  "bin_mult Pls w = Pls"
    4.64 -  bin_mult_Min  "bin_mult Min w = bin_minus w"
    4.65 +  bin_mult_Pls  "bin_mult bin.Pls w = bin.Pls"
    4.66 +  bin_mult_Min  "bin_mult bin.Min w = bin_minus w"
    4.67    bin_mult_BIT  "bin_mult (v BIT x) w =
    4.68  	            (if x then (bin_add (NCons (bin_mult v w) False) w)
    4.69  	                  else (NCons (bin_mult v w) False))"
     5.1 --- a/src/HOL/Integ/NatBin.thy	Mon Aug 12 17:48:15 2002 +0200
     5.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Aug 12 17:48:19 2002 +0200
     5.3 @@ -26,10 +26,10 @@
     5.4  declare split_div[of _ _ "number_of k", standard, arith_split]
     5.5  declare split_mod[of _ _ "number_of k", standard, arith_split]
     5.6  
     5.7 -lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
     5.8 +lemma nat_number_of_Pls: "number_of bin.Pls = (0::nat)"
     5.9    by (simp add: number_of_Pls nat_number_of_def)
    5.10  
    5.11 -lemma nat_number_of_Min: "number_of Min = (0::nat)"
    5.12 +lemma nat_number_of_Min: "number_of bin.Min = (0::nat)"
    5.13    apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
    5.14    apply (simp add: neg_nat)
    5.15    done
     6.1 --- a/src/HOL/Integ/nat_bin.ML	Mon Aug 12 17:48:15 2002 +0200
     6.2 +++ b/src/HOL/Integ/nat_bin.ML	Mon Aug 12 17:48:19 2002 +0200
     6.3 @@ -449,8 +449,8 @@
     6.4  	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
     6.5  qed "eq_number_of_BIT_BIT"; 
     6.6  
     6.7 -Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
     6.8 -\     (x=False & (((number_of v) ::int) = number_of Pls))"; 
     6.9 +Goal "((number_of (v BIT x) ::int) = number_of bin.Pls) = \
    6.10 +\     (x=False & (((number_of v) ::int) = number_of bin.Pls))"; 
    6.11  by (simp_tac (simpset_of Int.thy addsimps
    6.12  	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
    6.13  by (res_inst_tac [("x", "number_of v")] spec 1);
    6.14 @@ -460,8 +460,8 @@
    6.15  by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
    6.16  qed "eq_number_of_BIT_Pls"; 
    6.17  
    6.18 -Goal "((number_of (v BIT x) ::int) = number_of Min) = \
    6.19 -\     (x=True & (((number_of v) ::int) = number_of Min))"; 
    6.20 +Goal "((number_of (v BIT x) ::int) = number_of bin.Min) = \
    6.21 +\     (x=True & (((number_of v) ::int) = number_of bin.Min))"; 
    6.22  by (simp_tac (simpset_of Int.thy addsimps
    6.23  	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
    6.24  by (res_inst_tac [("x", "number_of v")] spec 1);
    6.25 @@ -470,7 +470,7 @@
    6.26  by Auto_tac;
    6.27  qed "eq_number_of_BIT_Min"; 
    6.28  
    6.29 -Goal "(number_of Pls ::int) ~= number_of Min"; 
    6.30 +Goal "(number_of bin.Pls ::int) ~= number_of bin.Min"; 
    6.31  by Auto_tac;
    6.32  qed "eq_number_of_Pls_Min"; 
    6.33  
     7.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon Aug 12 17:48:15 2002 +0200
     7.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Mon Aug 12 17:48:19 2002 +0200
     7.3 @@ -29,14 +29,10 @@
     7.4    | prefix_len pred (x :: xs) =
     7.5        if pred x then 1 + prefix_len pred xs else 0;
     7.6  
     7.7 -(*we consider all "spellings"; Min is likely to be declared elsewhere*)
     7.8 -fun bin_of (Const ("Pls", _)) = []
     7.9 -  | bin_of (Const ("bin.Pls", _)) = []
    7.10 +fun bin_of (Const ("bin.Pls", _)) = []
    7.11    | bin_of (Const ("Numeral.bin.Pls", _)) = []
    7.12 -  | bin_of (Const ("Min", _)) = [~1]
    7.13    | bin_of (Const ("bin.Min", _)) = [~1]
    7.14    | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
    7.15 -  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    7.16    | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    7.17    | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    7.18    | bin_of _ = raise Match;
    7.19 @@ -78,7 +74,9 @@
    7.20  (* theory setup *)
    7.21  
    7.22  val setup =
    7.23 - [Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    7.24 + [Theory.hide_consts false
    7.25 +    ["Numeral.bin.Pls", "Numeral.bin.Min"],
    7.26 +Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    7.27    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    7.28  
    7.29  
     8.1 --- a/src/HOL/ex/BinEx.thy	Mon Aug 12 17:48:15 2002 +0200
     8.2 +++ b/src/HOL/ex/BinEx.thy	Mon Aug 12 17:48:19 2002 +0200
     8.3 @@ -278,10 +278,10 @@
     8.4  consts normal :: "bin set"
     8.5  inductive normal
     8.6    intros
     8.7 -    Pls [simp]: "Pls: normal"
     8.8 -    Min [simp]: "Min: normal"
     8.9 -    BIT_F [simp]: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal"
    8.10 -    BIT_T [simp]: "w: normal ==> w \<noteq> Min ==> w BIT True : normal"
    8.11 +    Pls [simp]: "bin.Pls: normal"
    8.12 +    Min [simp]: "bin.Min: normal"
    8.13 +    BIT_F [simp]: "w: normal ==> w \<noteq> bin.Pls ==> w BIT False : normal"
    8.14 +    BIT_T [simp]: "w: normal ==> w \<noteq> bin.Min ==> w BIT True : normal"
    8.15  
    8.16  text {*
    8.17    \medskip Binary arithmetic on normalized operands yields normalized
    8.18 @@ -303,12 +303,12 @@
    8.19      apply (auto simp add: NCons_Pls NCons_Min)
    8.20    done
    8.21  
    8.22 -lemma NCons_True: "NCons w True \<noteq> Pls"
    8.23 +lemma NCons_True: "NCons w True \<noteq> bin.Pls"
    8.24    apply (induct w)
    8.25      apply auto
    8.26    done
    8.27  
    8.28 -lemma NCons_False: "NCons w False \<noteq> Min"
    8.29 +lemma NCons_False: "NCons w False \<noteq> bin.Min"
    8.30    apply (induct w)
    8.31      apply auto
    8.32    done
    8.33 @@ -338,7 +338,7 @@
    8.34      apply simp_all
    8.35    done
    8.36  
    8.37 -lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (0::int))"
    8.38 +lemma normal_Pls_eq_0: "w \<in> normal ==> (w = bin.Pls) = (number_of w = (0::int))"
    8.39    apply (erule normal.induct)
    8.40       apply auto
    8.41    done
    8.42 @@ -362,11 +362,11 @@
    8.43  But on the way we get
    8.44  
    8.45  Procedure "int_add_eval_numerals" produced rewrite rule:
    8.46 -number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (Pls BIT True))
    8.47 +number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (bin.Pls BIT True))
    8.48  
    8.49  and eventually we arrive not at false but at
    8.50  
    8.51 -"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (Pls BIT True)))))"
    8.52 +"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (bin.Pls BIT True)))))"
    8.53  
    8.54  The simplification with eq_commute should now be obsolete.
    8.55  *)