src/HOL/Hoare/Arith2.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14353 79f9fbef9106
child 17278 f27456a2a975
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/Hoare/Arith2.ML
     2     ID:         $Id$
     3     Author:     Norbert Galm
     4     Copyright   1995 TUM
     5 
     6 More arithmetic lemmas.
     7 *)
     8 
     9 open Arith2;
    10 
    11 
    12 (*** cd ***)
    13 
    14 
    15 Goalw [cd_def] "0<n ==> cd n n n";
    16 by (Asm_simp_tac 1);
    17 qed "cd_nnn";
    18 
    19 Goalw [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n";
    20 by (blast_tac (claset() addIs [dvd_imp_le]) 1);
    21 qed "cd_le";
    22 
    23 Goalw [cd_def] "cd x m n = cd x n m";
    24 by (Fast_tac 1);
    25 qed "cd_swap";
    26 
    27 Goalw [cd_def] "n<=m ==> cd x m n = cd x (m-n) n";
    28 by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
    29 qed "cd_diff_l";
    30 
    31 Goalw [cd_def] "m<=n ==> cd x m n = cd x m (n-m)";
    32 by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
    33 qed "cd_diff_r";
    34 
    35 
    36 (*** gcd ***)
    37 
    38 Goalw [gcd_def] "0<n ==> n = gcd n n";
    39 by (ftac cd_nnn 1);
    40 by (rtac (some_equality RS sym) 1);
    41 by (blast_tac (claset() addDs [cd_le]) 1);
    42 by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);
    43 qed "gcd_nnn";
    44 
    45 val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
    46 by (simp_tac (simpset() addsimps [cd_swap]) 1);
    47 qed "gcd_swap";
    48 
    49 Goalw [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n";
    50 by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1);
    51 by (Asm_simp_tac 1);
    52 by (rtac allI 1);
    53 by (etac cd_diff_l 1);
    54 qed "gcd_diff_l";
    55 
    56 Goalw [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)";
    57 by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1);
    58 by (Asm_simp_tac 1);
    59 by (rtac allI 1);
    60 by (etac cd_diff_r 1);
    61 qed "gcd_diff_r";
    62 
    63 
    64 (*** pow ***)
    65 
    66 Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
    67 by (asm_simp_tac (simpset() addsimps [power2_eq_square RS sym, 
    68                    power_mult RS sym, mult_div_cancel]) 1);
    69 qed "sq_pow_div2";
    70 Addsimps [sq_pow_div2];