1.1 --- a/doc-src/TutorialI/Rules/Forward.thy Mon Jan 22 11:01:49 2001 +0100
1.2 +++ b/doc-src/TutorialI/Rules/Forward.thy Mon Jan 22 11:02:53 2001 +0100
1.3 @@ -11,23 +11,23 @@
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 - done
1.9 +apply (auto simp add: is_gcd_def);
1.10 +done
1.11
1.12 lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
1.13 - apply (rule is_gcd_unique)
1.14 - apply (rule is_gcd)
1.15 - apply (subst is_gcd_commute)
1.16 - apply (simp add: is_gcd)
1.17 - done
1.18 +apply (rule is_gcd_unique)
1.19 +apply (rule is_gcd)
1.20 +apply (subst is_gcd_commute)
1.21 +apply (simp add: is_gcd)
1.22 +done
1.23
1.24 lemma gcd_1 [simp]: "gcd(m,1) = 1"
1.25 - apply (simp)
1.26 - done
1.27 +apply simp
1.28 +done
1.29
1.30 lemma gcd_1_left [simp]: "gcd(1,m) = 1"
1.31 - apply (simp add: gcd_commute [of 1])
1.32 - done
1.33 +apply (simp add: gcd_commute [of 1])
1.34 +done
1.35
1.36 text{*\noindent
1.37 as far as HERE.
1.38 @@ -49,7 +49,7 @@
1.39 lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
1.40 apply (induct_tac m n rule: gcd.induct)
1.41 apply (case_tac "n=0")
1.42 -apply (simp)
1.43 +apply simp
1.44 apply (case_tac "k=0")
1.45 apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
1.46 done
1.47 @@ -115,12 +115,50 @@
1.48 by (rule gcd_mult [of k 1, simplified])
1.49
1.50
1.51 +text{*
1.52 +NEXT SECTION: Methods for Forward Proof
1.53 +
1.54 +NEW
1.55 +
1.56 +theorem arg_cong, useful in forward steps
1.57 +@{thm[display] arg_cong[no_vars]}
1.58 +\rulename{arg_cong}
1.59 +*}
1.60 +
1.61 +lemma "#2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
1.62 +apply intro
1.63 +txt{*
1.64 +before using arg_cong
1.65 +@{subgoals[display,indent=0,margin=65]}
1.66 +*};
1.67 +apply (drule_tac f="\<lambda>x. x mod u" in arg_cong)
1.68 +txt{*
1.69 +after using arg_cong
1.70 +@{subgoals[display,indent=0,margin=65]}
1.71 +*};
1.72 +apply (simp add: mod_Suc)
1.73 +done
1.74 +
1.75 +text{*
1.76 +have just used this rule:
1.77 +@{thm[display] mod_Suc[no_vars]}
1.78 +\rulename{mod_Suc}
1.79 +
1.80 +@{thm[display] mult_le_mono1[no_vars]}
1.81 +\rulename{mult_le_mono1}
1.82 +*}
1.83 +
1.84 +
1.85 +text{*
1.86 +example of "insert"
1.87 +*}
1.88 +
1.89 lemma relprime_dvd_mult:
1.90 "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m";
1.91 apply (insert gcd_mult_distrib2 [of m k n])
1.92 -apply (simp)
1.93 +apply simp
1.94 apply (erule_tac t="m" in ssubst);
1.95 -apply (simp)
1.96 +apply simp
1.97 done
1.98
1.99
1.100 @@ -134,7 +172,7 @@
1.101 lemma div_mult_self_is_m:
1.102 "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
1.103 apply (insert mod_div_equality [of "m*n" n])
1.104 -apply (simp)
1.105 +apply simp
1.106 done
1.107
1.108 lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
1.109 @@ -144,13 +182,6 @@
1.110 lemma relprime_20_81: "gcd(#20,#81) = 1";
1.111 by (simp add: gcd.simps)
1.112
1.113 -text{*example of arg_cong (NEW)
1.114 -
1.115 -@{thm[display] arg_cong[no_vars]}
1.116 -\rulename{arg_cong}
1.117 -*}
1.118 -
1.119 -
1.120 text {*
1.121 Examples of 'OF'
1.122
1.123 @@ -172,36 +203,19 @@
1.124
1.125 lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)";
1.126 apply (subgoal_tac "z = #34 \<or> z = #36")
1.127 +txt{*
1.128 +the tactic leaves two subgoals:
1.129 +@{subgoals[display,indent=0,margin=65]}
1.130 +*};
1.131 apply blast
1.132 apply (subgoal_tac "z \<noteq> #35")
1.133 +txt{*
1.134 +the tactic leaves two subgoals:
1.135 +@{subgoals[display,indent=0,margin=65]}
1.136 +*};
1.137 apply arith
1.138 apply force
1.139 done
1.140
1.141 -text
1.142 -{*
1.143 -proof\ (prove):\ step\ 1\isanewline
1.144 -\isanewline
1.145 -goal\ (lemma):\isanewline
1.146 -\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline
1.147 -\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
1.148 -\ \ \ \ \ \ \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isasymrbrakk \isanewline
1.149 -\ \ \ \ \isasymLongrightarrow \ Q\ z\isanewline
1.150 -\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline
1.151 -\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36
1.152 -
1.153 -
1.154 -
1.155 -proof\ (prove):\ step\ 3\isanewline
1.156 -\isanewline
1.157 -goal\ (lemma):\isanewline
1.158 -\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline
1.159 -\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
1.160 -\ \ \ \ \ \ \ z\ \isasymnoteq \ \#35\isasymrbrakk \isanewline
1.161 -\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isanewline
1.162 -\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline
1.163 -\ \ \ \ \isasymLongrightarrow \ z\ \isasymnoteq \ \#35
1.164 -*}
1.165 -
1.166
1.167 end