src/FOL/ex/Nat.thy
changeset 70047 01732226987a
parent 69602 e65314985426
     1.1 --- a/src/FOL/ex/Nat.thy	Tue Mar 05 14:45:27 2019 +0100
     1.2 +++ b/src/FOL/ex/Nat.thy	Tue Mar 05 16:40:12 2019 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
     1.5  
     1.6  theory Nat
     1.7 -imports FOL
     1.8 +  imports FOL
     1.9  begin
    1.10  
    1.11  typedecl nat
    1.12 @@ -14,17 +14,17 @@
    1.13  
    1.14  axiomatization
    1.15    Zero :: \<open>nat\<close>  (\<open>0\<close>) and
    1.16 -  Suc :: \<open>nat => nat\<close> and
    1.17 -  rec :: \<open>[nat, 'a, [nat, 'a] => 'a] => 'a\<close>
    1.18 +  Suc :: \<open>nat \<Rightarrow> nat\<close> and
    1.19 +  rec :: \<open>[nat, 'a, [nat, 'a] \<Rightarrow> 'a] \<Rightarrow> 'a\<close>
    1.20  where
    1.21 -  induct: \<open>[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)\<close> and
    1.22 -  Suc_inject: \<open>Suc(m)=Suc(n) ==> m=n\<close> and
    1.23 -  Suc_neq_0: \<open>Suc(m)=0 ==> R\<close> and
    1.24 +  induct: \<open>\<lbrakk>P(0); \<And>x. P(x) \<Longrightarrow> P(Suc(x))\<rbrakk> \<Longrightarrow> P(n)\<close> and
    1.25 +  Suc_inject: \<open>Suc(m)=Suc(n) \<Longrightarrow> m=n\<close> and
    1.26 +  Suc_neq_0: \<open>Suc(m)=0 \<Longrightarrow> R\<close> and
    1.27    rec_0: \<open>rec(0,a,f) = a\<close> and
    1.28    rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m,a,f))\<close>
    1.29  
    1.30 -definition add :: \<open>[nat, nat] => nat\<close>  (infixl \<open>+\<close> 60)
    1.31 -  where \<open>m + n == rec(m, n, %x y. Suc(y))\<close>
    1.32 +definition add :: \<open>[nat, nat] \<Rightarrow> nat\<close>  (infixl \<open>+\<close> 60)
    1.33 +  where \<open>m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))\<close>
    1.34  
    1.35  
    1.36  subsection \<open>Proofs about the natural numbers\<close>
    1.37 @@ -76,7 +76,7 @@
    1.38  done
    1.39  
    1.40  lemma
    1.41 -  assumes prem: \<open>!!n. f(Suc(n)) = Suc(f(n))\<close>
    1.42 +  assumes prem: \<open>\<And>n. f(Suc(n)) = Suc(f(n))\<close>
    1.43    shows \<open>f(i+j) = i+f(j)\<close>
    1.44  apply (rule_tac n = \<open>i\<close> in induct)
    1.45  apply simp