src/FOL/ex/Nat_Class.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@29752
     1
(*  Title:      FOL/ex/Nat_Class.thy
wenzelm@1246
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@1246
     3
*)
wenzelm@1246
     4
wenzelm@70047
     5
section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
wenzelm@70047
     6
wenzelm@29752
     7
theory Nat_Class
wenzelm@70047
     8
  imports FOL
wenzelm@17245
     9
begin
wenzelm@17245
    10
wenzelm@60770
    11
text \<open>
wenzelm@70047
    12
  This is an abstract version of \<^file>\<open>Nat.thy\<close>. Instead of axiomatizing a
wenzelm@70047
    13
  single type \<open>nat\<close>, it defines the class of all these types (up to
wenzelm@69593
    14
  isomorphism).
wenzelm@17245
    15
wenzelm@70047
    16
  Note: The \<open>rec\<close> operator has been made \<^emph>\<open>monomorphic\<close>, because class
wenzelm@70047
    17
  axioms cannot contain more than one type variable.
wenzelm@60770
    18
\<close>
wenzelm@1246
    19
wenzelm@29751
    20
class nat =
wenzelm@69602
    21
  fixes Zero :: \<open>'a\<close>  (\<open>0\<close>)
wenzelm@69602
    22
    and Suc :: \<open>'a \<Rightarrow> 'a\<close>
wenzelm@69602
    23
    and rec :: \<open>'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a\<close>
wenzelm@69602
    24
  assumes induct: \<open>P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)\<close>
wenzelm@69602
    25
    and Suc_inject: \<open>Suc(m) = Suc(n) \<Longrightarrow> m = n\<close>
wenzelm@69602
    26
    and Suc_neq_Zero: \<open>Suc(m) = 0 \<Longrightarrow> R\<close>
wenzelm@69602
    27
    and rec_Zero: \<open>rec(0, a, f) = a\<close>
wenzelm@69602
    28
    and rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m, a, f))\<close>
wenzelm@29751
    29
begin
wenzelm@1246
    30
wenzelm@69602
    31
definition add :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixl \<open>+\<close> 60)
wenzelm@69602
    32
  where \<open>m + n = rec(m, n, \<lambda>x y. Suc(y))\<close>
wenzelm@19819
    33
wenzelm@69602
    34
lemma Suc_n_not_n: \<open>Suc(k) \<noteq> (k::'a)\<close>
wenzelm@69602
    35
  apply (rule_tac n = \<open>k\<close> in induct)
wenzelm@29751
    36
   apply (rule notI)
wenzelm@29751
    37
   apply (erule Suc_neq_Zero)
wenzelm@29751
    38
  apply (rule notI)
wenzelm@29751
    39
  apply (erule notE)
wenzelm@29751
    40
  apply (erule Suc_inject)
wenzelm@29751
    41
  done
wenzelm@19819
    42
wenzelm@69602
    43
lemma \<open>(k + m) + n = k + (m + n)\<close>
wenzelm@29751
    44
  apply (rule induct)
wenzelm@29751
    45
  back
wenzelm@29751
    46
  back
wenzelm@29751
    47
  back
wenzelm@29751
    48
  back
wenzelm@29751
    49
  back
wenzelm@29751
    50
  oops
wenzelm@19819
    51
wenzelm@69602
    52
lemma add_Zero [simp]: \<open>0 + n = n\<close>
wenzelm@29751
    53
  apply (unfold add_def)
wenzelm@29751
    54
  apply (rule rec_Zero)
wenzelm@29751
    55
  done
wenzelm@1246
    56
wenzelm@69602
    57
lemma add_Suc [simp]: \<open>Suc(m) + n = Suc(m + n)\<close>
wenzelm@29751
    58
  apply (unfold add_def)
wenzelm@29751
    59
  apply (rule rec_Suc)
wenzelm@29751
    60
  done
wenzelm@19819
    61
wenzelm@69602
    62
lemma add_assoc: \<open>(k + m) + n = k + (m + n)\<close>
wenzelm@69602
    63
  apply (rule_tac n = \<open>k\<close> in induct)
wenzelm@29751
    64
   apply simp
wenzelm@29751
    65
  apply simp
wenzelm@29751
    66
  done
wenzelm@19819
    67
wenzelm@69602
    68
lemma add_Zero_right: \<open>m + 0 = m\<close>
wenzelm@69602
    69
  apply (rule_tac n = \<open>m\<close> in induct)
wenzelm@29751
    70
   apply simp
wenzelm@29751
    71
  apply simp
wenzelm@29751
    72
  done
wenzelm@19819
    73
wenzelm@69602
    74
lemma add_Suc_right: \<open>m + Suc(n) = Suc(m + n)\<close>
wenzelm@69602
    75
  apply (rule_tac n = \<open>m\<close> in induct)
wenzelm@29751
    76
   apply simp_all
wenzelm@29751
    77
  done
wenzelm@19819
    78
wenzelm@19819
    79
lemma
wenzelm@69602
    80
  assumes prem: \<open>\<And>n. f(Suc(n)) = Suc(f(n))\<close>
wenzelm@69602
    81
  shows \<open>f(i + j) = i + f(j)\<close>
wenzelm@69602
    82
  apply (rule_tac n = \<open>i\<close> in induct)
wenzelm@29751
    83
   apply simp
wenzelm@29751
    84
  apply (simp add: prem)
wenzelm@29751
    85
  done
wenzelm@1246
    86
wenzelm@1246
    87
end
wenzelm@29751
    88
wenzelm@29751
    89
end