src/HOL/NumberTheory/EulerFermat.ML
changeset 9572 bfee45ac5d38
parent 9508 4d01dbf6ded7
child 9634 61b57cc1cb5a
equal deleted inserted replaced
9571:c869d1886a32 9572:bfee45ac5d38
    86 Goal "a <= b - #1 ==> a < (b::int)";
    86 Goal "a <= b - #1 ==> a < (b::int)";
    87 by Auto_tac;
    87 by Auto_tac;
    88 val lemma = result();
    88 val lemma = result();
    89 
    89 
    90 Goalw [norRRset_def]
    90 Goalw [norRRset_def]
    91       "[| #1<m; zgcd(a,m) = #1 |] ==> (EX! b. [a = b](mod m) & b:(norRRset m))";
    91      "[| #1<m; zgcd(a,m) = #1 |] ==> (EX! b. [a = b](mod m) & b:(norRRset m))";
    92 by (cut_inst_tac [("a","a"),("m","m")] zcong_zless_unique 1);
    92 by (cut_inst_tac [("a","a"),("m","m")] zcong_zless_unique 1);
    93 by Auto_tac;
    93 by Auto_tac;
    94 by (res_inst_tac [("m","m")] zcong_zless_imp_eq 2);
    94 by (res_inst_tac [("m","m")] zcong_zless_imp_eq 2);
    95 by (auto_tac (claset() addIs [Bnor_mem_zle,Bnor_mem_zg,zcong_trans,
    95 by (auto_tac (claset() addIs [Bnor_mem_zle,Bnor_mem_zg,zcong_trans,
    96                               zless_imp_zle,lemma],
    96                               zless_imp_zle,lemma],
   145 by (rtac RsetR_zmult_mono 1);
   145 by (rtac RsetR_zmult_mono 1);
   146 by (rtac Bnor_in_RsetR 1);
   146 by (rtac Bnor_in_RsetR 1);
   147 by (ALLGOALS Asm_simp_tac);
   147 by (ALLGOALS Asm_simp_tac);
   148 qed "noX_is_RRset";
   148 qed "noX_is_RRset";
   149 
   149 
   150 Goal "EX! a. P a ==> P (@ a. P a)";
       
   151 by Auto_tac;
       
   152 by (stac select_equality 1);
       
   153 by Auto_tac;
       
   154 val lemma = result();
       
   155 
       
   156 Goal "[| #1<m; is_RRset A m; a:A |] \
   150 Goal "[| #1<m; is_RRset A m; a:A |] \
   157 \    ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
   151 \    ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
   158 \        (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
   152 \        (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
   159 by (rtac lemma 1);
   153 by (rtac (norR_mem_unique RS ex1_implies_ex RS ex_someI) 1);
   160 by (rtac norR_mem_unique 1);
       
   161 by (rtac RRset_gcd 2);
   154 by (rtac RRset_gcd 2);
   162 by (ALLGOALS Asm_simp_tac);
   155 by (ALLGOALS Asm_simp_tac);
   163 val lemma_some = result();
   156 val lemma_some = result();
   164 
   157 
   165 Goalw [RRset2norRR_def]
   158 Goalw [RRset2norRR_def]