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