src/FOLP/ex/Nat.thy
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 25991 31b38a39e589
child 35762 af3ff2ba4c54
permissions -rw-r--r--
renamed structure Display_Goal to Goal_Display;
clasohm@1477
     1
(*  Title:      FOLP/ex/nat.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1477
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
*)
clasohm@0
     6
wenzelm@17480
     7
header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
wenzelm@17480
     8
wenzelm@17480
     9
theory Nat
wenzelm@17480
    10
imports FOLP
wenzelm@17480
    11
begin
wenzelm@17480
    12
wenzelm@17480
    13
typedecl nat
wenzelm@25991
    14
arities nat :: "term"
wenzelm@25991
    15
wenzelm@25991
    16
consts
wenzelm@25991
    17
  0 :: nat    ("0")
wenzelm@25991
    18
  Suc :: "nat => nat"
wenzelm@25991
    19
  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
wenzelm@25991
    20
  add :: "[nat, nat] => nat"    (infixl "+" 60)
clasohm@0
    21
clasohm@0
    22
  (*Proof terms*)
wenzelm@25991
    23
  nrec :: "[nat, p, [nat, p] => p] => p"
wenzelm@25991
    24
  ninj :: "p => p"
wenzelm@25991
    25
  nneq :: "p => p"
wenzelm@25991
    26
  rec0 :: "p"
wenzelm@25991
    27
  recSuc :: "p"
wenzelm@17480
    28
wenzelm@17480
    29
axioms
wenzelm@17480
    30
  induct:     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
wenzelm@17480
    31
              |] ==> nrec(n,b,c):P(n)"
clasohm@0
    32
wenzelm@17480
    33
  Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
wenzelm@17480
    34
  Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R"
wenzelm@17480
    35
  rec_0:      "rec0 : rec(0,a,f) = a"
wenzelm@17480
    36
  rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
wenzelm@25991
    37
wenzelm@25991
    38
defs
wenzelm@17480
    39
  add_def:    "m+n == rec(m, n, %x y. Suc(y))"
clasohm@0
    40
wenzelm@25991
    41
axioms
wenzelm@17480
    42
  nrecB0:     "b: A ==> nrec(0,b,c) = b : A"
wenzelm@17480
    43
  nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
wenzelm@17480
    44
wenzelm@25991
    45
wenzelm@25991
    46
subsection {* Proofs about the natural numbers *}
wenzelm@25991
    47
wenzelm@25991
    48
lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
wenzelm@25991
    49
apply (rule_tac n = k in induct)
wenzelm@25991
    50
apply (rule notI)
wenzelm@25991
    51
apply (erule Suc_neq_0)
wenzelm@25991
    52
apply (rule notI)
wenzelm@25991
    53
apply (erule notE)
wenzelm@25991
    54
apply (erule Suc_inject)
wenzelm@25991
    55
done
wenzelm@25991
    56
wenzelm@25991
    57
lemma "?p : (k+m)+n = k+(m+n)"
wenzelm@25991
    58
apply (rule induct)
wenzelm@25991
    59
back
wenzelm@25991
    60
back
wenzelm@25991
    61
back
wenzelm@25991
    62
back
wenzelm@25991
    63
back
wenzelm@25991
    64
back
wenzelm@25991
    65
oops
wenzelm@25991
    66
wenzelm@25991
    67
lemma add_0 [simp]: "?p : 0+n = n"
wenzelm@25991
    68
apply (unfold add_def)
wenzelm@25991
    69
apply (rule rec_0)
wenzelm@25991
    70
done
wenzelm@25991
    71
wenzelm@25991
    72
lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
wenzelm@25991
    73
apply (unfold add_def)
wenzelm@25991
    74
apply (rule rec_Suc)
wenzelm@25991
    75
done
wenzelm@25991
    76
wenzelm@25991
    77
wenzelm@25991
    78
lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
wenzelm@25991
    79
  apply (erule subst)
wenzelm@25991
    80
  apply (rule refl)
wenzelm@25991
    81
  done
wenzelm@25991
    82
wenzelm@25991
    83
lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
wenzelm@25991
    84
  apply (erule subst, erule subst, rule refl)
wenzelm@25991
    85
  done
wenzelm@25991
    86
wenzelm@25991
    87
lemmas nat_congs = Suc_cong Plus_cong
wenzelm@25991
    88
wenzelm@25991
    89
ML {*
wenzelm@25991
    90
  val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
wenzelm@25991
    91
*}
wenzelm@25991
    92
wenzelm@25991
    93
lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
wenzelm@25991
    94
apply (rule_tac n = k in induct)
wenzelm@25991
    95
apply (tactic {* SIMP_TAC add_ss 1 *})
wenzelm@25991
    96
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
wenzelm@25991
    97
done
wenzelm@25991
    98
wenzelm@25991
    99
lemma add_0_right: "?p : m+0 = m"
wenzelm@25991
   100
apply (rule_tac n = m in induct)
wenzelm@25991
   101
apply (tactic {* SIMP_TAC add_ss 1 *})
wenzelm@25991
   102
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
wenzelm@25991
   103
done
wenzelm@25991
   104
wenzelm@25991
   105
lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
wenzelm@25991
   106
apply (rule_tac n = m in induct)
wenzelm@25991
   107
apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
wenzelm@25991
   108
done
wenzelm@25991
   109
wenzelm@25991
   110
(*mk_typed_congs appears not to work with FOLP's version of subst*)
wenzelm@17480
   111
clasohm@0
   112
end