src/Doc/Tutorial/Rules/Forward.thy
changeset 68238 eb57621568bb
parent 67406 23307fd33906
equal deleted inserted replaced
68237:e7c85e2dc198 68238:eb57621568bb
    53 text\<open>\noindent
    53 text\<open>\noindent
    54 of, simplified
    54 of, simplified
    55 \<close>
    55 \<close>
    56 
    56 
    57 
    57 
    58 lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
    58 lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1] for k
    59 lemmas gcd_mult_1 = gcd_mult_0 [simplified]
    59 lemmas gcd_mult_1 = gcd_mult_0 [simplified]
    60 
    60 
    61 lemmas where1 = gcd_mult_distrib2 [where m=1]
    61 lemmas where1 = gcd_mult_distrib2 [where m=1]
    62 
    62 
    63 lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1]
    63 lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1]
    64 
    64 
    65 lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"]
    65 lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] for j k
    66 
    66 
    67 text \<open>
    67 text \<open>
    68 example using ``of'':
    68 example using ``of'':
    69 @{thm[display] gcd_mult_distrib2 [of _ 1]}
    69 @{thm[display] gcd_mult_distrib2 [of _ 1]}
    70 
    70 
    85 \<close>
    85 \<close>
    86 
    86 
    87 lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
    87 lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
    88       (*not quite right: we need ?k but this gives k*)
    88       (*not quite right: we need ?k but this gives k*)
    89 
    89 
    90 lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
    90 lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym] for k
    91       (*better in one step!*)
    91       (*better in one step!*)
    92 
    92 
    93 text \<open>
    93 text \<open>
    94 more legible, and variables properly generalized
    94 more legible, and variables properly generalized
    95 \<close>
    95 \<close>
    96 
    96 
    97 lemma gcd_mult [simp]: "gcd k (k*n) = k"
    97 lemma gcd_mult [simp]: "gcd k (k*n) = k"
    98 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
    98 by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
    99 
    99 
   100 
   100 
   101 lemmas gcd_self0 = gcd_mult [of k 1, simplified]
   101 lemmas gcd_self0 = gcd_mult [of k 1, simplified] for k
   102 
   102 
   103 
   103 
   104 text \<open>
   104 text \<open>
   105 @{thm[display] gcd_mult}
   105 @{thm[display] gcd_mult}
   106 \rulename{gcd_mult}
   106 \rulename{gcd_mult}