author | paulson |
Mon, 23 Sep 1996 18:18:18 +0200 | |
changeset 2010 | 0a22b9d63a18 |
parent 1779 | 1155c06fa956 |
child 2033 | 639de962ded4 |
permissions | -rw-r--r-- |
1461 | 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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
Lemmas for fun2.thy |
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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
open Fun2; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
(* Type 'a::term => 'b::pcpo is pointed *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
|
892 | 15 |
qed_goalw "minimal_fun" Fun2.thy [UU_fun_def] "UU_fun << f" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
(fn prems => |
1461 | 17 |
[ |
18 |
(rtac (inst_fun_po RS ssubst) 1), |
|
19 |
(rewtac less_fun_def), |
|
20 |
(fast_tac (HOL_cs addSIs [minimal]) 1) |
|
21 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
23 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
(* make the symbol << accessible for type fun *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
26 |
|
892 | 27 |
qed_goal "less_fun" Fun2.thy "(f1 << f2) = (! x. f1(x) << f2(x))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
(fn prems => |
1461 | 29 |
[ |
30 |
(rtac (inst_fun_po RS ssubst) 1), |
|
31 |
(fold_goals_tac [less_fun_def]), |
|
32 |
(rtac refl 1) |
|
33 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
34 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
36 |
(* 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
|
37 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
|
892 | 39 |
qed_goal "ch2ch_fun" Fun2.thy |
1461 | 40 |
"is_chain(S::nat=>('a::term => 'b::po)) ==> is_chain(% i.S(i)(x))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
(fn prems => |
1461 | 42 |
[ |
43 |
(cut_facts_tac prems 1), |
|
44 |
(rewtac is_chain), |
|
45 |
(rtac allI 1), |
|
46 |
(rtac spec 1), |
|
47 |
(rtac (less_fun RS subst) 1), |
|
48 |
(etac allE 1), |
|
49 |
(atac 1) |
|
50 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
51 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
(* 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
|
54 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
|
892 | 56 |
qed_goal "ub2ub_fun" Fun2.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
57 |
" range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
(fn prems => |
1461 | 59 |
[ |
60 |
(cut_facts_tac prems 1), |
|
61 |
(rtac ub_rangeI 1), |
|
62 |
(rtac allI 1), |
|
63 |
(rtac allE 1), |
|
64 |
(rtac (less_fun RS subst) 1), |
|
65 |
(etac (ub_rangeE RS spec) 1), |
|
66 |
(atac 1) |
|
67 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
68 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
69 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
70 |
(* Type 'a::term => 'b::pcpo is chain complete *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
71 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
72 |
|
892 | 73 |
qed_goal "lub_fun" Fun2.thy |
1461 | 74 |
"is_chain(S::nat=>('a::term => 'b::pcpo)) ==> \ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
75 |
\ range(S) <<| (% x.lub(range(% i.S(i)(x))))" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
76 |
(fn prems => |
1461 | 77 |
[ |
78 |
(cut_facts_tac prems 1), |
|
79 |
(rtac is_lubI 1), |
|
80 |
(rtac conjI 1), |
|
81 |
(rtac ub_rangeI 1), |
|
82 |
(rtac allI 1), |
|
83 |
(rtac (less_fun RS ssubst) 1), |
|
84 |
(rtac allI 1), |
|
85 |
(rtac is_ub_thelub 1), |
|
86 |
(etac ch2ch_fun 1), |
|
87 |
(strip_tac 1), |
|
88 |
(rtac (less_fun RS ssubst) 1), |
|
89 |
(rtac allI 1), |
|
90 |
(rtac is_lub_thelub 1), |
|
91 |
(etac ch2ch_fun 1), |
|
92 |
(etac ub2ub_fun 1) |
|
93 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
94 |
|
1779 | 95 |
bind_thm ("thelub_fun", lub_fun RS thelubI); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
96 |
(* is_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
|
97 |
|
892 | 98 |
qed_goal "cpo_fun" Fun2.thy |
1461 | 99 |
"is_chain(S::nat=>('a::term => 'b::pcpo)) ==> ? x. range(S) <<| x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
100 |
(fn prems => |
1461 | 101 |
[ |
102 |
(cut_facts_tac prems 1), |
|
103 |
(rtac exI 1), |
|
104 |
(etac lub_fun 1) |
|
105 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
106 |