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