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