|
(* Title: FOL/ex/Nat_Class.thy
Author: Markus Wenzel, TU Muenchen
*)
section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close>
theory Nat_Class
imports FOL
begin
text \<open>
This is an abstract version of \<^file>\<open>Nat.thy\<close>. Instead of axiomatizing a
single type \<open>nat\<close>, it defines the class of all these types (up to
isomorphism).
Note: The \<open>rec\<close> operator has been made \<^emph>\<open>monomorphic\<close>, because class
axioms cannot contain more than one type variable.
\<close>
class nat =
fixes Zero :: \<open>'a\<close> (\<open>0\<close>)
and Suc :: \<open>'a \<Rightarrow> 'a\<close>
and rec :: \<open>'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a\<close>
assumes induct: \<open>P(0) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)\<close>
and Suc_inject: \<open>Suc(m) = Suc(n) \<Longrightarrow> m = n\<close>
and Suc_neq_Zero: \<open>Suc(m) = 0 \<Longrightarrow> R\<close>
and rec_Zero: \<open>rec(0, a, f) = a\<close>
and rec_Suc: \<open>rec(Suc(m), a, f) = f(m, rec(m, a, f))\<close>
begin
definition add :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>+\<close> 60)
where \<open>m + n = rec(m, n, \<lambda>x y. Suc(y))\<close>
lemma Suc_n_not_n: \<open>Suc(k) \<noteq> (k::'a)\<close>
apply (rule_tac n = \<open>k\<close> in induct)
apply (rule notI)
apply (erule Suc_neq_Zero)
apply (rule notI)
apply (erule notE)
apply (erule Suc_inject)
done
lemma \<open>(k + m) + n = k + (m + n)\<close>
apply (rule induct)
back
back
back
back
back
oops
lemma add_Zero [simp]: \<open>0 + n = n\<close>
apply (unfold add_def)
apply (rule rec_Zero)
done
lemma add_Suc [simp]: \<open>Suc(m) + n = Suc(m + n)\<close>
apply (unfold add_def)
apply (rule rec_Suc)
done
lemma add_assoc: \<open>(k + m) + n = k + (m + n)\<close>
apply (rule_tac n = \<open>k\<close> in induct)
apply simp
apply simp
done
lemma add_Zero_right: \<open>m + 0 = m\<close>
apply (rule_tac n = \<open>m\<close> in induct)
apply simp
apply simp
done
lemma add_Suc_right: \<open>m + Suc(n) = Suc(m + n)\<close>
apply (rule_tac n = \<open>m\<close> in induct)
apply simp_all
done
lemma
assumes prem: \<open>\<And>n. f(Suc(n)) = Suc(f(n))\<close>
shows \<open>f(i + j) = i + f(j)\<close>
apply (rule_tac n = \<open>i\<close> in induct)
apply simp
apply (simp add: prem)
done
end
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
