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