src/Doc/Tutorial/Rules/Forward.thy
changeset 58860 fee7cfa69c50
parent 55159 608c157d743d
child 64242 93c6f0da5c70
     1.1 --- a/src/Doc/Tutorial/Rules/Forward.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Rules/Forward.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  (** Commutativity **)
     1.5  
     1.6  lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
     1.7 -apply (auto simp add: is_gcd_def);
     1.8 +apply (auto simp add: is_gcd_def)
     1.9  done
    1.10  
    1.11  lemma gcd_commute: "gcd m n = gcd n m"
    1.12 @@ -48,15 +48,15 @@
    1.13  text {*
    1.14  @{thm[display] gcd_mult_distrib2}
    1.15  \rulename{gcd_mult_distrib2}
    1.16 -*};
    1.17 +*}
    1.18  
    1.19  text{*\noindent
    1.20  of, simplified
    1.21  *}
    1.22  
    1.23  
    1.24 -lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1];
    1.25 -lemmas gcd_mult_1 = gcd_mult_0 [simplified];
    1.26 +lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
    1.27 +lemmas gcd_mult_1 = gcd_mult_0 [simplified]
    1.28  
    1.29  lemmas where1 = gcd_mult_distrib2 [where m=1]
    1.30  
    1.31 @@ -82,23 +82,23 @@
    1.32  
    1.33  @{thm[display] sym}
    1.34  \rulename{sym}
    1.35 -*};
    1.36 +*}
    1.37  
    1.38 -lemmas gcd_mult0 = gcd_mult_1 [THEN sym];
    1.39 +lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
    1.40        (*not quite right: we need ?k but this gives k*)
    1.41  
    1.42 -lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
    1.43 +lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
    1.44        (*better in one step!*)
    1.45  
    1.46  text {*
    1.47  more legible, and variables properly generalized
    1.48 -*};
    1.49 +*}
    1.50  
    1.51  lemma gcd_mult [simp]: "gcd k (k*n) = k"
    1.52  by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
    1.53  
    1.54  
    1.55 -lemmas gcd_self0 = gcd_mult [of k 1, simplified];
    1.56 +lemmas gcd_self0 = gcd_mult [of k 1, simplified]
    1.57  
    1.58  
    1.59  text {*
    1.60 @@ -107,7 +107,7 @@
    1.61  
    1.62  @{thm[display] gcd_self0}
    1.63  \rulename{gcd_self0}
    1.64 -*};
    1.65 +*}
    1.66  
    1.67  text {*
    1.68  Rules handy with THEN
    1.69 @@ -117,12 +117,12 @@
    1.70  
    1.71  @{thm[display] iffD2}
    1.72  \rulename{iffD2}
    1.73 -*};
    1.74 +*}
    1.75  
    1.76  
    1.77  text {*
    1.78  again: more legible, and variables properly generalized
    1.79 -*};
    1.80 +*}
    1.81  
    1.82  lemma gcd_self [simp]: "gcd k k = k"
    1.83  by (rule gcd_mult [of k 1, simplified])
    1.84 @@ -143,12 +143,12 @@
    1.85  txt{*
    1.86  before using arg_cong
    1.87  @{subgoals[display,indent=0,margin=65]}
    1.88 -*};
    1.89 +*}
    1.90  apply (drule_tac f="\<lambda>x. x mod u" in arg_cong)
    1.91  txt{*
    1.92  after using arg_cong
    1.93  @{subgoals[display,indent=0,margin=65]}
    1.94 -*};
    1.95 +*}
    1.96  apply (simp add: mod_Suc)
    1.97  done
    1.98  
    1.99 @@ -172,7 +172,7 @@
   1.100  txt{*@{subgoals[display,indent=0,margin=65]}*}
   1.101  apply simp
   1.102  txt{*@{subgoals[display,indent=0,margin=65]}*}
   1.103 -apply (erule_tac t="m" in ssubst);
   1.104 +apply (erule_tac t="m" in ssubst)
   1.105  apply simp
   1.106  done
   1.107  
   1.108 @@ -185,16 +185,16 @@
   1.109  
   1.110  @{thm[display] mod_div_equality}
   1.111  \rulename{mod_div_equality}
   1.112 -*};
   1.113 +*}
   1.114  
   1.115  (*MOVED to Force.thy, which now depends only on Divides.thy
   1.116  lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
   1.117  *)
   1.118  
   1.119 -lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
   1.120 +lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"
   1.121  by (auto intro: relprime_dvd_mult elim: dvdE)
   1.122  
   1.123 -lemma relprime_20_81: "gcd 20 81 = 1";
   1.124 +lemma relprime_20_81: "gcd 20 81 = 1"
   1.125  by (simp add: gcd.simps)
   1.126  
   1.127  text {*
   1.128 @@ -214,20 +214,20 @@
   1.129  @{thm[display] dvd_add [OF dvd_refl dvd_refl]}
   1.130  
   1.131  @{thm[display] dvd_add [OF _ dvd_refl]}
   1.132 -*};
   1.133 +*}
   1.134  
   1.135 -lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)";
   1.136 +lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)"
   1.137  apply (subgoal_tac "z = 34 \<or> z = 36")
   1.138  txt{*
   1.139  the tactic leaves two subgoals:
   1.140  @{subgoals[display,indent=0,margin=65]}
   1.141 -*};
   1.142 +*}
   1.143  apply blast
   1.144  apply (subgoal_tac "z \<noteq> 35")
   1.145  txt{*
   1.146  the tactic leaves two subgoals:
   1.147  @{subgoals[display,indent=0,margin=65]}
   1.148 -*};
   1.149 +*}
   1.150  apply arith
   1.151  apply force
   1.152  done