isabelle: src/ZF/ex/Primrec.thy@2c8a8be36c94 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/ex/Primrec.thy
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	5
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	6	Primitive Recursive Functions: the inductive definition
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	7
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	8	Proof adopted from
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	9	Nora Szasz,
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	10	A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	11	In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	12
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	13	See also E. Mendelson, Introduction to Mathematical Logic.
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	14	(Van Nostrand, 1964), page 250, exercise 11.
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	15	*)
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	16
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	17	Primrec = Primrec_defs +
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	18	consts
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	19	prim_rec :: i
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	20
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	21	inductive
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	22	domains "prim_rec" <= "list(nat)->nat"
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	23	intrs
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	24	SC "SC : prim_rec"
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	25	CONST "k: nat ==> CONST(k) : prim_rec"
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	26	PROJ "i: nat ==> PROJ(i) : prim_rec"
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	27	COMP "[\| g: prim_rec; fs: list(prim_rec) \|] ==> COMP(g,fs): prim_rec"
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	28	PREC "[\| f: prim_rec; g: prim_rec \|] ==> PREC(f,g): prim_rec"
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	29	monos "[list_mono]"
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: 3841 diff changeset	30	con_defs "[SC_def, CONST_def, PROJ_def, COMP_def, PREC_def]"
3841 22bbc1676768 fixed fixed dots; wenzelm parents: 3840 diff changeset	31	type_intrs "nat_typechecks @ list.intrs @
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	32	[lam_type, list_case_type, drop_type, map_type,
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	33	apply_type, rec_type]"
515 abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	34
abcc438e7c27 installation of new inductive/datatype sections lcp parents: diff changeset	35	end

author	paulson
	Mon, 28 Dec 1998 16:54:01 +0100
changeset 6046	2c8a8be36c94
parent 6044	e0f9d930e956
child 6117	f9aad8ccd590
permissions	-rw-r--r--