changed 2 to #2
authorpaulson
Thu May 04 15:15:37 2000 +0200 (2000-05-04)
changeset 879150b650d19641
parent 8790 c4aaa5936e0c
child 8792 59a4b5e6a591
changed 2 to #2
src/HOL/Hoare/Arith2.ML
src/HOL/Hoare/Arith2.thy
src/HOL/Hoare/Examples.ML
src/HOL/IMPP/EvenOdd.ML
src/HOL/IMPP/EvenOdd.thy
src/HOL/Quot/FRACT.ML
     1.1 --- a/src/HOL/Hoare/Arith2.ML	Thu May 04 15:14:56 2000 +0200
     1.2 +++ b/src/HOL/Hoare/Arith2.ML	Thu May 04 15:15:37 2000 +0200
     1.3 @@ -63,10 +63,8 @@
     1.4  
     1.5  (*** pow ***)
     1.6  
     1.7 -Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
     1.8 -by (subgoal_tac "n*n=n^2" 1);
     1.9 -by (etac ssubst 1 THEN stac (power_mult RS sym) 1);
    1.10 -by (stac mult_div_cancel 1);
    1.11 -by (ALLGOALS Asm_simp_tac);
    1.12 +Goal "m mod #2 = 0 ==> ((n::nat)*n)^(m div #2) = n^m";
    1.13 +by (asm_simp_tac (simpset() addsimps [power_two RS sym, power_mult RS sym,
    1.14 +				      mult_div_cancel]) 1);
    1.15  qed "sq_pow_div2";
    1.16  Addsimps [sq_pow_div2];
     2.1 --- a/src/HOL/Hoare/Arith2.thy	Thu May 04 15:14:56 2000 +0200
     2.2 +++ b/src/HOL/Hoare/Arith2.thy	Thu May 04 15:15:37 2000 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  More arithmetic.  Much of this duplicates ex/Primes.
     2.5  *)
     2.6  
     2.7 -Arith2 = Power +
     2.8 +Arith2 = Main +
     2.9  
    2.10  constdefs
    2.11    cd      :: [nat, nat, nat] => bool
     3.1 --- a/src/HOL/Hoare/Examples.ML	Thu May 04 15:14:56 2000 +0200
     3.2 +++ b/src/HOL/Hoare/Examples.ML	Thu May 04 15:15:37 2000 +0200
     3.3 @@ -43,17 +43,16 @@
     3.4  \ c := 1; \
     3.5  \ WHILE b ~= 0 \
     3.6  \ INV {A^B = c * a^b} \
     3.7 -\ DO  WHILE b mod 2 = 0 \
     3.8 +\ DO  WHILE b mod #2 = 0 \
     3.9  \     INV {A^B = c * a^b} \
    3.10 -\     DO  a := a*a; b := b div 2 OD; \
    3.11 +\     DO  a := a*a; b := b div #2 OD; \
    3.12  \     c := c*a; b := b-1 \
    3.13  \ OD \
    3.14  \ {c = A^B}";
    3.15  by (hoare_tac (Asm_full_simp_tac) 1);
    3.16  by (case_tac "b" 1);
    3.17 -by (hyp_subst_tac 1);
    3.18  by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
    3.19 -by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
    3.20 +by (Asm_simp_tac 1);
    3.21  qed "power_by_mult";
    3.22  
    3.23  (** Factorial **)
     4.1 --- a/src/HOL/IMPP/EvenOdd.ML	Thu May 04 15:14:56 2000 +0200
     4.2 +++ b/src/HOL/IMPP/EvenOdd.ML	Thu May 04 15:15:37 2000 +0200
     4.3 @@ -19,7 +19,7 @@
     4.4  Addsimps [not_even_1];
     4.5  
     4.6  Goalw [even_def] "even (Suc (Suc n)) = even n";
     4.7 -by (subgoal_tac "Suc (Suc n) = n+2" 1);
     4.8 +by (subgoal_tac "Suc (Suc n) = n+#2" 1);
     4.9  by  (Simp_tac 2);
    4.10  be ssubst 1;
    4.11  br dvd_reduce 1;
     5.1 --- a/src/HOL/IMPP/EvenOdd.thy	Thu May 04 15:14:56 2000 +0200
     5.2 +++ b/src/HOL/IMPP/EvenOdd.thy	Thu May 04 15:15:37 2000 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  EvenOdd = Misc +
     5.5  
     5.6  constdefs even :: nat => bool
     5.7 -  "even n == 2 dvd n"
     5.8 +  "even n == #2 dvd n"
     5.9  
    5.10  consts
    5.11    Even, Odd :: pname
     6.1 --- a/src/HOL/Quot/FRACT.ML	Thu May 04 15:14:56 2000 +0200
     6.2 +++ b/src/HOL/Quot/FRACT.ML	Thu May 04 15:15:37 2000 +0200
     6.3 @@ -11,7 +11,7 @@
     6.4  qed "inst_NP_per";
     6.5  
     6.6  
     6.7 -Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
     6.8 +Goalw [half_def] "half = <[abs_NP(n,#2*n)]>";
     6.9  by (rtac per_class_eqI 1);
    6.10  by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
    6.11  qed "test";