src/HOL/ex/Abstract_NAT.thy
 author wenzelm Sat Nov 22 14:57:04 2014 +0100 (2014-11-22) changeset 59031 4c3bb56b8ce7 parent 58889 5b7a9633cfa8 child 63054 1b237d147cc4 permissions -rw-r--r--
misc tuning and modernization;
```     1 (*  Title:      HOL/ex/Abstract_NAT.thy
```
```     2     Author:     Makarius
```
```     3 *)
```
```     4
```
```     5 section \<open>Abstract Natural Numbers primitive recursion\<close>
```
```     6
```
```     7 theory Abstract_NAT
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 text \<open>Axiomatic Natural Numbers (Peano) -- a monomorphic theory.\<close>
```
```    12
```
```    13 locale NAT =
```
```    14   fixes zero :: 'n
```
```    15     and succ :: "'n \<Rightarrow> 'n"
```
```    16   assumes succ_inject [simp]: "succ m = succ n \<longleftrightarrow> m = n"
```
```    17     and succ_neq_zero [simp]: "succ m \<noteq> zero"
```
```    18     and induct [case_names zero succ, induct type: 'n]:
```
```    19       "P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n"
```
```    20 begin
```
```    21
```
```    22 lemma zero_neq_succ [simp]: "zero \<noteq> succ m"
```
```    23   by (rule succ_neq_zero [symmetric])
```
```    24
```
```    25
```
```    26 text \<open>\medskip Primitive recursion as a (functional) relation -- polymorphic!\<close>
```
```    27
```
```    28 inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
```
```    29   for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
```
```    30 where
```
```    31     Rec_zero: "Rec e r zero e"
```
```    32   | Rec_succ: "Rec e r m n \<Longrightarrow> Rec e r (succ m) (r m n)"
```
```    33
```
```    34 lemma Rec_functional:
```
```    35   fixes x :: 'n
```
```    36   shows "\<exists>!y::'a. Rec e r x y"
```
```    37 proof -
```
```    38   let ?R = "Rec e r"
```
```    39   show ?thesis
```
```    40   proof (induct x)
```
```    41     case zero
```
```    42     show "\<exists>!y. ?R zero y"
```
```    43     proof
```
```    44       show "?R zero e" ..
```
```    45       fix y assume "?R zero y"
```
```    46       then show "y = e" by cases simp_all
```
```    47     qed
```
```    48   next
```
```    49     case (succ m)
```
```    50     from \<open>\<exists>!y. ?R m y\<close>
```
```    51     obtain y where y: "?R m y"
```
```    52       and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
```
```    53     show "\<exists>!z. ?R (succ m) z"
```
```    54     proof
```
```    55       from y show "?R (succ m) (r m y)" ..
```
```    56       fix z assume "?R (succ m) z"
```
```    57       then obtain u where "z = r m u" and "?R m u" by cases simp_all
```
```    58       with yy' show "z = r m y" by (simp only:)
```
```    59     qed
```
```    60   qed
```
```    61 qed
```
```    62
```
```    63
```
```    64 text \<open>\medskip The recursion operator -- polymorphic!\<close>
```
```    65
```
```    66 definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
```
```    67   where "rec e r x = (THE y. Rec e r x y)"
```
```    68
```
```    69 lemma rec_eval:
```
```    70   assumes Rec: "Rec e r x y"
```
```    71   shows "rec e r x = y"
```
```    72   unfolding rec_def
```
```    73   using Rec_functional and Rec by (rule the1_equality)
```
```    74
```
```    75 lemma rec_zero [simp]: "rec e r zero = e"
```
```    76 proof (rule rec_eval)
```
```    77   show "Rec e r zero e" ..
```
```    78 qed
```
```    79
```
```    80 lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
```
```    81 proof (rule rec_eval)
```
```    82   let ?R = "Rec e r"
```
```    83   have "?R m (rec e r m)"
```
```    84     unfolding rec_def using Rec_functional by (rule theI')
```
```    85   then show "?R (succ m) (r m (rec e r m))" ..
```
```    86 qed
```
```    87
```
```    88
```
```    89 text \<open>\medskip Example: addition (monomorphic)\<close>
```
```    90
```
```    91 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
```
```    92   where "add m n = rec n (\<lambda>_ k. succ k) m"
```
```    93
```
```    94 lemma add_zero [simp]: "add zero n = n"
```
```    95   and add_succ [simp]: "add (succ m) n = succ (add m n)"
```
```    96   unfolding add_def by simp_all
```
```    97
```
```    98 lemma add_assoc: "add (add k m) n = add k (add m n)"
```
```    99   by (induct k) simp_all
```
```   100
```
```   101 lemma add_zero_right: "add m zero = m"
```
```   102   by (induct m) simp_all
```
```   103
```
```   104 lemma add_succ_right: "add m (succ n) = succ (add m n)"
```
```   105   by (induct m) simp_all
```
```   106
```
```   107 lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
```
```   108     succ (succ (succ (succ (succ zero))))"
```
```   109   by simp
```
```   110
```
```   111
```
```   112 text \<open>\medskip Example: replication (polymorphic)\<close>
```
```   113
```
```   114 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
```
```   115   where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
```
```   116
```
```   117 lemma repl_zero [simp]: "repl zero x = []"
```
```   118   and repl_succ [simp]: "repl (succ n) x = x # repl n x"
```
```   119   unfolding repl_def by simp_all
```
```   120
```
```   121 lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
```
```   122   by simp
```
```   123
```
```   124 end
```
```   125
```
```   126
```
```   127 text \<open>\medskip Just see that our abstract specification makes sense \dots\<close>
```
```   128
```
```   129 interpretation NAT 0 Suc
```
```   130 proof (rule NAT.intro)
```
```   131   fix m n
```
```   132   show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
```
```   133   show "Suc m \<noteq> 0" by simp
```
```   134   fix P
```
```   135   assume zero: "P 0"
```
```   136     and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
```
```   137   show "P n"
```
```   138   proof (induct n)
```
```   139     case 0
```
```   140     show ?case by (rule zero)
```
```   141   next
```
```   142     case Suc
```
```   143     then show ?case by (rule succ)
```
```   144   qed
```
```   145 qed
```
```   146
```
```   147 end
```