src/HOL/ex/Abstract_NAT.thy
author wenzelm
Tue Nov 14 22:16:59 2006 +0100 (2006-11-14)
changeset 21368 bffb2240d03f
parent 20713 823967ef47f1
child 21392 e571e84cbe89
permissions -rw-r--r--
converted to 'inductive2';
proper localized definitions;
added rec examples;
wenzelm@19087
     1
(*
wenzelm@19087
     2
    ID:         $Id$
wenzelm@19087
     3
    Author:     Makarius
wenzelm@19087
     4
*)
wenzelm@19087
     5
wenzelm@19087
     6
header {* Abstract Natural Numbers with polymorphic 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
wenzelm@21368
    29
inductive2
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@21368
    46
      show "?R zero e" by (rule Rec_zero)
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@21368
    57
      from y show "?R (succ m) (r m y)" by (rule Rec_succ)
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@21368
    69
  rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
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@21368
    80
  show "Rec e r zero e" by (rule Rec_zero)
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@21368
    88
  then show "?R (succ m) (r m (rec e r m))" by (rule Rec_succ)
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@21368
    95
  add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
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@21368
   111
wenzelm@21368
   112
text {* \medskip Example: replication (polymorphic) *}
wenzelm@21368
   113
wenzelm@21368
   114
definition
wenzelm@21368
   115
  repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
wenzelm@21368
   116
  "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
wenzelm@21368
   117
wenzelm@21368
   118
lemma repl_zero [simp]: "repl zero x = []"
wenzelm@21368
   119
  and repl_succ [simp]: "repl (succ n) x = x # repl n x"
wenzelm@21368
   120
  unfolding repl_def by simp_all
wenzelm@21368
   121
wenzelm@21368
   122
lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
wenzelm@21368
   123
  by simp
wenzelm@21368
   124
wenzelm@21368
   125
end
wenzelm@21368
   126
wenzelm@21368
   127
wenzelm@21368
   128
text {* \medskip Just see that our abstract specification makes sense \dots *}
wenzelm@19087
   129
wenzelm@19087
   130
interpretation NAT [0 Suc]
wenzelm@19087
   131
proof (rule NAT.intro)
wenzelm@19087
   132
  fix m n
wenzelm@19087
   133
  show "(Suc m = Suc n) = (m = n)" by simp
wenzelm@19087
   134
  show "Suc m \<noteq> 0" by simp
wenzelm@19087
   135
  fix P
wenzelm@19087
   136
  assume zero: "P 0"
wenzelm@19087
   137
    and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
wenzelm@19087
   138
  show "P n"
wenzelm@19087
   139
  proof (induct n)
wenzelm@19087
   140
    case 0 show ?case by (rule zero)
wenzelm@19087
   141
  next
wenzelm@19087
   142
    case Suc then show ?case by (rule succ)
wenzelm@19087
   143
  qed
wenzelm@19087
   144
qed
wenzelm@19087
   145
wenzelm@19087
   146
end