equal
deleted
inserted
replaced
84 (* ------------------------------------------------------------------------ *) |
84 (* ------------------------------------------------------------------------ *) |
85 (* Type 'a::term => 'b::pcpo is chain complete *) |
85 (* Type 'a::term => 'b::pcpo is chain complete *) |
86 (* ------------------------------------------------------------------------ *) |
86 (* ------------------------------------------------------------------------ *) |
87 |
87 |
88 qed_goal "lub_fun" Fun2.thy |
88 qed_goal "lub_fun" Fun2.thy |
89 "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> \ |
89 "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \ |
90 \ range(S) <<| (% x.lub(range(% i.S(i)(x))))" |
90 \ range(S) <<| (% x.lub(range(% i.S(i)(x))))" |
91 (fn prems => |
91 (fn prems => |
92 [ |
92 [ |
93 (cut_facts_tac prems 1), |
93 (cut_facts_tac prems 1), |
94 (rtac is_lubI 1), |
94 (rtac is_lubI 1), |
109 |
109 |
110 bind_thm ("thelub_fun", lub_fun RS thelubI); |
110 bind_thm ("thelub_fun", lub_fun RS thelubI); |
111 (* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *) |
111 (* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *) |
112 |
112 |
113 qed_goal "cpo_fun" Fun2.thy |
113 qed_goal "cpo_fun" Fun2.thy |
114 "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> ? x. range(S) <<| x" |
114 "is_chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x" |
115 (fn prems => |
115 (fn prems => |
116 [ |
116 [ |
117 (cut_facts_tac prems 1), |
117 (cut_facts_tac prems 1), |
118 (rtac exI 1), |
118 (rtac exI 1), |
119 (etac lub_fun 1) |
119 (etac lub_fun 1) |