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