src/HOL/NatArith.thy
author paulson
Fri, 29 Oct 2004 15:16:02 +0200
changeset 15270 8b3f707a78a7
parent 15140 322485b816ac
child 15404 a9a762f586b5
permissions -rw-r--r--
fixed reference to renamed theorem
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/NatArith.thy
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
13297
wenzelm
parents: 11655
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel
wenzelm
parents: 11655
diff changeset
     4
*)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     5
13297
wenzelm
parents: 11655
diff changeset
     6
header {* More arithmetic on natural numbers *}
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15048
diff changeset
     8
theory NatArith
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     9
imports Nat
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15048
diff changeset
    10
files "arith_data.ML"
c69542757a4d New theory header syntax.
nipkow
parents: 15048
diff changeset
    11
begin
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    12
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    13
setup arith_setup
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    14
13297
wenzelm
parents: 11655
diff changeset
    15
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11454
diff changeset
    16
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
14208
144f45277d5a misc tidying
paulson
parents: 13499
diff changeset
    17
by (simp add: less_eq reflcl_trancl [symmetric]
144f45277d5a misc tidying
paulson
parents: 13499
diff changeset
    18
            del: reflcl_trancl, arith)
11454
7514e5e21cb8 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents: 11324
diff changeset
    19
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    20
lemma nat_diff_split:
10599
2df753cf86e9 miniscoping of nat_diff_split
paulson
parents: 10214
diff changeset
    21
    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
13297
wenzelm
parents: 11655
diff changeset
    22
    -- {* elimination of @{text -} on @{text nat} *}
wenzelm
parents: 11655
diff changeset
    23
  by (cases "a<b" rule: case_split)
wenzelm
parents: 11655
diff changeset
    24
    (auto simp add: diff_is_0_eq [THEN iffD2])
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    25
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    26
lemma nat_diff_split_asm:
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    27
    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
13297
wenzelm
parents: 11655
diff changeset
    28
    -- {* elimination of @{text -} on @{text nat} in assumptions *}
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    29
  by (simp split: nat_diff_split)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    30
11164
03f5dc539fd9 added add_arith (just as hint by now)
oheimb
parents: 10599
diff changeset
    31
ML {*
03f5dc539fd9 added add_arith (just as hint by now)
oheimb
parents: 10599
diff changeset
    32
 val nat_diff_split = thm "nat_diff_split";
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    33
 val nat_diff_split_asm = thm "nat_diff_split_asm";
13499
f95f5818f24f Counter example generation mods.
nipkow
parents: 13297
diff changeset
    34
*}
f95f5818f24f Counter example generation mods.
nipkow
parents: 13297
diff changeset
    35
(* Careful: arith_tac produces counter examples!
11181
d04f57b91166 renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents: 11164
diff changeset
    36
fun add_arith cs = cs addafter ("arith_tac", arith_tac);
14607
099575a938e5 tuned document;
wenzelm
parents: 14208
diff changeset
    37
TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    38
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    39
lemmas [arith_split] = nat_diff_split split_min split_max
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    40
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    41
end