src/Doc/Tutorial/Rules/Forward.thy
author wenzelm
Sun, 20 May 2018 22:04:46 +0200
changeset 68238 eb57621568bb
parent 67406 23307fd33906
permissions -rw-r--r--
avoid undeclared frees;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55159
608c157d743d Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents: 48985
diff changeset
     1
theory Forward imports TPrimes begin
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
     2
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
     3
text\<open>\noindent
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
     4
Forward proof material: of, OF, THEN, simplify, rule_format.
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
     5
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
     6
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
     7
text\<open>\noindent
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
     8
SKIP most developments...
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
     9
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    10
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    11
(** Commutativity **)
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    12
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    13
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 55159
diff changeset
    14
apply (auto simp add: is_gcd_def)
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    15
done
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    16
25261
3dc292be0b54 recdef -> fun
nipkow
parents: 16417
diff changeset
    17
lemma gcd_commute: "gcd m n = gcd n m"
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    18
apply (rule is_gcd_unique)
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    19
apply (rule is_gcd)
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    20
apply (subst is_gcd_commute)
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    21
apply (simp add: is_gcd)
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    22
done
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    23
25261
3dc292be0b54 recdef -> fun
nipkow
parents: 16417
diff changeset
    24
lemma gcd_1 [simp]: "gcd m (Suc 0) = Suc 0"
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    25
apply simp
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    26
done
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    27
25261
3dc292be0b54 recdef -> fun
nipkow
parents: 16417
diff changeset
    28
lemma gcd_1_left [simp]: "gcd (Suc 0) m = Suc 0"
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
    29
apply (simp add: gcd_commute [of "Suc 0"])
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    30
done
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    31
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    32
text\<open>\noindent
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    33
as far as HERE.
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    34
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    35
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    36
text\<open>\noindent
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    37
SKIP THIS PROOF
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    38
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    39
25261
3dc292be0b54 recdef -> fun
nipkow
parents: 16417
diff changeset
    40
lemma gcd_mult_distrib2: "k * gcd m n = gcd (k*m) (k*n)"
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    41
apply (induct_tac m n rule: gcd.induct)
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    42
apply (case_tac "n=0")
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
    43
apply simp
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    44
apply (case_tac "k=0")
45617
cc0800432333 updated proof;
wenzelm
parents: 27658
diff changeset
    45
apply simp_all
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    46
done
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    47
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    48
text \<open>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    49
@{thm[display] gcd_mult_distrib2}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    50
\rulename{gcd_mult_distrib2}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    51
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    52
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    53
text\<open>\noindent
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    54
of, simplified
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    55
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    56
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    57
68238
eb57621568bb avoid undeclared frees;
wenzelm
parents: 67406
diff changeset
    58
lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1] for k
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 55159
diff changeset
    59
lemmas gcd_mult_1 = gcd_mult_0 [simplified]
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    60
14403
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    61
lemmas where1 = gcd_mult_distrib2 [where m=1]
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    62
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    63
lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1]
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    64
68238
eb57621568bb avoid undeclared frees;
wenzelm
parents: 67406
diff changeset
    65
lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] for j k
14403
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    66
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    67
text \<open>
14403
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    68
example using ``of'':
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    69
@{thm[display] gcd_mult_distrib2 [of _ 1]}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    70
14403
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    71
example using ``where'':
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    72
@{thm[display] gcd_mult_distrib2 [where m=1]}
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    73
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    74
example using ``where'', ``and'':
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    75
@{thm[display] gcd_mult_distrib2 [where m=1 and k="j+k"]}
32d1526d3237 new "where" section
paulson
parents: 13550
diff changeset
    76
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    77
@{thm[display] gcd_mult_0}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    78
\rulename{gcd_mult_0}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    79
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    80
@{thm[display] gcd_mult_1}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    81
\rulename{gcd_mult_1}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    82
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    83
@{thm[display] sym}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    84
\rulename{sym}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    85
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    86
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 55159
diff changeset
    87
lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
13550
5a176b8dda84 removal of blast.overloaded
paulson
parents: 12390
diff changeset
    88
      (*not quite right: we need ?k but this gives k*)
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    89
68238
eb57621568bb avoid undeclared frees;
wenzelm
parents: 67406
diff changeset
    90
lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym] for k
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    91
      (*better in one step!*)
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    92
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    93
text \<open>
13550
5a176b8dda84 removal of blast.overloaded
paulson
parents: 12390
diff changeset
    94
more legible, and variables properly generalized
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
    95
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    96
25261
3dc292be0b54 recdef -> fun
nipkow
parents: 16417
diff changeset
    97
lemma gcd_mult [simp]: "gcd k (k*n) = k"
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    98
by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
    99
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   100
68238
eb57621568bb avoid undeclared frees;
wenzelm
parents: 67406
diff changeset
   101
lemmas gcd_self0 = gcd_mult [of k 1, simplified] for k
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   102
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   103
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   104
text \<open>
25264
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   105
@{thm[display] gcd_mult}
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   106
\rulename{gcd_mult}
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   107
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   108
@{thm[display] gcd_self0}
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   109
\rulename{gcd_self0}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   110
\<close>
25264
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   111
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   112
text \<open>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   113
Rules handy with THEN
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   114
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   115
@{thm[display] iffD1}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   116
\rulename{iffD1}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   117
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   118
@{thm[display] iffD2}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   119
\rulename{iffD2}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   120
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   121
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   122
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   123
text \<open>
13550
5a176b8dda84 removal of blast.overloaded
paulson
parents: 12390
diff changeset
   124
again: more legible, and variables properly generalized
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   125
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   126
25261
3dc292be0b54 recdef -> fun
nipkow
parents: 16417
diff changeset
   127
lemma gcd_self [simp]: "gcd k k = k"
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   128
by (rule gcd_mult [of k 1, simplified])
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   129
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   130
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   131
text\<open>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   132
NEXT SECTION: Methods for Forward Proof
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   133
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   134
NEW
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   135
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   136
theorem arg_cong, useful in forward steps
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   137
@{thm[display] arg_cong[no_vars]}
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   138
\rulename{arg_cong}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   139
\<close>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   140
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
   141
lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
12390
2fa13b499975 adapted intr/elim uses;
wenzelm
parents: 12156
diff changeset
   142
apply (intro notI)
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   143
txt\<open>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   144
before using arg_cong
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   145
@{subgoals[display,indent=0,margin=65]}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   146
\<close>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   147
apply (drule_tac f="\<lambda>x. x mod u" in arg_cong)
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   148
txt\<open>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   149
after using arg_cong
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   150
@{subgoals[display,indent=0,margin=65]}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   151
\<close>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   152
apply (simp add: mod_Suc)
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   153
done
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   154
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   155
text\<open>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   156
have just used this rule:
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   157
@{thm[display] mod_Suc[no_vars]}
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   158
\rulename{mod_Suc}
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   159
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   160
@{thm[display] mult_le_mono1[no_vars]}
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   161
\rulename{mult_le_mono1}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   162
\<close>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   163
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   164
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   165
text\<open>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   166
example of "insert"
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   167
\<close>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   168
55159
608c157d743d Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents: 48985
diff changeset
   169
lemma relprime_dvd_mult:
25261
3dc292be0b54 recdef -> fun
nipkow
parents: 16417
diff changeset
   170
      "\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   171
apply (insert gcd_mult_distrib2 [of m k n])
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   172
txt\<open>@{subgoals[display,indent=0,margin=65]}\<close>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   173
apply simp
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   174
txt\<open>@{subgoals[display,indent=0,margin=65]}\<close>
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 55159
diff changeset
   175
apply (erule_tac t="m" in ssubst)
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   176
apply simp
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   177
done
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   178
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   179
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   180
text \<open>
25264
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   181
@{thm[display] relprime_dvd_mult}
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   182
\rulename{relprime_dvd_mult}
7007bc8ddae4 recdef to fun
paulson
parents: 25261
diff changeset
   183
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   184
Another example of "insert"
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   185
64242
93c6f0da5c70 more standardized theorem names for facts involving the div and mod identity
haftmann
parents: 58860
diff changeset
   186
@{thm[display] div_mult_mod_eq}
93c6f0da5c70 more standardized theorem names for facts involving the div and mod identity
haftmann
parents: 58860
diff changeset
   187
\rulename{div_mult_mod_eq}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   188
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   189
11407
138919f1a135 tweaks for new version
paulson
parents: 10958
diff changeset
   190
(*MOVED to Force.thy, which now depends only on Divides.thy
138919f1a135 tweaks for new version
paulson
parents: 10958
diff changeset
   191
lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
138919f1a135 tweaks for new version
paulson
parents: 10958
diff changeset
   192
*)
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   193
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 55159
diff changeset
   194
lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"
27658
674496eb5965 (adjusted)
haftmann
parents: 25264
diff changeset
   195
by (auto intro: relprime_dvd_mult elim: dvdE)
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   196
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 55159
diff changeset
   197
lemma relprime_20_81: "gcd 20 81 = 1"
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   198
by (simp add: gcd.simps)
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   199
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   200
text \<open>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   201
Examples of 'OF'
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   202
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   203
@{thm[display] relprime_dvd_mult}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   204
\rulename{relprime_dvd_mult}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   205
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   206
@{thm[display] relprime_dvd_mult [OF relprime_20_81]}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   207
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   208
@{thm[display] dvd_refl}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   209
\rulename{dvd_refl}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   210
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   211
@{thm[display] dvd_add}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   212
\rulename{dvd_add}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   213
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   214
@{thm[display] dvd_add [OF dvd_refl dvd_refl]}
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   215
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   216
@{thm[display] dvd_add [OF _ dvd_refl]}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   217
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   218
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 55159
diff changeset
   219
lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)"
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
   220
apply (subgoal_tac "z = 34 \<or> z = 36")
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   221
txt\<open>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   222
the tactic leaves two subgoals:
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   223
@{subgoals[display,indent=0,margin=65]}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   224
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   225
apply blast
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
   226
apply (subgoal_tac "z \<noteq> 35")
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   227
txt\<open>
10958
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   228
the tactic leaves two subgoals:
fd582f0d649b arg_cong example; tidying to use @subgoals
paulson
parents: 10877
diff changeset
   229
@{subgoals[display,indent=0,margin=65]}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 64242
diff changeset
   230
\<close>
10846
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   231
apply arith
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   232
apply force
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   233
done
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   234
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   235
623141a08705 reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff changeset
   236
end