isabelle: src/HOL/Induct/Acc.thy@06189132c67b (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
5102 8c782c25a11e Adapted to new inductive definition package. berghofe parents: 3120 diff changeset	12	Acc = WF + Inductive +
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	13
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	14	constdefs
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	15	pred :: "['b, ('a * 'b)set] => 'a set" (Set of predecessors)
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	16	"pred x r == {y. (y,x):r}"
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	17
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	18	consts
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	19	acc :: "('a * 'a)set => 'a set" (Accessible part)
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	20
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	21	inductive "acc(r)"
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	22	intrs
c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	23	pred "pred a r: Pow(acc(r)) ==> a: acc(r)"
5717 0d28dbe484b6 Changed syntax of inductive. berghofe parents: 5273 diff changeset	24	monos Pow_mono
3120 c58423c20740 New directory to contain examples of (co)inductive definitions paulson parents: diff changeset	25
5273 70f478d55606 Added macro `termi' nipkow parents: 5102 diff changeset	26	syntax termi :: "('a * 'a)set => 'a set"
70f478d55606 Added macro `termi' nipkow parents: 5102 diff changeset	27	translations "termi r" == "acc(r^-1)"
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	paulson
	Thu, 27 May 1999 10:13:52 +0200
changeset 6738	06189132c67b
parent 5717	0d28dbe484b6
child 7721	cb353d802ade
permissions	-rw-r--r--