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