src/HOL/ex/Abstract_NAT.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63054 1b237d147cc4
permissions -rw-r--r--
bundle lifting_syntax;
     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       show "y = e" if "?R zero y" for y
    46         using that 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" and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'"
    52       by blast
    53     show "\<exists>!z. ?R (succ m) z"
    54     proof
    55       from y show "?R (succ m) (r m y)" ..
    56     next
    57       fix z
    58       assume "?R (succ m) z"
    59       then obtain u where "z = r m u" and "?R m u"
    60         by cases simp_all
    61       with yy' show "z = r m y"
    62         by (simp only:)
    63     qed
    64   qed
    65 qed
    66 
    67 
    68 text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>
    69 
    70 definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
    71   where "rec e r x = (THE y. Rec e r x y)"
    72 
    73 lemma rec_eval:
    74   assumes Rec: "Rec e r x y"
    75   shows "rec e r x = y"
    76   unfolding rec_def
    77   using Rec_functional and Rec by (rule the1_equality)
    78 
    79 lemma rec_zero [simp]: "rec e r zero = e"
    80 proof (rule rec_eval)
    81   show "Rec e r zero e" ..
    82 qed
    83 
    84 lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
    85 proof (rule rec_eval)
    86   let ?R = "Rec e r"
    87   have "?R m (rec e r m)"
    88     unfolding rec_def using Rec_functional by (rule theI')
    89   then show "?R (succ m) (r m (rec e r m))" ..
    90 qed
    91 
    92 
    93 text \<open>\<^medskip> Example: addition (monomorphic)\<close>
    94 
    95 definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
    96   where "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 \<open>\<^medskip> Example: replication (polymorphic)\<close>
   117 
   118 definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
   119   where "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 \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>
   132 
   133 interpretation NAT 0 Suc
   134 proof (rule NAT.intro)
   135   fix m n
   136   show "Suc m = Suc n \<longleftrightarrow> m = n" by simp
   137   show "Suc m \<noteq> 0" by simp
   138   show "P n"
   139     if zero: "P 0"
   140     and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
   141     for P
   142   proof (induct n)
   143     case 0
   144     show ?case by (rule zero)
   145   next
   146     case Suc
   147     then show ?case by (rule succ)
   148   qed
   149 qed
   150 
   151 end