22 val mem_const = Const("op :", [iT,iT]--->FOLogic.oT); |
22 val mem_const = Const("op :", [iT,iT]--->FOLogic.oT); |
23 |
23 |
24 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
24 (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) |
25 fun mk_all_imp (A,P) = |
25 fun mk_all_imp (A,P) = |
26 FOLogic.all_const iT $ |
26 FOLogic.all_const iT $ |
27 Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0)); |
27 Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ |
|
28 betapply(P, Bound 0)); |
28 |
29 |
29 val Part_const = Const("Part", [iT,iT-->iT]--->iT); |
30 val Part_const = Const("Part", [iT,iT-->iT]--->iT); |
30 |
31 |
31 val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT); |
32 val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT); |
32 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); |
33 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); |