src/FOL/ex/Nat.thy
author wenzelm
Tue Mar 05 16:40:12 2019 +0100 (2 months ago ago)
changeset 70047 01732226987a
parent 69602 e65314985426
permissions -rw-r--r--
misc tuning and modernization;
     1 (*  Title:      FOL/ex/Nat.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 *)
     5 
     6 section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
     7 
     8 theory Nat
     9   imports FOL
    10 begin
    11 
    12 typedecl nat
    13 instance nat :: \<open>term\<close> ..
    14 
    15 axiomatization
    16   Zero :: \<open>nat\<close>  (\<open>0\<close>) and
    17   Suc :: \<open>nat \<Rightarrow> nat\<close> and
    18   rec :: \<open>[nat, 'a, [nat, 'a] \<Rightarrow> 'a] \<Rightarrow> 'a\<close>
    19 where
    20   induct: \<open>\<lbrakk>P(0); \<And>x. P(x) \<Longrightarrow> P(Suc(x))\<rbrakk> \<Longrightarrow> P(n)\<close> and
    21   Suc_inject: \<open>Suc(m)=Suc(n) \<Longrightarrow> m=n\<close> and
    22   Suc_neq_0: \<open>Suc(m)=0 \<Longrightarrow> R\<close> and
    23   rec_0: \<open>rec(0,a,f) = a\<close> and
    24   rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m,a,f))\<close>
    25 
    26 definition add :: \<open>[nat, nat] \<Rightarrow> nat\<close>  (infixl \<open>+\<close> 60)
    27   where \<open>m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))\<close>
    28 
    29 
    30 subsection \<open>Proofs about the natural numbers\<close>
    31 
    32 lemma Suc_n_not_n: \<open>Suc(k) \<noteq> k\<close>
    33 apply (rule_tac n = \<open>k\<close> in induct)
    34 apply (rule notI)
    35 apply (erule Suc_neq_0)
    36 apply (rule notI)
    37 apply (erule notE)
    38 apply (erule Suc_inject)
    39 done
    40 
    41 lemma \<open>(k+m)+n = k+(m+n)\<close>
    42 apply (rule induct)
    43 back
    44 back
    45 back
    46 back
    47 back
    48 back
    49 oops
    50 
    51 lemma add_0 [simp]: \<open>0+n = n\<close>
    52 apply (unfold add_def)
    53 apply (rule rec_0)
    54 done
    55 
    56 lemma add_Suc [simp]: \<open>Suc(m)+n = Suc(m+n)\<close>
    57 apply (unfold add_def)
    58 apply (rule rec_Suc)
    59 done
    60 
    61 lemma add_assoc: \<open>(k+m)+n = k+(m+n)\<close>
    62 apply (rule_tac n = \<open>k\<close> in induct)
    63 apply simp
    64 apply simp
    65 done
    66 
    67 lemma add_0_right: \<open>m+0 = m\<close>
    68 apply (rule_tac n = \<open>m\<close> in induct)
    69 apply simp
    70 apply simp
    71 done
    72 
    73 lemma add_Suc_right: \<open>m+Suc(n) = Suc(m+n)\<close>
    74 apply (rule_tac n = \<open>m\<close> in induct)
    75 apply simp_all
    76 done
    77 
    78 lemma
    79   assumes prem: \<open>\<And>n. f(Suc(n)) = Suc(f(n))\<close>
    80   shows \<open>f(i+j) = i+f(j)\<close>
    81 apply (rule_tac n = \<open>i\<close> in induct)
    82 apply simp
    83 apply (simp add: prem)
    84 done
    85 
    86 end