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