author  kleing 
Mon, 21 Jun 2004 10:25:57 +0200  
changeset 14981  e73f8140af78 
parent 12338  de0f4a63baa5 
child 15562  8455c9671494 
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 

297  5 
Conservative extension of theory Porder0 by constant definitions 
243
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 

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

9 

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

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

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

4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset

14 
tord :: "'a::po set => bool" 
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset

15 
chain :: "(nat=>'a::po) => bool" 
1479  16 
max_in_chain :: "[nat,nat=>'a::po]=>bool" 
17 
finite_chain :: "(nat=>'a::po)=>bool" 

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

18 

2394  19 
syntax 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12114
diff
changeset

20 
"@LUB" :: "('b => 'a) => 'a" (binder "LUB " 10) 
2394  21 

22 
translations 

23 

3842  24 
"LUB x. t" == "lub(range(%x. t))" 
2394  25 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12030
diff
changeset

26 
syntax (xsymbols) 
2394  27 

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

29 

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

30 
defs 
243
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 
(* class definitions *) 
11346  33 
is_ub_def "S < x == ! y. y:S > y<<x" 
34 
is_lub_def "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

35 

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

36 
(* Arbitrary chains are total orders *) 
11346  37 
tord_def "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

38 

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

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

41 

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

42 
(* finite chains, needed for monotony of continouous functions *) 
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

43 
max_in_chain_def "max_in_chain i C == ! j. i <= j > C(i) = C(j)" 
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset

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

45 

2640  46 
lub_def "lub S == (@x. S << x)" 
1274  47 

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

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

49 

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

50 