isabelle: src/ZF/ex/Primrec_defs.ML@a528a716a312 (annotated)

6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	1	(* Title: ZF/ex/Primrec
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	2	ID: $Id$
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	4	Copyright 1994 University of Cambridge
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	5
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	6	Primitive Recursive Functions: preliminary definitions
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	7	*)
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	8
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	9	(Theory TF redeclares map_type)
6248 c31c07509637 * empty log message * wenzelm parents: 6153 diff changeset	10	val map_type = thm "List.map_type";
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	11
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	12	( Useful special cases of evaluation *)
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	13
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6248 diff changeset	14	Goalw [SC_def] "[\| x \\<in> nat; l \\<in> list(nat) \|] ==> SC ` (Cons(x,l)) = succ(x)";
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	15	by (Asm_simp_tac 1);
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	16	qed "SC";
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	17
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6248 diff changeset	18	Goalw [CONST_def] "[\| l \\<in> list(nat) \|] ==> CONST(k) ` l = k";
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	19	by (Asm_simp_tac 1);
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	20	qed "CONST";
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	21
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6248 diff changeset	22	Goalw [PROJ_def] "[\| x \\<in> nat; l \\<in> list(nat) \|] ==> PROJ(0) ` (Cons(x,l)) = x";
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	23	by (Asm_simp_tac 1);
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	24	qed "PROJ_0";
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	25
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6248 diff changeset	26	Goalw [COMP_def] "[\| l \\<in> list(nat) \|] ==> COMP(g,[f]) ` l = g` [f`l]";
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	27	by (Asm_simp_tac 1);
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	28	qed "COMP_1";
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	29
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6248 diff changeset	30	Goalw [PREC_def] "l \\<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	31	by (Asm_simp_tac 1);
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	32	qed "PREC_0";
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	33
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	34	Goalw [PREC_def]
11316 b4e71bd751e4 X-symbols for set theory paulson parents: 6248 diff changeset	35	"[\| x \\<in> nat; l \\<in> list(nat) \|] ==> \
6044 e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	36	\ PREC(f,g) ` (Cons(succ(x),l)) = \
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	37	\ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	38	by (Asm_simp_tac 1);
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	39	qed "PREC_succ";
e0f9d930e956 Needs separate theory Primrec_defs due to new inductive defs package paulson parents: diff changeset	40

author	wenzelm
	Sat, 20 Oct 2001 20:20:41 +0200
changeset 11852	a528a716a312
parent 11316	b4e71bd751e4
permissions	-rw-r--r--