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
```