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