author  clasohm 
Wed, 29 Jun 1994 12:03:41 +0200  
changeset 442  13ac1fd0a14d 
parent 243  c22b85994e17 
child 1150  66512c9e6bd6 
permissions  rwrr 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

1 
(* Title: HOLCF/fix.thy 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

3 
Author: Franz Regensburger 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

4 
Copyright 1993 Technische Universitaet Muenchen 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

5 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

6 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

7 
definitions for fixed point operator and admissibility 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

8 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

9 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

10 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

11 
Fix = Cfun3 + 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

12 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

13 
consts 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

14 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

15 
iterate :: "nat=>('a>'a)=>'a=>'a" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

16 
Ifix :: "('a>'a)=>'a" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

17 
fix :: "('a>'a)>'a" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

18 
adm :: "('a=>bool)=>bool" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

19 
admw :: "('a=>bool)=>bool" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

20 
chain_finite :: "'a=>bool" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

21 
flat :: "'a=>bool" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

22 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

23 
rules 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

24 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

25 
iterate_def "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

26 
Ifix_def "Ifix(F) == lub(range(%i.iterate(i,F,UU)))" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

27 
fix_def "fix == (LAM f. Ifix(f))" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

28 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

29 
adm_def "adm(P) == !Y. is_chain(Y) > \ 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

30 
\ (!i.P(Y(i))) > P(lub(range(Y)))" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

31 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

32 
admw_def "admw(P)== (!F.((!n.P(iterate(n,F,UU)))>\ 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

33 
\ P(lub(range(%i.iterate(i,F,UU))))))" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

34 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

35 
chain_finite_def "chain_finite(x::'a)==\ 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

36 
\ !Y. is_chain(Y::nat=>'a) > (? n.max_in_chain(n,Y))" 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

37 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

38 
flat_def "flat(x::'a) ==\ 
442
13ac1fd0a14d
added parentheses made necessary by change of constrain's precedence
clasohm
parents:
243
diff
changeset

39 
\ ! x y. (x::'a) << y > (x = UU)  (x=y)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

40 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

41 
end 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

42 