src/HOL/ex/Abstract_NAT.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 44603 a6f9a70d655d
child 58889 5b7a9633cfa8
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
wenzelm@44603
     1
(*  Title:      HOL/ex/Abstract_NAT.thy
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
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@21368
    31
    Rec_zero: "Rec e r zero e"
wenzelm@21368
    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@21368
    45
      fix y assume "?R zero y"
wenzelm@21368
    46
      then show "y = e" by cases simp_all
wenzelm@21368
    47
    qed
wenzelm@21368
    48
  next
wenzelm@21368
    49
    case (succ m)
wenzelm@21368
    50
    from `\<exists>!y. ?R m y`
wenzelm@21368
    51
    obtain y where y: "?R m y"
wenzelm@21368
    52
      and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" 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@21368
    56
      fix z assume "?R (succ m) z"
wenzelm@21368
    57
      then obtain u where "z = r m u" and "?R m u" by cases simp_all
wenzelm@21368
    58
      with yy' show "z = r m y" by (simp only:)
wenzelm@21368
    59
    qed
wenzelm@19087
    60
  qed
wenzelm@19087
    61
qed
wenzelm@19087
    62
wenzelm@19087
    63
wenzelm@21368
    64
text {* \medskip The recursion operator -- polymorphic! *}
wenzelm@19087
    65
wenzelm@44603
    66
definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
wenzelm@44603
    67
  where "rec e r x = (THE y. Rec e r x y)"
wenzelm@19087
    68
wenzelm@21368
    69
lemma rec_eval:
wenzelm@21368
    70
  assumes Rec: "Rec e r x y"
wenzelm@19087
    71
  shows "rec e r x = y"
wenzelm@19087
    72
  unfolding rec_def
wenzelm@19087
    73
  using Rec_functional and Rec by (rule the1_equality)
wenzelm@19087
    74
wenzelm@21368
    75
lemma rec_zero [simp]: "rec e r zero = e"
wenzelm@19087
    76
proof (rule rec_eval)
wenzelm@21392
    77
  show "Rec e r zero e" ..
wenzelm@19087
    78
qed
wenzelm@19087
    79
wenzelm@21368
    80
lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
wenzelm@19087
    81
proof (rule rec_eval)
wenzelm@21368
    82
  let ?R = "Rec e r"
wenzelm@21368
    83
  have "?R m (rec e r m)"
wenzelm@21368
    84
    unfolding rec_def using Rec_functional by (rule theI')
wenzelm@21392
    85
  then show "?R (succ m) (r m (rec e r m))" ..
wenzelm@19087
    86
qed
wenzelm@19087
    87
wenzelm@19087
    88
wenzelm@21368
    89
text {* \medskip Example: addition (monomorphic) *}
wenzelm@21368
    90
wenzelm@44603
    91
definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
wenzelm@44603
    92
  where "add m n = rec n (\<lambda>_ k. succ k) m"
wenzelm@21368
    93
wenzelm@21368
    94
lemma add_zero [simp]: "add zero n = n"
wenzelm@21368
    95
  and add_succ [simp]: "add (succ m) n = succ (add m n)"
wenzelm@21368
    96
  unfolding add_def by simp_all
wenzelm@21368
    97
wenzelm@21368
    98
lemma add_assoc: "add (add k m) n = add k (add m n)"
wenzelm@21368
    99
  by (induct k) simp_all
wenzelm@21368
   100
wenzelm@21368
   101
lemma add_zero_right: "add m zero = m"
wenzelm@21368
   102
  by (induct m) simp_all
wenzelm@21368
   103
wenzelm@21368
   104
lemma add_succ_right: "add m (succ n) = succ (add m n)"
wenzelm@21368
   105
  by (induct m) simp_all
wenzelm@21368
   106
wenzelm@21392
   107
lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
wenzelm@21392
   108
    succ (succ (succ (succ (succ zero))))"
wenzelm@21392
   109
  by simp
wenzelm@21392
   110
wenzelm@21368
   111
wenzelm@21368
   112
text {* \medskip Example: replication (polymorphic) *}
wenzelm@21368
   113
wenzelm@44603
   114
definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
wenzelm@44603
   115
  where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
wenzelm@21368
   116
wenzelm@21368
   117
lemma repl_zero [simp]: "repl zero x = []"
wenzelm@21368
   118
  and repl_succ [simp]: "repl (succ n) x = x # repl n x"
wenzelm@21368
   119
  unfolding repl_def by simp_all
wenzelm@21368
   120
wenzelm@21368
   121
lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
wenzelm@21368
   122
  by simp
wenzelm@21368
   123
wenzelm@21368
   124
end
wenzelm@21368
   125
wenzelm@21368
   126
wenzelm@21368
   127
text {* \medskip Just see that our abstract specification makes sense \dots *}
wenzelm@19087
   128
ballarin@29234
   129
interpretation NAT 0 Suc
wenzelm@19087
   130
proof (rule NAT.intro)
wenzelm@19087
   131
  fix m n
wenzelm@19087
   132
  show "(Suc m = Suc n) = (m = n)" by simp
wenzelm@19087
   133
  show "Suc m \<noteq> 0" by simp
wenzelm@19087
   134
  fix P
wenzelm@19087
   135
  assume zero: "P 0"
wenzelm@19087
   136
    and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
wenzelm@19087
   137
  show "P n"
wenzelm@19087
   138
  proof (induct n)
wenzelm@44603
   139
    case 0
wenzelm@44603
   140
    show ?case by (rule zero)
wenzelm@19087
   141
  next
wenzelm@44603
   142
    case Suc
wenzelm@44603
   143
    then show ?case by (rule succ)
wenzelm@19087
   144
  qed
wenzelm@19087
   145
qed
wenzelm@19087
   146
wenzelm@19087
   147
end