misc tuning and modernization;
authorwenzelm
Tue Mar 05 16:40:12 2019 +0100 (6 weeks ago ago)
changeset 7004701732226987a
parent 70046 c28da0820b8b
child 70048 3fd9298dd200
misc tuning and modernization;
src/FOL/ex/Nat.thy
src/FOL/ex/Nat_Class.thy
     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 =