author wenzelm Tue Mar 05 16:40:12 2019 +0100 (6 weeks ago ago) changeset 70047 01732226987a parent 70046 c28da0820b8b child 70048 3fd9298dd200
misc tuning and modernization;
 src/FOL/ex/Nat.thy file | annotate | diff | revisions src/FOL/ex/Nat_Class.thy file | annotate | diff | revisions
```     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
```
```     2.1 --- a/src/FOL/ex/Nat_Class.thy	Tue Mar 05 14:45:27 2019 +0100
2.2 +++ b/src/FOL/ex/Nat_Class.thy	Tue Mar 05 16:40:12 2019 +0100
2.3 @@ -2,17 +2,19 @@
2.4      Author:     Markus Wenzel, TU Muenchen
2.5  *)
2.6
2.7 +section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
2.8 +
2.9  theory Nat_Class
2.10 -imports FOL
2.11 +  imports FOL
2.12  begin
2.13
2.14  text \<open>
2.15 -  This is an abstract version of theory \<open>Nat\<close>. Instead of axiomatizing a
2.16 -  single type \<open>nat\<close> we define the class of all these types (up to
2.17 +  This is an abstract version of \<^file>\<open>Nat.thy\<close>. Instead of axiomatizing a
2.18 +  single type \<open>nat\<close>, it defines the class of all these types (up to
2.19    isomorphism).
2.20
2.21 -  Note: The \<open>rec\<close> operator had to be made \<^emph>\<open>monomorphic\<close>, because class axioms
2.22 -  may not contain more than one type variable.
2.23 +  Note: The \<open>rec\<close> operator has been made \<^emph>\<open>monomorphic\<close>, because class
2.24 +  axioms cannot contain more than one type variable.
2.25  \<close>
2.26
2.27  class nat =
```