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