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