# HG changeset patch # User wenzelm # Date 1140120723 -3600 # Node ID 8d83af663714ca2b65d0c04827dabb6de9f84a2d # Parent 1b3780be6cc25a2d0e111fb94e1d0636f23d0fd7 Abstract Natural Numbers with polymorphic recursion. diff -r 1b3780be6cc2 -r 8d83af663714 src/HOL/ex/Abstract_NAT.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Abstract_NAT.thy Thu Feb 16 21:12:03 2006 +0100 @@ -0,0 +1,113 @@ +(* + ID: $Id$ + Author: Makarius +*) + +header {* Abstract Natural Numbers with polymorphic recursion *} + +theory Abstract_NAT +imports Main +begin + +text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *} + +locale NAT = + fixes zero :: 'n + and succ :: "'n \ 'n" + assumes succ_inject [simp]: "(succ m = succ n) = (m = n)" + and succ_neq_zero [simp]: "succ m \ zero" + and induct [case_names zero succ, induct type: 'n]: + "P zero \ (\n. P n \ P (succ n)) \ P n" + +lemma (in NAT) zero_neq_succ [simp]: "zero \ succ m" + by (rule succ_neq_zero [symmetric]) + + +text {* + Primitive recursion as a (functional) relation -- polymorphic! + + (We simulate a localized version of the inductive packages using + explicit premises + parameters, and an abbreviation.) *} + +consts + REC :: "'n \ ('n \ 'n) \ 'a \ ('n \ 'a \ 'a) \ ('n * 'a) set" +inductive "REC zero succ e r" + intros + Rec_zero: "NAT zero succ \ (zero, e) \ REC zero succ e r" + Rec_succ: "NAT zero succ \ (m, n) \ REC zero succ e r \ + (succ m, r m n) \ REC zero succ e r" + +abbreviation (in NAT) (output) + "Rec = REC zero succ" + +lemma (in NAT) Rec_functional: + fixes x :: 'n + shows "\!y::'a. (x, y) \ Rec e r" (is "\!y::'a. _ \ ?Rec") +proof (induct x) + case zero + show "\!y. (zero, y) \ ?Rec" + proof + show "(zero, e) \ ?Rec" by (rule Rec_zero) + fix y assume "(zero, y) \ ?Rec" + then show "y = e" by cases simp_all + qed +next + case (succ m) + from `\!y. (m, y) \ ?Rec` + obtain y where y: "(m, y) \ ?Rec" + and yy': "\y'. (m, y') \ ?Rec \ y = y'" by blast + show "\!z. (succ m, z) \ ?Rec" + proof + from _ y show "(succ m, r m y) \ ?Rec" by (rule Rec_succ) + fix z assume "(succ m, z) \ ?Rec" + then obtain u where "z = r m u" and "(m, u) \ ?Rec" by cases simp_all + with yy' show "z = r m y" by (simp only:) + qed +qed + + +text {* The recursion operator -- polymorphic! *} + +definition (in NAT) + "rec e r x = (THE y. (x, y) \ Rec e r)" + +lemma (in NAT) rec_eval: + assumes Rec: "(x, y) \ Rec e r" + shows "rec e r x = y" + unfolding rec_def + using Rec_functional and Rec by (rule the1_equality) + +lemma (in NAT) rec_zero: "rec e r zero = e" +proof (rule rec_eval) + show "(zero, e) \ Rec e r" by (rule Rec_zero) +qed + +lemma (in NAT) rec_succ: "rec e r (succ m) = r m (rec e r m)" +proof (rule rec_eval) + let ?Rec = "Rec e r" + have "(m, rec e r m) \ ?Rec" + unfolding rec_def + using Rec_functional by (rule theI') + with _ show "(succ m, r m (rec e r m)) \ ?Rec" by (rule Rec_succ) +qed + + +text {* Just see that our abstract specification makes sense \dots *} + +interpretation NAT [0 Suc] +proof (rule NAT.intro) + fix m n + show "(Suc m = Suc n) = (m = n)" by simp + show "Suc m \ 0" by simp + fix P + assume zero: "P 0" + and succ: "\n. P n \ P (Suc n)" + show "P n" + proof (induct n) + case 0 show ?case by (rule zero) + next + case Suc then show ?case by (rule succ) + qed +qed + +end