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