author | wenzelm |
Tue, 29 Aug 2000 20:13:17 +0200 | |
changeset 9730 | 11d137b25555 |
parent 9248 | e1dee89de037 |
child 11346 | 0d28bc664955 |
permissions | -rw-r--r-- |
9245 | 1 |
(* Title: HOLCF/Fun2.ML |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
9245 | 6 |
Class Instance =>::(term,po)po |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
|
2640 | 9 |
(* for compatibility with old HOLCF-Version *) |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
10 |
Goal "(op <<)=(%f g.!x. f x << g x)"; |
9245 | 11 |
by (fold_goals_tac [less_fun_def]); |
12 |
by (rtac refl 1); |
|
13 |
qed "inst_fun_po"; |
|
2640 | 14 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
(* Type 'a::term => 'b::pcpo is pointed *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
19 |
Goal "(%z. UU) << x"; |
9245 | 20 |
by (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1); |
21 |
qed "minimal_fun"; |
|
2640 | 22 |
|
23 |
bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym); |
|
24 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
25 |
Goal "? x::'a=>'b::pcpo.!y. x<<y"; |
9245 | 26 |
by (res_inst_tac [("x","(%z. UU)")] exI 1); |
27 |
by (rtac (minimal_fun RS allI) 1); |
|
28 |
qed "least_fun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
31 |
(* make the symbol << accessible for type fun *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
34 |
Goal "(f1 << f2) = (! x. f1(x) << f2(x))"; |
9245 | 35 |
by (stac inst_fun_po 1); |
36 |
by (rtac refl 1); |
|
37 |
qed "less_fun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
40 |
(* chains of functions yield chains in the po range *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
|
9245 | 43 |
Goalw [chain] "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))"; |
44 |
by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1); |
|
45 |
qed "ch2ch_fun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
46 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
47 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
48 |
(* upper bounds of function chains yield upper bound in the po range *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
49 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
50 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
51 |
Goal "range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)"; |
9245 | 52 |
by (rtac ub_rangeI 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
53 |
by (dtac ub_rangeD 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
54 |
by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
55 |
by Auto_tac; |
9245 | 56 |
qed "ub2ub_fun"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
57 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
59 |
(* Type 'a::term => 'b::pcpo is chain complete *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
60 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
61 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
62 |
Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> \ |
9245 | 63 |
\ range(S) <<| (% x. lub(range(% i. S(i)(x))))"; |
64 |
by (rtac is_lubI 1); |
|
65 |
by (rtac ub_rangeI 1); |
|
66 |
by (stac less_fun 1); |
|
67 |
by (rtac allI 1); |
|
68 |
by (rtac is_ub_thelub 1); |
|
69 |
by (etac ch2ch_fun 1); |
|
70 |
by (strip_tac 1); |
|
71 |
by (stac less_fun 1); |
|
72 |
by (rtac allI 1); |
|
73 |
by (rtac is_lub_thelub 1); |
|
74 |
by (etac ch2ch_fun 1); |
|
75 |
by (etac ub2ub_fun 1); |
|
76 |
qed "lub_fun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
77 |
|
1779 | 78 |
bind_thm ("thelub_fun", lub_fun RS thelubI); |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
79 |
(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
80 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
81 |
Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"; |
9245 | 82 |
by (rtac exI 1); |
83 |
by (etac lub_fun 1); |
|
84 |
qed "cpo_fun"; |