author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5102  8c782c25a11e 
child 5273  70f478d55606 
permissions  rwrr 
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. PaulinMohring, Inductive Definitions in the System Coq. 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
Research Report 9249, 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  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)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
monos "[Pow_mono]" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 
end 