# HG changeset patch
# User wenzelm
# Date 1484758612 -3600
# Node ID 31044168af84dc23f4c0a8c28a5f97f2f65c3608
# Parent  7e0c8924dfdac83a6a36ade873ff90afb82b7c9c
clarified theory name;
tuned;

diff -r 7e0c8924dfda -r 31044168af84 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Jan 18 15:57:00 2017 +0000
+++ b/src/HOL/ROOT	Wed Jan 18 17:56:52 2017 +0100
@@ -541,7 +541,7 @@
     Adhoc_Overloading_Examples
     Iff_Oracle
     Coercion_Examples
-    Abstract_NAT
+    Peano_Axioms
     Guess
     Functions
     Induction_Schema
diff -r 7e0c8924dfda -r 31044168af84 src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Wed Jan 18 15:57:00 2017 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-(*  Title:      HOL/ex/Abstract_NAT.thy
-    Author:     Makarius
-*)
-
-section \<open>Abstract Natural Numbers primitive recursion\<close>
-
-theory Abstract_NAT
-imports Main
-begin
-
-text \<open>Axiomatic Natural Numbers (Peano) -- a monomorphic theory.\<close>
-
-locale NAT =
-  fixes zero :: 'n
-    and succ :: "'n \<Rightarrow> 'n"
-  assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n"
-    and succ_neq_zero [simp]: "succ m \<noteq> zero"
-    and induct [case_names zero succ, induct type: 'n]:
-      "P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n"
-begin
-
-lemma zero_neq_succ [simp]: "zero \<noteq> succ m"
-  by (rule succ_neq_zero [symmetric])
-
-
-text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>
-
-inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
-  for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
-where
-  Rec_zero: "Rec e r zero e"
-| Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
-
-lemma Rec_functional:
-  fixes x :: 'n
-  shows "\<exists>!y::'a. Rec e r x y"
-proof -
-  let ?R = "Rec e r"
-  show ?thesis
-  proof (induct x)
-    case zero
-    show "\<exists>!y. ?R zero y"
-    proof
-      show "?R zero e" ..
-      show "y = e" if "?R zero y" for y
-        using that by cases simp_all
-    qed
-  next
-    case (succ m)
-    from \<open>\<exists>!y. ?R m y\<close>
-    obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'"
-      by blast
-    show "\<exists>!z. ?R (succ m) z"
-    proof
-      from y show "?R (succ m) (r m y)" ..
-    next
-      fix z
-      assume "?R (succ m) z"
-      then obtain u where "z = r m u" and "?R m u"
-        by cases simp_all
-      with yy' show "z = r m y"
-        by (simp only:)
-    qed
-  qed
-qed
-
-
-text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
-
-definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
-  where "rec e r x = (THE y. Rec e r x y)"
-
-lemma rec_eval:
-  assumes Rec: "Rec e r x y"
-  shows "rec e r x = y"
-  unfolding rec_def
-  using Rec_functional and Rec by (rule the1_equality)
-
-lemma rec_zero [simp]: "rec e r zero = e"
-proof (rule rec_eval)
-  show "Rec e r zero e" ..
-qed
-
-lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
-proof (rule rec_eval)
-  let ?R = "Rec e r"
-  have "?R m (rec e r m)"
-    unfolding rec_def using Rec_functional by (rule theI')
-  then show "?R (succ m) (r m (rec e r m))" ..
-qed
-
-
-text \<open>\<^medskip> Example: addition (monomorphic)\<close>
-
-definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
-  where "add m n = rec n (\<lambda>_ k. succ k) m"
-
-lemma add_zero [simp]: "add zero n = n"
-  and add_succ [simp]: "add (succ m) n = succ (add m n)"
-  unfolding add_def by simp_all
-
-lemma add_assoc: "add (add k m) n = add k (add m n)"
-  by (induct k) simp_all
-
-lemma add_zero_right: "add m zero = m"
-  by (induct m) simp_all
-
-lemma add_succ_right: "add m (succ n) = succ (add m n)"
-  by (induct m) simp_all
-
-lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
-    succ (succ (succ (succ (succ zero))))"
-  by simp
-
-
-text \<open>\<^medskip> Example: replication (polymorphic)\<close>
-
-definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
-  where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
-
-lemma repl_zero [simp]: "repl zero x = []"
-  and repl_succ [simp]: "repl (succ n) x = x # repl n x"
-  unfolding repl_def by simp_all
-
-lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
-  by simp
-
-end
-
-
-text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
-
-interpretation NAT 0 Suc
-proof (rule NAT.intro)
-  fix m n
-  show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
-  show "Suc m \<noteq> 0" by simp
-  show "P n"
-    if zero: "P 0"
-    and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
-    for P
-  proof (induct n)
-    case 0
-    show ?case by (rule zero)
-  next
-    case Suc
-    then show ?case by (rule succ)
-  qed
-qed
-
-end
diff -r 7e0c8924dfda -r 31044168af84 src/HOL/ex/Peano_Axioms.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Peano_Axioms.thy	Wed Jan 18 17:56:52 2017 +0100
@@ -0,0 +1,143 @@
+section \<open>Peano's axioms for Natural Numbers\<close>
+
+theory Peano_Axioms
+  imports Main
+begin
+
+locale peano =
+  fixes zero :: 'n
+  fixes succ :: "'n \<Rightarrow> 'n"
+  assumes succ_neq_zero [simp]: "succ m \<noteq> zero"
+  assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n"
+  assumes induct [case_names zero succ, induct type: 'n]:
+    "P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n"
+begin
+
+lemma zero_neq_succ [simp]: "zero \<noteq> succ m"
+  by (rule succ_neq_zero [symmetric])
+
+
+text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>
+
+inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
+  for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+  Rec_zero: "Rec e r zero e"
+| Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
+
+lemma Rec_functional: "\<exists>!y::'a. Rec e r x y" for x :: 'n
+proof -
+  let ?R = "Rec e r"
+  show ?thesis
+  proof (induct x)
+    case zero
+    show "\<exists>!y. ?R zero y"
+    proof
+      show "?R zero e" ..
+      show "y = e" if "?R zero y" for y
+        using that by cases simp_all
+    qed
+  next
+    case (succ m)
+    from \<open>\<exists>!y. ?R m y\<close>
+    obtain y where y: "?R m y" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'"
+      by blast
+    show "\<exists>!z. ?R (succ m) z"
+    proof
+      from y show "?R (succ m) (r m y)" ..
+    next
+      fix z
+      assume "?R (succ m) z"
+      then obtain u where "z = r m u" and "?R m u"
+        by cases simp_all
+      with yy' show "z = r m y"
+        by (simp only:)
+    qed
+  qed
+qed
+
+
+text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
+
+definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
+  where "rec e r x = (THE y. Rec e r x y)"
+
+lemma rec_eval:
+  assumes Rec: "Rec e r x y"
+  shows "rec e r x = y"
+  unfolding rec_def
+  using Rec_functional and Rec by (rule the1_equality)
+
+lemma rec_zero [simp]: "rec e r zero = e"
+proof (rule rec_eval)
+  show "Rec e r zero e" ..
+qed
+
+lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
+proof (rule rec_eval)
+  let ?R = "Rec e r"
+  have "?R m (rec e r m)"
+    unfolding rec_def using Rec_functional by (rule theI')
+  then show "?R (succ m) (r m (rec e r m))" ..
+qed
+
+
+text \<open>\<^medskip> Example: addition (monomorphic)\<close>
+
+definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
+  where "add m n = rec n (\<lambda>_ k. succ k) m"
+
+lemma add_zero [simp]: "add zero n = n"
+  and add_succ [simp]: "add (succ m) n = succ (add m n)"
+  unfolding add_def by simp_all
+
+lemma add_assoc: "add (add k m) n = add k (add m n)"
+  by (induct k) simp_all
+
+lemma add_zero_right: "add m zero = m"
+  by (induct m) simp_all
+
+lemma add_succ_right: "add m (succ n) = succ (add m n)"
+  by (induct m) simp_all
+
+lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
+    succ (succ (succ (succ (succ zero))))"
+  by simp
+
+
+text \<open>\<^medskip> Example: replication (polymorphic)\<close>
+
+definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
+  where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
+
+lemma repl_zero [simp]: "repl zero x = []"
+  and repl_succ [simp]: "repl (succ n) x = x # repl n x"
+  unfolding repl_def by simp_all
+
+lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
+  by simp
+
+end
+
+
+text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
+
+interpretation peano 0 Suc
+proof
+  fix m n
+  show "Suc m \<noteq> 0" by simp
+  show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
+  show "P n"
+    if zero: "P 0"
+    and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
+    for P
+  proof (induct n)
+    case 0
+    show ?case by (rule zero)
+  next
+    case Suc
+    then show ?case by (rule succ)
+  qed
+qed
+
+end