src/HOL/ex/Abstract_NAT.thy
author wenzelm
Thu Feb 16 21:12:03 2006 +0100 (2006-02-16)
changeset 19087 8d83af663714
child 19363 667b5ea637dd
permissions -rw-r--r--
Abstract Natural Numbers with polymorphic recursion.
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@19087
    21
wenzelm@19087
    22
lemma (in NAT) zero_neq_succ [simp]: "zero \<noteq> succ m"
wenzelm@19087
    23
  by (rule succ_neq_zero [symmetric])
wenzelm@19087
    24
wenzelm@19087
    25
wenzelm@19087
    26
text {*
wenzelm@19087
    27
  Primitive recursion as a (functional) relation -- polymorphic!
wenzelm@19087
    28
wenzelm@19087
    29
  (We simulate a localized version of the inductive packages using
wenzelm@19087
    30
  explicit premises + parameters, and an abbreviation.) *}
wenzelm@19087
    31
wenzelm@19087
    32
consts
wenzelm@19087
    33
  REC :: "'n \<Rightarrow> ('n \<Rightarrow> 'n) \<Rightarrow> 'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('n * 'a) set"
wenzelm@19087
    34
inductive "REC zero succ e r"
wenzelm@19087
    35
  intros
wenzelm@19087
    36
    Rec_zero: "NAT zero succ \<Longrightarrow> (zero, e) \<in> REC zero succ e r"
wenzelm@19087
    37
    Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
wenzelm@19087
    38
      (succ m, r m n) \<in> REC zero succ e r"
wenzelm@19087
    39
wenzelm@19087
    40
abbreviation (in NAT) (output)
wenzelm@19087
    41
  "Rec = REC zero succ"
wenzelm@19087
    42
wenzelm@19087
    43
lemma (in NAT) Rec_functional:
wenzelm@19087
    44
  fixes x :: 'n
wenzelm@19087
    45
  shows "\<exists>!y::'a. (x, y) \<in> Rec e r"  (is "\<exists>!y::'a. _ \<in> ?Rec")
wenzelm@19087
    46
proof (induct x)
wenzelm@19087
    47
  case zero
wenzelm@19087
    48
  show "\<exists>!y. (zero, y) \<in> ?Rec"
wenzelm@19087
    49
  proof
wenzelm@19087
    50
    show "(zero, e) \<in> ?Rec" by (rule Rec_zero)
wenzelm@19087
    51
    fix y assume "(zero, y) \<in> ?Rec"
wenzelm@19087
    52
    then show "y = e" by cases simp_all
wenzelm@19087
    53
  qed
wenzelm@19087
    54
next
wenzelm@19087
    55
  case (succ m)
wenzelm@19087
    56
  from `\<exists>!y. (m, y) \<in> ?Rec`
wenzelm@19087
    57
  obtain y where y: "(m, y) \<in> ?Rec"
wenzelm@19087
    58
    and yy': "\<And>y'. (m, y') \<in> ?Rec \<Longrightarrow> y = y'" by blast
wenzelm@19087
    59
  show "\<exists>!z. (succ m, z) \<in> ?Rec"
wenzelm@19087
    60
  proof
wenzelm@19087
    61
    from _ y show "(succ m, r m y) \<in> ?Rec" by (rule Rec_succ)
wenzelm@19087
    62
    fix z assume "(succ m, z) \<in> ?Rec"
wenzelm@19087
    63
    then obtain u where "z = r m u" and "(m, u) \<in> ?Rec" by cases simp_all
wenzelm@19087
    64
    with yy' show "z = r m y" by (simp only:)
wenzelm@19087
    65
  qed
wenzelm@19087
    66
qed
wenzelm@19087
    67
wenzelm@19087
    68
wenzelm@19087
    69
text {* The recursion operator -- polymorphic! *}
wenzelm@19087
    70
wenzelm@19087
    71
definition (in NAT)
wenzelm@19087
    72
  "rec e r x = (THE y. (x, y) \<in> Rec e r)"
wenzelm@19087
    73
wenzelm@19087
    74
lemma (in NAT) rec_eval:
wenzelm@19087
    75
  assumes Rec: "(x, y) \<in> Rec e r"
wenzelm@19087
    76
  shows "rec e r x = y"
wenzelm@19087
    77
  unfolding rec_def
wenzelm@19087
    78
  using Rec_functional and Rec by (rule the1_equality)
wenzelm@19087
    79
wenzelm@19087
    80
lemma (in NAT) rec_zero: "rec e r zero = e"
wenzelm@19087
    81
proof (rule rec_eval)
wenzelm@19087
    82
  show "(zero, e) \<in> Rec e r" by (rule Rec_zero)
wenzelm@19087
    83
qed
wenzelm@19087
    84
wenzelm@19087
    85
lemma (in NAT) rec_succ: "rec e r (succ m) = r m (rec e r m)"
wenzelm@19087
    86
proof (rule rec_eval)
wenzelm@19087
    87
  let ?Rec = "Rec e r"
wenzelm@19087
    88
  have "(m, rec e r m) \<in> ?Rec"
wenzelm@19087
    89
    unfolding rec_def
wenzelm@19087
    90
    using Rec_functional by (rule theI')
wenzelm@19087
    91
  with _ show "(succ m, r m (rec e r m)) \<in> ?Rec" by (rule Rec_succ)
wenzelm@19087
    92
qed
wenzelm@19087
    93
wenzelm@19087
    94
wenzelm@19087
    95
text {* Just see that our abstract specification makes sense \dots *}
wenzelm@19087
    96
wenzelm@19087
    97
interpretation NAT [0 Suc]
wenzelm@19087
    98
proof (rule NAT.intro)
wenzelm@19087
    99
  fix m n
wenzelm@19087
   100
  show "(Suc m = Suc n) = (m = n)" by simp
wenzelm@19087
   101
  show "Suc m \<noteq> 0" by simp
wenzelm@19087
   102
  fix P
wenzelm@19087
   103
  assume zero: "P 0"
wenzelm@19087
   104
    and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
wenzelm@19087
   105
  show "P n"
wenzelm@19087
   106
  proof (induct n)
wenzelm@19087
   107
    case 0 show ?case by (rule zero)
wenzelm@19087
   108
  next
wenzelm@19087
   109
    case Suc then show ?case by (rule succ)
wenzelm@19087
   110
  qed
wenzelm@19087
   111
qed
wenzelm@19087
   112
wenzelm@19087
   113
end