1 (* Title: HOLCF/Fun2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 *) |
|
5 |
1 |
6 (* for compatibility with old HOLCF-Version *) |
2 (* legacy ML bindings *) |
7 Goal "(op <<)=(%f g.!x. f x << g x)"; |
|
8 by (fold_goals_tac [less_fun_def]); |
|
9 by (rtac refl 1); |
|
10 qed "inst_fun_po"; |
|
11 |
3 |
12 (* ------------------------------------------------------------------------ *) |
4 val inst_fun_po = thm "inst_fun_po"; |
13 (* Type 'a::type => 'b::pcpo is pointed *) |
5 val minimal_fun = thm "minimal_fun"; |
14 (* ------------------------------------------------------------------------ *) |
6 val UU_fun_def = thm "UU_fun_def"; |
15 |
7 val least_fun = thm "least_fun"; |
16 Goal "(%z. UU) << x"; |
8 val less_fun = thm "less_fun"; |
17 by (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1); |
9 val ch2ch_fun = thm "ch2ch_fun"; |
18 qed "minimal_fun"; |
10 val ub2ub_fun = thm "ub2ub_fun"; |
19 |
11 val lub_fun = thm "lub_fun"; |
20 bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym); |
12 val thelub_fun = thm "thelub_fun"; |
21 |
13 val cpo_fun = thm "cpo_fun"; |
22 Goal "? x::'a=>'b::pcpo.!y. x<<y"; |
|
23 by (res_inst_tac [("x","(%z. UU)")] exI 1); |
|
24 by (rtac (minimal_fun RS allI) 1); |
|
25 qed "least_fun"; |
|
26 |
|
27 (* ------------------------------------------------------------------------ *) |
|
28 (* make the symbol << accessible for type fun *) |
|
29 (* ------------------------------------------------------------------------ *) |
|
30 |
|
31 Goal "(f1 << f2) = (! x. f1(x) << f2(x))"; |
|
32 by (stac inst_fun_po 1); |
|
33 by (rtac refl 1); |
|
34 qed "less_fun"; |
|
35 |
|
36 (* ------------------------------------------------------------------------ *) |
|
37 (* chains of functions yield chains in the po range *) |
|
38 (* ------------------------------------------------------------------------ *) |
|
39 |
|
40 Goalw [chain_def] "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)"; |
|
41 by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1); |
|
42 qed "ch2ch_fun"; |
|
43 |
|
44 (* ------------------------------------------------------------------------ *) |
|
45 (* upper bounds of function chains yield upper bound in the po range *) |
|
46 (* ------------------------------------------------------------------------ *) |
|
47 |
|
48 Goal "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)"; |
|
49 by (rtac ub_rangeI 1); |
|
50 by (dtac ub_rangeD 1); |
|
51 by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1); |
|
52 by Auto_tac; |
|
53 qed "ub2ub_fun"; |
|
54 |
|
55 (* ------------------------------------------------------------------------ *) |
|
56 (* Type 'a::type => 'b::pcpo is chain complete *) |
|
57 (* ------------------------------------------------------------------------ *) |
|
58 |
|
59 Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> \ |
|
60 \ range(S) <<| (% x. lub(range(% i. S(i)(x))))"; |
|
61 by (rtac is_lubI 1); |
|
62 by (rtac ub_rangeI 1); |
|
63 by (stac less_fun 1); |
|
64 by (rtac allI 1); |
|
65 by (rtac is_ub_thelub 1); |
|
66 by (etac ch2ch_fun 1); |
|
67 by (strip_tac 1); |
|
68 by (stac less_fun 1); |
|
69 by (rtac allI 1); |
|
70 by (rtac is_lub_thelub 1); |
|
71 by (etac ch2ch_fun 1); |
|
72 by (etac ub2ub_fun 1); |
|
73 qed "lub_fun"; |
|
74 |
|
75 bind_thm ("thelub_fun", lub_fun RS thelubI); |
|
76 (* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *) |
|
77 |
|
78 Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x"; |
|
79 by (rtac exI 1); |
|
80 by (etac lub_fun 1); |
|
81 qed "cpo_fun"; |
|