isabelle: src/HOL/Induct/Acc.thy@0a604b2fc2b1 (annotated)

3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	1	(* Title: HOL/ex/Acc.thy
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	2	ID: $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	4	Copyright 1994 University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	5
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	6	Inductive definition of acc(r)
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	7
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	8	See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	9	Research Report 92-49, LIP, ENS Lyon. Dec 1992.
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	10	*)
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	11
7867 2efb66472812 fixed comment; wenzelm parents: 7800 diff changeset	12	header {* The accessible part of a relation *};
7759 44dd5dc8e90f tuned presentation; wenzelm parents: 7721 diff changeset	13
44dd5dc8e90f tuned presentation; wenzelm parents: 7721 diff changeset	14	theory Acc = WF + Inductive:;
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	15
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	16	consts
7759 44dd5dc8e90f tuned presentation; wenzelm parents: 7721 diff changeset	17	acc :: "('a * 'a)set => 'a set" -- {* accessible part *};
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	18
7721 cb353d802ade Tuned inductive definition. berghofe parents: 5717 diff changeset	19	inductive "acc r"
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	20	intrs
7800 8ee919e42174 improved presentation; wenzelm parents: 7759 diff changeset	21	accI [rulify_prems]:
8ee919e42174 improved presentation; wenzelm parents: 7759 diff changeset	22	"ALL y. (y, x) : r --> y : acc r ==> x : acc r"
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	23
7800 8ee919e42174 improved presentation; wenzelm parents: 7759 diff changeset	24	syntax
8ee919e42174 improved presentation; wenzelm parents: 7759 diff changeset	25	termi :: "('a * 'a)set => 'a set"
8ee919e42174 improved presentation; wenzelm parents: 7759 diff changeset	26	translations
8ee919e42174 improved presentation; wenzelm parents: 7759 diff changeset	27	"termi r" == "acc(r^-1)"
5273 70f478d55606 Added macro `termi' nipkow parents: 5102 diff changeset	28
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	29	end

author	wenzelm
	Sun, 31 Oct 1999 20:11:23 +0100
changeset 7990	0a604b2fc2b1
parent 7867	2efb66472812
child 9101	b643f4d7b9e9
permissions	-rw-r--r--