author  oheimb 
Fri, 13 Dec 1996 18:45:58 +0100  
changeset 2394  91d8abf108be 
parent 2291  fbd14a05fb88 
child 2640  ee4dfce170a0 
permissions  rwrr 
1479  1 
(* Title: HOLCF/porder.thy 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
1479  3 
Author: Franz Regensburger 
243
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 

297  6 
Conservative extension of theory Porder0 by constant definitions 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

7 

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 

297  10 
Porder = Porder0 + 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

11 

1479  12 
consts 
13 
"<" :: "['a set,'a::po] => bool" (infixl 55) 

14 
"<<" :: "['a set,'a::po] => bool" (infixl 55) 

15 
lub :: "'a set => 'a::po" 

16 
is_tord :: "'a::po set => bool" 

17 
is_chain :: "(nat=>'a::po) => bool" 

18 
max_in_chain :: "[nat,nat=>'a::po]=>bool" 

19 
finite_chain :: "(nat=>'a::po)=>bool" 

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

20 

2394  21 
syntax 
22 

23 
"@LUB" :: "(('b::term) => 'a) => 'a" (binder "LUB " 10) 

24 

25 
translations 

26 

27 
"LUB x. t" == "lub(range(%x.t))" 

28 

29 
syntax (symbols) 

30 

31 
"LUB " :: "[idts, 'a] => 'a" ("(3\\<Squnion>_./ _)"[0,10] 10) 

32 

1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

33 
defs 
243
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 
(* class definitions *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

36 

1479  37 
is_ub "S < x == ! y.y:S > y<<x" 
38 
is_lub "S << x == S < x & (! u. S < u > x << u)" 

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

39 

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 
(* Arbitrary chains are total orders *) 
2394  42 
is_tord "is_tord S == ! x y. x:S & y:S > (x<<y  y<<x)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

43 

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

44 
(* Here we use countable chains and I prefer to code them as functions! *) 
2394  45 
is_chain "is_chain F == (! i.F(i) << F(Suc(i)))" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

46 

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

47 
(* finite chains, needed for monotony of continouous functions *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

48 

1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

49 
max_in_chain_def "max_in_chain i C == ! j. i <= j > C(i) = C(j)" 
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

50 

2394  51 
finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

52 

1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

53 
rules 
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

54 

2394  55 
lub "lub S = (@x. S << x)" 
1274  56 

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

57 
end 
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

58 

74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

59 